Skip to content

Commit

Permalink
bump Mathlib; and copy lean-toolchain before testing
Browse files Browse the repository at this point in the history
  • Loading branch information
kim-em committed Jan 12, 2024
1 parent ac9ff73 commit 7df9e30
Show file tree
Hide file tree
Showing 2 changed files with 16 additions and 6 deletions.
1 change: 1 addition & 0 deletions test.sh
Original file line number Diff line number Diff line change
Expand Up @@ -39,4 +39,5 @@ for infile in $IN_DIR/*.in; do
done

# Run the Mathlib tests
cp lean-toolchain test/Mathlib/
cd test/Mathlib/ && ./test.sh
21 changes: 15 additions & 6 deletions test/Mathlib/lake-manifest.json
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
[{"url": "https://github.com/leanprover/std4",
"type": "git",
"subDir": null,
"rev": "ee49cf8fada1bf5a15592c399a925c401848227f",
"rev": "0b2e962a80b98df1c6455f8ae11f2bd16809067c",
"name": "std",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
Expand All @@ -13,7 +13,7 @@
{"url": "https://github.com/leanprover-community/quote4",
"type": "git",
"subDir": null,
"rev": "ccba5d35d07a448fab14c0e391c8105df6e2564c",
"rev": "1c88406514a636d241903e2e288d21dc6d861e01",
"name": "Qq",
"manifestFile": "lake-manifest.json",
"inputRev": "master",
Expand All @@ -22,7 +22,7 @@
{"url": "https://github.com/leanprover-community/aesop",
"type": "git",
"subDir": null,
"rev": "69404390bdc1de946bf0a2e51b1a69f308e56d7a",
"rev": "2ae78a474ddf0a39bc2afb9f9f284d2e64f48a70",
"name": "aesop",
"manifestFile": "lake-manifest.json",
"inputRev": "master",
Expand All @@ -31,10 +31,10 @@
{"url": "https://github.com/leanprover-community/ProofWidgets4",
"type": "git",
"subDir": null,
"rev": "bf61e90de075abfa27f638922e7aafafdce77c44",
"rev": "8dd18350791c85c0fc9adbd6254c94a81d260d35",
"name": "proofwidgets",
"manifestFile": "lake-manifest.json",
"inputRev": "v0.0.24-pre2",
"inputRev": "v0.0.25",
"inherited": true,
"configFile": "lakefile.lean"},
{"url": "https://github.com/leanprover/lean4-cli",
Expand All @@ -46,10 +46,19 @@
"inputRev": "main",
"inherited": true,
"configFile": "lakefile.lean"},
{"url": "https://github.com/leanprover-community/import-graph.git",
"type": "git",
"subDir": null,
"rev": "6f42d2822aba47eb690ed98c508a23e6f0becce2",
"name": "importGraph",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
"inherited": true,
"configFile": "lakefile.lean"},
{"url": "https://github.com/leanprover-community/mathlib4",
"type": "git",
"subDir": null,
"rev": "58eef79b1520d17ff085f58b599690c112a47e6b",
"rev": "0533bf2b33a502d71fdcd6599588f087b5c3a1d9",
"name": "mathlib",
"manifestFile": "lake-manifest.json",
"inputRev": "master",
Expand Down

0 comments on commit 7df9e30

Please sign in to comment.