Add Mathlib

Changes

3 changed files (+97/-2)

• lake-manifest.json
  • @@ -1,6 +1,96 @@
    {"version": "1.2.0", "packagesDir": ".lake/packages", - "packages": [], + "packages": + [{"url": "https://github.com/leanprover-community/mathlib4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "51e6992efd06126df61a496bebf8f49482a4e129", + "name": "mathlib", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.33.0-rc2", + "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/plausible", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "123d15766ba49356c02ebad2a4462dfe12d79899", + "name": "plausible", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/LeanSearchClient", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "f5c090429dff3cf66cb65562526c9ea6e8edfbcb", + "name": "LeanSearchClient", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/import-graph", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "bb3469a87774349fe01898d8bf2fc6a1ce6411ca", + "name": "importGraph", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/ProofWidgets4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "222c58dad7706a6e7cae46c0edd65ea881d3ee27", + "name": "proofwidgets", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/aesop", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "7db8190085343afde2f5d2cdcc9bac719b6ec02c", + "name": "aesop", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/quote4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "ef42f8944eaf5b6cbfbe75d1917d824c7dd6cf33", + "name": "Qq", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/batteries", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "76e1c118b0700b4ceafe99532e887d6431625e1a", + "name": "batteries", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "scope": "leanprover", + "rev": "1319485273bf87833fa472afbcefdedecb16b45f", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.33.0-rc2", + "inherited": true, + "configFile": "lakefile.toml"}], "name": "«lean-datalog»", "lakeDir": ".lake", "fixedToolchain": false}
• lakefile.toml
  • @@ -9,3 +9,8 @@
    [[lean_exe]] name = "mutable" root = "Mutable" + + [[require]] + name = "mathlib" + scope = "leanprover-community" + rev = "v4.33.0-rc2"
• lean-toolchain
  • @@ -1,1 +1,1 @@
    - leanprover/lean4:v4.33.0-rc1 + leanprover/lean4:v4.33.0-rc2