chore: bump lean version and disable equations (#52)

* chore: bump lean version

* unfix

* bump and disable equations

Author: b-mehta

lake-manifest.json

@@ -15,17 +15,17 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "c211948581bde9846a99e32d97a03f0d5307c31e",
+   "rev": "4e57d17bdc121dc17f25f2d8240a584c76a3a66e",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.20.0",
+   "inputRev": "v4.21.0-rc1",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2ac43674e92a695e96caac19f4002b25434636da",
+   "rev": "91ce5a8051438870cbb4e3c68cd12e23ace713b1",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a11bcb5238149ae5d8a0aa5e2f8eddf8a3a9b27d",
+   "rev": "d554d45b37832f5f8e8797ac0b00be585c8aea49",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,17 +55,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "21e6a0522cd2ae6cf88e9da99a1dd010408ab306",
+   "rev": "7518acaafc0ba29be6de6c3f37637fe4148b72cb",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.60",
+   "inputRev": "v0.0.61",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "ddfca7829bf8aa4083cdf9633935dddbb28b7b2a",
+   "rev": "c548baa6d2ed727c6e9b30ff627b7c67fda4a54c",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2865ea099ab1dd8d6fc93381d77a4ac87a85527a",
+   "rev": "f827c08bdd5044b75f0fdc3178c0c600e818b76f",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "7a0d63fbf8fd350e891868a06d9927efa545ac1e",
+   "rev": "3aafa48516440d6038efb626660c74dec6e640da",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -95,7 +95,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "f9e25dcbed001489c53bceeb1f1d50bbaf7451d4",
+   "rev": "1606fed39cd8bd366f8a192e6558972af869efa6",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lakefile.toml

@@ -14,6 +14,7 @@ linter.style.multiGoal = true # no multiple active goals
 [[require]]
 name = "mathlib"
 git = "https://github.com/leanprover-community/mathlib4.git"
+rev = "v4.21.0-rc1"
 
 [[require]]
 name = "checkdecls"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.20.0
+leanprover/lean4:v4.21.0-rc1

scripts/build_docs.sh

@@ -31,4 +31,4 @@ cd docbuild
 MATHLIB_NO_CACHE_ON_UPDATE=1 ~/.elan/bin/lake update doc-gen4
 
 # Build the docs
-~/.elan/bin/lake build ABCExceptions:docs
+DISABLE_EQUATIONS=1 ~/.elan/bin/lake build ABCExceptions:docs