From 29c514cb650bdbb0a8ba0705c7378fb27df707f1 Mon Sep 17 00:00:00 2001 From: JOSHCLUNE Date: Sat, 27 Sep 2025 18:32:53 -0400 Subject: [PATCH 1/9] Modify lakefile to depend on querySMT branch of fork rather than main lean-auto repo --- lake-manifest.json | 4 ++-- lakefile.lean | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 7a362a2..7e352bb 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -11,14 +11,14 @@ "inputRev": "v4.22.0", "inherited": false, "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/lean-auto.git", + {"url": "https://github.com/JOSHCLUNE/lean-auto.git", "type": "git", "subDir": null, "scope": "", "rev": "2c986b111ac17d448d81b988fc8c794375d603d7", "name": "auto", "manifestFile": "lake-manifest.json", - "inputRev": "2c986b111ac17d448d81b988fc8c794375d603d7", + "inputRev": "querySMT", "inherited": false, "configFile": "lakefile.lean"}], "name": "Duper", diff --git a/lakefile.lean b/lakefile.lean index bece81d..4aad259 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -2,7 +2,7 @@ import Lake open Lake DSL -require auto from git "https://github.com/leanprover-community/lean-auto.git"@"2c986b111ac17d448d81b988fc8c794375d603d7" +require auto from git "https://github.com/JOSHCLUNE/lean-auto.git"@"querySMT" require batteries from git "https://github.com/leanprover-community/batteries" @ "v4.22.0" package Duper { From a3f8ad49cb75caa14ceab396bc8b3aa0be1bd5d1 Mon Sep 17 00:00:00 2001 From: JOSHCLUNE Date: Sat, 27 Sep 2025 19:52:40 -0400 Subject: [PATCH 2/9] Update lean-auto --- lake-manifest.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lake-manifest.json b/lake-manifest.json index 7e352bb..4a2d706 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -15,7 +15,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "2c986b111ac17d448d81b988fc8c794375d603d7", + "rev": "280fb689c780f487fac5383dc7e5585f443ded00", "name": "auto", "manifestFile": "lake-manifest.json", "inputRev": "querySMT", From 2277a822002b15ae69c10fb6ad4ae602f0370ecd Mon Sep 17 00:00:00 2001 From: JOSHCLUNE Date: Tue, 30 Sep 2025 16:39:10 -0400 Subject: [PATCH 3/9] Update lake-manifest --- lake-manifest.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lake-manifest.json b/lake-manifest.json index 4a2d706..dff8d0f 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -15,7 +15,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "280fb689c780f487fac5383dc7e5585f443ded00", + "rev": "fc4f3b3e39350a6077cce6044f83a454138e58ef", "name": "auto", "manifestFile": "lake-manifest.json", "inputRev": "querySMT", From 27513c26c55504bf15cc14b5162071434462e272 Mon Sep 17 00:00:00 2001 From: JOSHCLUNE Date: Tue, 30 Sep 2025 16:49:00 -0400 Subject: [PATCH 4/9] Update lake-manifest --- lake-manifest.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lake-manifest.json b/lake-manifest.json index dff8d0f..50ebb32 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -15,7 +15,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "fc4f3b3e39350a6077cce6044f83a454138e58ef", + "rev": "d2d688fc76d09113523128ef7cccd1720a94a6a9", "name": "auto", "manifestFile": "lake-manifest.json", "inputRev": "querySMT", From 43faa09ee1e52d399fb7f8cf9d5b365343d8919c Mon Sep 17 00:00:00 2001 From: JOSHCLUNE Date: Wed, 1 Oct 2025 11:30:41 -0400 Subject: [PATCH 5/9] Update lake-manifest --- lake-manifest.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lake-manifest.json b/lake-manifest.json index 50ebb32..383b080 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -15,7 +15,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "d2d688fc76d09113523128ef7cccd1720a94a6a9", + "rev": "55b029550dd186622ddeb873e36e2a14d30f07a3", "name": "auto", "manifestFile": "lake-manifest.json", "inputRev": "querySMT", From 42bfedcf19ab5640cf3809b323ab2e1b04971931 Mon Sep 17 00:00:00 2001 From: JOSHCLUNE Date: Mon, 6 Oct 2025 11:15:33 -0400 Subject: [PATCH 6/9] Update lean-auto --- lake-manifest.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lake-manifest.json b/lake-manifest.json index 383b080..8783769 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -15,7 +15,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "55b029550dd186622ddeb873e36e2a14d30f07a3", + "rev": "c7dbbeaeb5d22506a346a8d9c2f86d8dd3b513a1", "name": "auto", "manifestFile": "lake-manifest.json", "inputRev": "querySMT", From e4f158b4142d5ccf9f1327dd9b77c261ac9ae85f Mon Sep 17 00:00:00 2001 From: JOSHCLUNE Date: Tue, 7 Oct 2025 08:42:47 -0400 Subject: [PATCH 7/9] Modify derivInfo so that lemmas obtained from definitional equalities aren't assumed to be from the goal --- Duper/Interface.lean | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/Duper/Interface.lean b/Duper/Interface.lean index d536851..3afcc4b 100644 --- a/Duper/Interface.lean +++ b/Duper/Interface.lean @@ -481,12 +481,16 @@ def formulasWithStringsToAutoLemmas (formulas : List (Expr × Expr × Array Name /-- Determines whether `lem`'s deriv info indicates that `lem` is part of the goal and should be included in the set of support. Note that `derivInfo` only works on lemmas generated from `formulasToAutoLemmas` or `formulasWithStringsToAutoLemmas`. In cases where the lemma was not generated from - `formulasToAutoLemmas`, `derivInfo` defaults to indicating that both `isFromGoal` and `includeInSetOfSupport` are `true`. -/ + `formulasToAutoLemmas`, `derivInfo` defaults to indicating that both `isFromGoal` and `includeInSetOfSupport` are `true`. The only exception to this + is if all leaves have exactly the form "termLikeDefEq", in which case `derivInfo` indicates that `isFromGoal` is `false`. -/ def derivInfo (lem : Auto.Lemma) : Bool × Bool := let derivLeaves := getLeavesFromDTr lem.deriv let matchesFormat := derivLeaves.any (fun l => "true, true".isPrefixOf l || "false, true".isPrefixOf l || "true, false".isPrefixOf l || "false, false".isPrefixOf l) if !matchesFormat then - (true, true) + if derivLeaves.all (fun l => l == "termLikeDefEq") then + (false, true) + else + (true, true) else let isFromGoal := derivLeaves.any (fun l => "true".isPrefixOf l) let includeInSetOfSupport := derivLeaves.any (fun l => "true, true".isPrefixOf l || "false, true".isPrefixOf l) From b0098f69427bd3db7a9d033056d049862bf997c0 Mon Sep 17 00:00:00 2001 From: JOSHCLUNE Date: Wed, 1 Apr 2026 21:56:14 -0400 Subject: [PATCH 8/9] Update lean-auto --- lake-manifest.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lake-manifest.json b/lake-manifest.json index 683e869..97e67ae 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -15,7 +15,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "c58b7f5afd2f2673db08860ecf9b57179308e63e", + "rev": "3f359a1a2ef00e1081d78f6d0e1d704bd6257588", "name": "auto", "manifestFile": "lake-manifest.json", "inputRev": "querySMT", From c65a3e772b43bcb5a6387a8675a23287d64b5373 Mon Sep 17 00:00:00 2001 From: JOSHCLUNE Date: Wed, 8 Apr 2026 19:05:13 -0400 Subject: [PATCH 9/9] Change lean-auto dependency to follow the hammer branch --- lake-manifest.json | 6 +++--- lakefile.lean | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 97e67ae..50aa0ed 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -11,14 +11,14 @@ "inputRev": "v4.29.0", "inherited": false, "configFile": "lakefile.toml"}, - {"url": "https://github.com/JOSHCLUNE/lean-auto.git", + {"url": "https://github.com/leanprover-community/lean-auto.git", "type": "git", "subDir": null, "scope": "", - "rev": "3f359a1a2ef00e1081d78f6d0e1d704bd6257588", + "rev": "7f6aec42310efd5c3311e944fff95cdabef4556a", "name": "auto", "manifestFile": "lake-manifest.json", - "inputRev": "querySMT", + "inputRev": "7f6aec42310efd5c3311e944fff95cdabef4556a", "inherited": false, "configFile": "lakefile.lean"}], "name": "Duper", diff --git a/lakefile.lean b/lakefile.lean index 2ea6ab8..b597328 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -2,7 +2,7 @@ import Lake open Lake DSL -require auto from git "https://github.com/JOSHCLUNE/lean-auto.git"@"querySMT" +require auto from git "https://github.com/leanprover-community/lean-auto.git"@"7f6aec42310efd5c3311e944fff95cdabef4556a" require batteries from git "https://github.com/leanprover-community/batteries" @ "v4.29.0" package Duper {