Skip to content

Update to v4.27.0 #29

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
JOSHCLUNE merged 1 commit into from
Jan 27, 2026
Merged

Update to v4.27.0 #29

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 8 additions & 8 deletions HammerCore/lake-manifest.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,40 +5,40 @@
"type": "git",
"subDir": null,
"scope": "",
"rev": "93e949f61679a9546d543a604f3f88b2a5eef262",
"rev": "03488acde08efdb914d9cacaf72618fd39c66701",
"name": "Duper",
"manifestFile": "lake-manifest.json",
"inputRev": "v4.26.0",
"inputRev": "v4.27.0",
"inherited": false,
"configFile": "lakefile.lean"},
{"url": "https://github.com/leanprover-community/aesop",
"type": "git",
"subDir": null,
"scope": "",
"rev": "2f6d238744c4cb07fdc91240feaf5d4221a27931",
"rev": "cb837cc26236ada03c81837bebe0acd9c70ced7d",
"name": "aesop",
"manifestFile": "lake-manifest.json",
"inputRev": "v4.26.0",
"inputRev": "v4.27.0",
"inherited": false,
"configFile": "lakefile.toml"},
{"url": "https://github.com/leanprover-community/batteries",
"type": "git",
"subDir": null,
"scope": "",
"rev": "24241822ef9d3e7f6a3bcc53ad136e12663db8f3",
"rev": "b25b36a7caf8e237e7d1e6121543078a06777c8a",
"name": "batteries",
"manifestFile": "lake-manifest.json",
"inputRev": "v4.26.0",
"inputRev": "v4.27.0",
"inherited": true,
"configFile": "lakefile.toml"},
{"url": "https://github.com/leanprover-community/lean-auto.git",
"type": "git",
"subDir": null,
"scope": "",
"rev": "6e66058117f0d073914c2c1f674b880537d9eb2e",
"rev": "7e8f3ab431d4790bd803e467d661b1be2522bfd3",
"name": "auto",
"manifestFile": "lake-manifest.json",
"inputRev": "v4.26.0-hammer",
"inputRev": "v4.27.0-hammer",
"inherited": true,
"configFile": "lakefile.lean"}],
"name": "HammerCore",
Expand Down
4 changes: 2 additions & 2 deletions HammerCore/lakefile.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,9 +1,9 @@
import Lake
open Lake DSL

require «aesop» from git "https://github.com/leanprover-community/aesop" @ "v4.26.0"
require «aesop» from git "https://github.com/leanprover-community/aesop" @ "v4.27.0"

require «Duper» from git "https://github.com/leanprover-community/duper.git" @ "v4.26.0"
require «Duper» from git "https://github.com/leanprover-community/duper.git" @ "v4.27.0"

package HammerCore {
precompileModules := true
Expand Down
2 changes: 1 addition & 1 deletion HammerCore/lean-toolchain
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1 +1 @@
leanprover/lean4:v4.26.0
leanprover/lean4:v4.27.0
16 changes: 9 additions & 7 deletions README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.26.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.27.0` (and the corresponding versions of Mathlib).

***Note:** Although the LeanHammer repository has been updated to support `v4.27.0`, the LeanPremise server which LeanHammer uses for premise selection is still being updated from `v4.26.0` to `v4.27.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.27.0`.*

Pull requests and issues are welcome.

## Adding LeanHammer to Your Project

To add LeanHammer for v4.26.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.27.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.26.0"
rev = "v4.27.0"

[[require]]
name = "mathlib"
scope = "leanprover-community"
rev = "v4.26.0"
rev = "v4.27.0"
```
The file `lean-toolchain` should contain the following:
```
leanprover/lean4:v4.26.0
leanprover/lean4:v4.27.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.26.0"
require Hammer from git "https://github.com/JOSHCLUNE/LeanHammer" @ "v4.27.0"

require mathlib from git "https://github.com/leanprover-community/mathlib4.git" @ "v4.26.0"
require mathlib from git "https://github.com/leanprover-community/mathlib4.git" @ "v4.27.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:
Expand Down
24 changes: 12 additions & 12 deletions lake-manifest.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,60 +12,60 @@
"type": "git",
"subDir": null,
"scope": "",
"rev": "9312503909aa8e8bb392530145cc1677a6298574",
"rev": "bd58c9efe2086d56ca361807014141a860ddbf8c",
"name": "Qq",
"manifestFile": "lake-manifest.json",
"inputRev": "v4.26.0",
"inputRev": "v4.27.0",
"inherited": false,
"configFile": "lakefile.toml"},
{"url": "https://github.com/hanwenzhu/premise-selection",
"type": "git",
"subDir": null,
"scope": "",
"rev": "d648fd5130a972d609ef846c0fa3e853753638bf",
"rev": "d0f19843efc9f3632325bc5eb45b1e924959dc00",
"name": "«premise-selection»",
"manifestFile": "lake-manifest.json",
"inputRev": "v4.26.0",
"inputRev": "v4.27.0",
"inherited": false,
"configFile": "lakefile.toml"},
{"url": "https://github.com/leanprover-community/duper.git",
"type": "git",
"subDir": null,
"scope": "",
"rev": "93e949f61679a9546d543a604f3f88b2a5eef262",
"rev": "03488acde08efdb914d9cacaf72618fd39c66701",
"name": "Duper",
"manifestFile": "lake-manifest.json",
"inputRev": "v4.26.0",
"inputRev": "v4.27.0",
"inherited": true,
"configFile": "lakefile.lean"},
{"url": "https://github.com/leanprover-community/aesop",
"type": "git",
"subDir": null,
"scope": "",
"rev": "2f6d238744c4cb07fdc91240feaf5d4221a27931",
"rev": "cb837cc26236ada03c81837bebe0acd9c70ced7d",
"name": "aesop",
"manifestFile": "lake-manifest.json",
"inputRev": "v4.26.0",
"inputRev": "v4.27.0",
"inherited": true,
"configFile": "lakefile.toml"},
{"url": "https://github.com/leanprover-community/batteries",
"type": "git",
"subDir": null,
"scope": "",
"rev": "24241822ef9d3e7f6a3bcc53ad136e12663db8f3",
"rev": "b25b36a7caf8e237e7d1e6121543078a06777c8a",
"name": "batteries",
"manifestFile": "lake-manifest.json",
"inputRev": "v4.26.0",
"inputRev": "v4.27.0",
"inherited": true,
"configFile": "lakefile.toml"},
{"url": "https://github.com/leanprover-community/lean-auto.git",
"type": "git",
"subDir": null,
"scope": "",
"rev": "6e66058117f0d073914c2c1f674b880537d9eb2e",
"rev": "7e8f3ab431d4790bd803e467d661b1be2522bfd3",
"name": "auto",
"manifestFile": "lake-manifest.json",
"inputRev": "v4.26.0-hammer",
"inputRev": "v4.27.0-hammer",
"inherited": true,
"configFile": "lakefile.lean"}],
"name": "Hammer",
Expand Down
4 changes: 2 additions & 2 deletions lakefile.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,12 +6,12 @@ defaultTargets = ["Hammer"]
[[require]]
name = "«premise-selection»"
git = "https://github.com/hanwenzhu/premise-selection"
rev = "v4.26.0"
rev = "v4.27.0"

[[require]]
name = "Qq"
git = "https://github.com/leanprover-community/quote4.git"
rev = "v4.26.0"
rev = "v4.27.0"

[[require]]
name = "HammerCore"
Expand Down
2 changes: 1 addition & 1 deletion lean-toolchain
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1 +1 @@
leanprover/lean4:v4.26.0
leanprover/lean4:v4.27.0