Update to lean v4.11.0

leanprover-community · Oct 13, 2024 · 87d7f13 · 87d7f13
2 parents 92c1afd + ad292bd
commit 87d7f13
Show file tree

Hide file tree

Showing 7 changed files with 11 additions and 12 deletions.
diff --git a/Duper/Preprocessing.lean b/Duper/Preprocessing.lean
@@ -9,7 +9,6 @@ namespace Duper
 namespace ProverM
 open Lean
 open Meta
-open Std
 open ProverM
 open RuleM
 open SimpResult

diff --git a/Duper/ProverM.lean b/Duper/ProverM.lean
@@ -14,7 +14,6 @@ namespace Duper
 namespace ProverM
 open Lean
 open Lean.Core
-open Std
 open RuleM
 open Expr
 

diff --git a/Duper/SubsumptionTrie.lean b/Duper/SubsumptionTrie.lean
@@ -5,7 +5,6 @@ namespace Duper
 
 open Lean
 open RuleM
-open Std
 open List
 open Expr
 

diff --git a/README.md b/README.md
@@ -7,7 +7,7 @@ Duper is an automatic proof-producing theorem prover broadly similar to Isabelle
 To use Duper in an existing Lean 4 project, first add this package as a dependency. In your lakefile.lean, add:
 
 ```lean
-require Duper from git "https://github.com/leanprover-community/duper.git" @ "v0.0.15"
+require Duper from git "https://github.com/leanprover-community/duper.git" @ "v0.0.16"
 ```
 
 Then, make sure that your `lean-toolchain` file contains the same version of Lean 4 as Duper and that if your project imports [batteries](https://github.com/leanprover-community/batteries), then it uses the same version of batteries as Duper. This step is necessary because Duper depends on batteries, so errors can arise if your project attempts to import a version of batteries different from the one imported by Duper.

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -1,22 +1,24 @@
-{"version": "1.0.0",
+{"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"url": "https://github.com/leanprover-community/lean-auto.git",
    "type": "git",
    "subDir": null,
-   "rev": "22d4c2e7f2453e16b9d980cae2367d38bedf3bf5",
+   "scope": "",
+   "rev": "2b6ed7d9f86d558d94b8d9036a637395163c4fa6",
    "name": "auto",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "22d4c2e7f2453e16b9d980cae2367d38bedf3bf5",
+   "inputRev": "2b6ed7d9f86d558d94b8d9036a637395163c4fa6",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "rev": "dcea9ce8aba248927fb2ea8d5752bfe1e3fe7b44",
+   "scope": "",
+   "rev": "9c6c2d647e57b2b7a0b42dd8080c698bd33a1b6f",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.9.1",
+   "inputRev": "v4.11.0",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "Duper",

diff --git a/lakefile.lean b/lakefile.lean
@@ -2,8 +2,8 @@ import Lake
 
 open Lake DSL
 
-require auto from git "https://github.com/leanprover-community/lean-auto.git"@"22d4c2e7f2453e16b9d980cae2367d38bedf3bf5"
-require batteries from git "https://github.com/leanprover-community/batteries" @ "v4.9.1"
+require auto from git "https://github.com/leanprover-community/lean-auto.git"@"2b6ed7d9f86d558d94b8d9036a637395163c4fa6"
+require batteries from git "https://github.com/leanprover-community/batteries" @ "v4.11.0"
 
 package Duper {
   precompileModules := true

diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.9.1
+leanprover/lean4:v4.11.0