From 4bc154d25b77cf3065c1fc961aa137a6a25e0335 Mon Sep 17 00:00:00 2001 From: JOSHCLUNE Date: Wed, 3 Dec 2025 20:43:39 -0500 Subject: [PATCH 1/3] Update to v4.26.0-rc2 --- Duper/TPTPParser/PrattParser.lean | 8 ++++---- lake-manifest.json | 8 ++++---- lakefile.lean | 4 ++-- lean-toolchain | 2 +- 4 files changed, 11 insertions(+), 11 deletions(-) diff --git a/Duper/TPTPParser/PrattParser.lean b/Duper/TPTPParser/PrattParser.lean index 00f6db3..332ebc8 100644 --- a/Duper/TPTPParser/PrattParser.lean +++ b/Duper/TPTPParser/PrattParser.lean @@ -43,7 +43,7 @@ def tokenPrefixes : Std.HashSet String := Std.HashSet.emptyWithCapacity.insertMany $ tokens.flatMap (fun t => Id.run do let mut res := [] let mut pref := "" - for c in t.data do + for c in t.toList do pref := pref.push c res := pref :: res return res @@ -88,7 +88,7 @@ def finalizeToken : TokenizerM Unit := do setStatus .default def tokenizeAux (str : String) : TokenizerM Unit := do - for char in str.data do + for char in str.toList do match ← getStatus with | .default => if char.isWhitespace then @@ -105,7 +105,7 @@ def tokenizeAux (str : String) : TokenizerM Unit := do setStatus .comment else if tokenPrefixes.contains ((← getCurrToken).push char) then addToCurrToken char - else if tokenPrefixes.contains ([char].asString) then + else if tokenPrefixes.contains (String.ofList [char]) then finalizeToken addToCurrToken char else throw $ IO.userError s!"Invalid token: {char}" @@ -493,7 +493,7 @@ partial def collectConstantsOfCmd (topLevel : Bool) (acc : Std.HashMap String Ex match t with | ⟨.ident n, as⟩ => do let acc ← as.foldlM (collectConstantsOfCmd false) acc - if n.data[0]!.isLower && n.data[0]! != '$' && !acc.contains n + if n.toList[0]!.isLower && n.toList[0]! != '$' && !acc.contains n then let ty ← as.foldlM (fun acc _ => mkArrow (mkConst `Iota) acc) diff --git a/lake-manifest.json b/lake-manifest.json index f402e39..b087dd1 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,20 +5,20 @@ "type": "git", "subDir": null, "scope": "", - "rev": "ffad3f5b7ebe1ac3e09779ec8a863a5138c1246c", + "rev": "afe9302d9243cee630b0be95322b38b90342ddbf", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "v4.25.1", + "inputRev": "v4.26.0-rc2", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/lean-auto.git", "type": "git", "subDir": null, "scope": "", - "rev": "e1ef2099e666103b85cd099a1ab5086ede15e7c0", + "rev": "9af397d7cb8c0cf62ed449ab8859a1bb3b5dc3a9", "name": "auto", "manifestFile": "lake-manifest.json", - "inputRev": "v4.25.2-hammer", + "inputRev": "v4.26.0-rc2-hammer", "inherited": false, "configFile": "lakefile.lean"}], "name": "Duper", diff --git a/lakefile.lean b/lakefile.lean index 9fbfddf..dc08c0f 100644 --- 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"@"v4.25.2-hammer" -require batteries from git "https://github.com/leanprover-community/batteries" @ "v4.25.1" +require auto from git "https://github.com/leanprover-community/lean-auto.git"@"v4.26.0-rc2-hammer" +require batteries from git "https://github.com/leanprover-community/batteries" @ "v4.26.0-rc2" package Duper { precompileModules := true diff --git a/lean-toolchain b/lean-toolchain index 370b26d..be1fbc3 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.25.2 +leanprover/lean4:v4.26.0-rc2 From 5879a6efcb09e68490c67ba4dcae569813ea4f7f Mon Sep 17 00:00:00 2001 From: JOSHCLUNE Date: Sun, 14 Dec 2025 10:30:57 -0500 Subject: [PATCH 2/3] Update to v4.26.0 --- Duper/Tests/temp2.lean | 20 ++++++++++++++++++++ lake-manifest.json | 8 ++++---- lakefile.lean | 4 ++-- lean-toolchain | 2 +- 4 files changed, 27 insertions(+), 7 deletions(-) diff --git a/Duper/Tests/temp2.lean b/Duper/Tests/temp2.lean index f00a418..d6254bf 100644 --- a/Duper/Tests/temp2.lean +++ b/Duper/Tests/temp2.lean @@ -10,6 +10,7 @@ set_option auto.native true open Lean Auto +/- @[rebind Auto.Native.solverFunc] def Auto.duperPort (lemmas inhLemmas : Array Lemma) : MetaM Expr := do let formulas ← Duper.autoLemmasToFormulas lemmas @@ -23,6 +24,7 @@ def Auto.duperPort (lemmas inhLemmas : Array Lemma) : MetaM Expr := do selFunction := none } .none +-/ inductive myType | const1 : myType @@ -115,3 +117,21 @@ theorem exists₂_comm {ι₁ ι₂ : Sort} {κ₁ : ι₁ → Sort} {κ₂ : ι₂ → Sort} {p : ∀ i₁, κ₁ i₁ → ∀ i₂, κ₂ i₂ → Prop} : (∃ i₁ j₁ i₂ j₂, p i₁ j₁ i₂ j₂) ↔ ∃ i₂ j₂ i₁ j₁, p i₁ j₁ i₂ j₂ := by duper [*] {preprocessing := no_preprocessing} + +-------------------------------------------------------------------- + +set_option trace.duper.printProof true in +set_option trace.duper.proofReconstruction true in +set_option trace.duper.saturate.debug true in +set_option trace.duper.rule.superposition true in +-- set_option trace.duper.prover.saturate true in +set_option enableSuperpositionWatchClauses true in +set_option superpositionWatchClause1 4 in +set_option superpositionWatchClause2 5 in +example (f : Nat → Prop) (h1 : ∀ x : Nat, f (x + x)) (h2 : ¬ f (1 + 1)) : False := by + duper [*] {portfolioInstance := 1} -- {preprocessing := no_preprocessing} works + +-- In the above example, Duper fails to perform an inference that it ought to be able to perform +-- First reason: superposition inference is not performed due to condition 7 +-- Second reason: After disabling the above check, Duper never reaches "Inside yC for..." line. This seems like a bug to me, but will +-- require more investigation. diff --git a/lake-manifest.json b/lake-manifest.json index b087dd1..88bce54 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,20 +5,20 @@ "type": "git", "subDir": null, "scope": "", - "rev": "afe9302d9243cee630b0be95322b38b90342ddbf", + "rev": "24241822ef9d3e7f6a3bcc53ad136e12663db8f3", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "v4.26.0-rc2", + "inputRev": "v4.26.0", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/lean-auto.git", "type": "git", "subDir": null, "scope": "", - "rev": "9af397d7cb8c0cf62ed449ab8859a1bb3b5dc3a9", + "rev": "6e66058117f0d073914c2c1f674b880537d9eb2e", "name": "auto", "manifestFile": "lake-manifest.json", - "inputRev": "v4.26.0-rc2-hammer", + "inputRev": "v4.26.0-hammer", "inherited": false, "configFile": "lakefile.lean"}], "name": "Duper", diff --git a/lakefile.lean b/lakefile.lean index dc08c0f..1a6b4f2 100644 --- 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"@"v4.26.0-rc2-hammer" -require batteries from git "https://github.com/leanprover-community/batteries" @ "v4.26.0-rc2" +require auto from git "https://github.com/leanprover-community/lean-auto.git"@"v4.26.0-hammer" +require batteries from git "https://github.com/leanprover-community/batteries" @ "v4.26.0" package Duper { precompileModules := true diff --git a/lean-toolchain b/lean-toolchain index be1fbc3..e59446d 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.26.0-rc2 +leanprover/lean4:v4.26.0 From 4970a9073727c1c71c0cb605caf81c86d3b47672 Mon Sep 17 00:00:00 2001 From: JOSHCLUNE Date: Sun, 14 Dec 2025 10:33:07 -0500 Subject: [PATCH 3/3] Update README --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 8378e70..96566d8 100644 --- 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" @ "v4.25.2" +require Duper from git "https://github.com/leanprover-community/duper.git" @ "v4.26.0" ``` 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.