From 57e92011322ccb6fa25cbb2e8e74c271daeefce4 Mon Sep 17 00:00:00 2001 From: JOSHCLUNE Date: Thu, 19 Feb 2026 00:01:59 -0500 Subject: [PATCH 1/2] Update to v4.28.0 --- HammerCore/lake-manifest.json | 16 ++++++++-------- HammerCore/lakefile.lean | 4 ++-- HammerCore/lean-toolchain | 2 +- README.md | 16 +++++++++------- lake-manifest.json | 24 ++++++++++++------------ lakefile.toml | 4 ++-- lean-toolchain | 2 +- 7 files changed, 35 insertions(+), 33 deletions(-) diff --git a/HammerCore/lake-manifest.json b/HammerCore/lake-manifest.json index 70fd032..e843c99 100644 --- a/HammerCore/lake-manifest.json +++ b/HammerCore/lake-manifest.json @@ -5,40 +5,40 @@ "type": "git", "subDir": null, "scope": "", - "rev": "03488acde08efdb914d9cacaf72618fd39c66701", + "rev": "4aa43d4e9802737dc7dbefd92a247e2a62f9ce81", "name": "Duper", "manifestFile": "lake-manifest.json", - "inputRev": "v4.27.0", + "inputRev": "v4.28.0", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "", - "rev": "cb837cc26236ada03c81837bebe0acd9c70ced7d", + "rev": "f642a64c76df8ba9cb53dba3b919425a0c2aeaf1", "name": "aesop", "manifestFile": "lake-manifest.json", - "inputRev": "v4.27.0", + "inputRev": "v4.28.0", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, "scope": "", - "rev": "b25b36a7caf8e237e7d1e6121543078a06777c8a", + "rev": "495c008c3e3f4fb4256ff5582ddb3abf3198026f", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "v4.27.0", + "inputRev": "v4.28.0", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/lean-auto.git", "type": "git", "subDir": null, "scope": "", - "rev": "7e8f3ab431d4790bd803e467d661b1be2522bfd3", + "rev": "1f8a3b2f31366ec7da2a160e634004c52be6631e", "name": "auto", "manifestFile": "lake-manifest.json", - "inputRev": "v4.27.0-hammer", + "inputRev": "v4.28.0-hammer", "inherited": true, "configFile": "lakefile.lean"}], "name": "HammerCore", diff --git a/HammerCore/lakefile.lean b/HammerCore/lakefile.lean index 278d08a..fe32326 100644 --- a/HammerCore/lakefile.lean +++ b/HammerCore/lakefile.lean @@ -1,9 +1,9 @@ import Lake open Lake DSL -require «aesop» from git "https://github.com/leanprover-community/aesop" @ "v4.27.0" +require «aesop» from git "https://github.com/leanprover-community/aesop" @ "v4.28.0" -require «Duper» from git "https://github.com/leanprover-community/duper.git" @ "v4.27.0" +require «Duper» from git "https://github.com/leanprover-community/duper.git" @ "v4.28.0" package HammerCore { precompileModules := true diff --git a/HammerCore/lean-toolchain b/HammerCore/lean-toolchain index 5249182..4c685fa 100644 --- a/HammerCore/lean-toolchain +++ b/HammerCore/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.27.0 +leanprover/lean4:v4.28.0 diff --git a/README.md b/README.md index 9d94dbc..a94244d 100644 --- a/README.md +++ b/README.md @@ -2,36 +2,38 @@ LeanHammer is an automated reasoning tool for Lean that brings together multiple proof search and reconstruction techniques and combines them into one tool. The `hammer` tactic provided by LeanHammer uses a variety of techniques to search for a proof of the current goal, then constructs a suggestion for a tactic script which can replace the `hammer` invocation. -LeanHammer is in an early stage of its development and is therefore subject to breaking changes. There are currently versions of the hammer that are compatible with the stable versions of Lean from `v4.20.0` through `v4.27.0` (and the corresponding versions of Mathlib). +LeanHammer is in an early stage of its development and is therefore subject to breaking changes. There are currently versions of the hammer that are compatible with the stable versions of Lean from `v4.20.0` through `v4.28.0` (and the corresponding versions of Mathlib). + +**Note:** Although the LeanHammer repository has been updated to support `v4.28.0`, the LeanPremise server which LeanHammer uses for premise selection is still being updated from `v4.27.0` to `v4.28.0`. During the intermediate period while this update is occurring, premise selection may be slower and less accurate than usual. This note will be removed once the server has been fully updated to `v4.28.0`. Pull requests and issues are welcome. ## Adding LeanHammer to Your Project -To add LeanHammer for `v4.27.0` to an existing project with a `lakefile.toml` file, replace the Mathlib dependency in `lakefile.toml` with the following: +To add LeanHammer for `v4.28.0` to an existing project with a `lakefile.toml` file, replace the Mathlib dependency in `lakefile.toml` with the following: ```toml [[require]] name = "Hammer" git = "https://github.com/JOSHCLUNE/LeanHammer" -rev = "v4.27.0" +rev = "v4.28.0" [[require]] name = "mathlib" scope = "leanprover-community" -rev = "v4.27.0" +rev = "v4.28.0" ``` The file `lean-toolchain` should contain the following: ``` -leanprover/lean4:v4.27.0 +leanprover/lean4:v4.28.0 ``` If you have a project with a `lakefile.lean` instead of `lakefile.toml`, you can use this instead: ```lean -require Hammer from git "https://github.com/JOSHCLUNE/LeanHammer" @ "v4.27.0" +require Hammer from git "https://github.com/JOSHCLUNE/LeanHammer" @ "v4.28.0" -require mathlib from git "https://github.com/leanprover-community/mathlib4.git" @ "v4.27.0" +require mathlib from git "https://github.com/leanprover-community/mathlib4.git" @ "v4.28.0" ``` Then use `lake update` to fetch the hammer and the corresponding versions of Lean and Mathlib. This also retrieves the Zipperposition executable that comes with LeanHammer. (This executable will be stored in the existing project's `.lake` directory.) The following example should then compile without any warnings or errors: diff --git a/lake-manifest.json b/lake-manifest.json index 0d04ea4..11af3eb 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -12,60 +12,60 @@ "type": "git", "subDir": null, "scope": "", - "rev": "bd58c9efe2086d56ca361807014141a860ddbf8c", + "rev": "b8f98e9087e02c8553945a2c5abf07cec8e798c3", "name": "Qq", "manifestFile": "lake-manifest.json", - "inputRev": "v4.27.0", + "inputRev": "v4.28.0", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/hanwenzhu/premise-selection", "type": "git", "subDir": null, "scope": "", - "rev": "d0f19843efc9f3632325bc5eb45b1e924959dc00", + "rev": "546741e1bacbe8779cbb03a9cb7254bc43336442", "name": "«premise-selection»", "manifestFile": "lake-manifest.json", - "inputRev": "v4.27.0", + "inputRev": "v4.28.0", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/duper.git", "type": "git", "subDir": null, "scope": "", - "rev": "03488acde08efdb914d9cacaf72618fd39c66701", + "rev": "4aa43d4e9802737dc7dbefd92a247e2a62f9ce81", "name": "Duper", "manifestFile": "lake-manifest.json", - "inputRev": "v4.27.0", + "inputRev": "v4.28.0", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "", - "rev": "cb837cc26236ada03c81837bebe0acd9c70ced7d", + "rev": "f642a64c76df8ba9cb53dba3b919425a0c2aeaf1", "name": "aesop", "manifestFile": "lake-manifest.json", - "inputRev": "v4.27.0", + "inputRev": "v4.28.0", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, "scope": "", - "rev": "b25b36a7caf8e237e7d1e6121543078a06777c8a", + "rev": "495c008c3e3f4fb4256ff5582ddb3abf3198026f", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "v4.27.0", + "inputRev": "v4.28.0", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/lean-auto.git", "type": "git", "subDir": null, "scope": "", - "rev": "7e8f3ab431d4790bd803e467d661b1be2522bfd3", + "rev": "1f8a3b2f31366ec7da2a160e634004c52be6631e", "name": "auto", "manifestFile": "lake-manifest.json", - "inputRev": "v4.27.0-hammer", + "inputRev": "v4.28.0-hammer", "inherited": true, "configFile": "lakefile.lean"}], "name": "Hammer", diff --git a/lakefile.toml b/lakefile.toml index e947900..8e2547d 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -6,12 +6,12 @@ defaultTargets = ["Hammer"] [[require]] name = "«premise-selection»" git = "https://github.com/hanwenzhu/premise-selection" -rev = "v4.27.0" +rev = "v4.28.0" [[require]] name = "Qq" git = "https://github.com/leanprover-community/quote4.git" -rev = "v4.27.0" +rev = "v4.28.0" [[require]] name = "HammerCore" diff --git a/lean-toolchain b/lean-toolchain index 5249182..4c685fa 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.27.0 +leanprover/lean4:v4.28.0 From 5a236636d5f9f19399a22ee0443b72bf65c23a8b Mon Sep 17 00:00:00 2001 From: JOSHCLUNE Date: Thu, 19 Feb 2026 00:02:40 -0500 Subject: [PATCH 2/2] Update README --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index a94244d..5e621a9 100644 --- a/README.md +++ b/README.md @@ -4,7 +4,7 @@ LeanHammer is an automated reasoning tool for Lean that brings together multiple LeanHammer is in an early stage of its development and is therefore subject to breaking changes. There are currently versions of the hammer that are compatible with the stable versions of Lean from `v4.20.0` through `v4.28.0` (and the corresponding versions of Mathlib). -**Note:** Although the LeanHammer repository has been updated to support `v4.28.0`, the LeanPremise server which LeanHammer uses for premise selection is still being updated from `v4.27.0` to `v4.28.0`. During the intermediate period while this update is occurring, premise selection may be slower and less accurate than usual. This note will be removed once the server has been fully updated to `v4.28.0`. +***Note:** Although the LeanHammer repository has been updated to support `v4.28.0`, the LeanPremise server which LeanHammer uses for premise selection is still being updated from `v4.27.0` to `v4.28.0`. During the intermediate period while this update is occurring, premise selection may be slower and less accurate than usual. This note will be removed once the server has been fully updated to `v4.28.0`.* Pull requests and issues are welcome.