summaryrefslogtreecommitdiff
path: root/backends
diff options
context:
space:
mode:
authorSon Ho2023-07-04 14:57:51 +0200
committerSon Ho2023-07-04 14:57:51 +0200
commit87d6f6c7c90bf7b427397d6bd2e2c70d610678e3 (patch)
treece6f570b8916db1877e505f719461241bafaed0d /backends
parent4fd17e4bb91eb46d4704643dfbfbbf0874837b07 (diff)
Reorganize the Lean tests
Diffstat (limited to '')
-rw-r--r--backends/lean/Base.lean1
-rw-r--r--backends/lean/lake-manifest.json10
-rw-r--r--backends/lean/lean-toolchain2
3 files changed, 9 insertions, 4 deletions
diff --git a/backends/lean/Base.lean b/backends/lean/Base.lean
index 6e9ff873..1f8cbc8e 100644
--- a/backends/lean/Base.lean
+++ b/backends/lean/Base.lean
@@ -1,4 +1,3 @@
import Base.Primitives
import Base.Diverge
-import Base.TestTactics
import Base.Arith
diff --git a/backends/lean/lake-manifest.json b/backends/lean/lake-manifest.json
index e5d362fc..40eb1682 100644
--- a/backends/lean/lake-manifest.json
+++ b/backends/lean/lake-manifest.json
@@ -2,9 +2,15 @@
"packagesDir": "lake-packages",
"packages":
[{"git":
+ {"url": "https://github.com/EdAyers/ProofWidgets4",
+ "subDir?": null,
+ "rev": "c43db94a8f495dad37829e9d7ad65483d68c86b8",
+ "name": "proofwidgets",
+ "inputRev?": "v0.0.11"}},
+ {"git":
{"url": "https://github.com/leanprover-community/mathlib4.git",
"subDir?": null,
- "rev": "cdb1b898e4317567699181f27533182046ebc544",
+ "rev": "4f103b3696795c62e76fb89d177efb91c29afdf5",
"name": "mathlib",
"inputRev?": null}},
{"git":
@@ -22,6 +28,6 @@
{"git":
{"url": "https://github.com/leanprover/std4",
"subDir?": null,
- "rev": "6932c4ea52914dc6b0488944e367459ddc4d01a6",
+ "rev": "e68aa8f5fe47aad78987df45f99094afbcb5e936",
"name": "std",
"inputRev?": "main"}}]}
diff --git a/backends/lean/lean-toolchain b/backends/lean/lean-toolchain
index 1211e372..42e7d786 100644
--- a/backends/lean/lean-toolchain
+++ b/backends/lean/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2023-05-31 \ No newline at end of file
+leanprover/lean4:nightly-2023-06-20 \ No newline at end of file