LeanHammer

Stream: general

[Thomas Zhu]

This is a discussion thread for #announce > LeanHammer. Please don't hesitate to ask question or give feedback about our tool!

For bug / performance reports, please also don't hesitate to open an issue at https://github.com/JOSHCLUNE/LeanHammer!

[Riccardo Brasca]

Thanks for all the work!! What is the typical use case and how does it overlap with grind? (Sorry if everything is explained in the paper, I will read it tomorrow)

[Yaël Dillies]

I just tried installing the hammer in Toric and it fails with the following obscure error:

$ lake update
info: Hammer: cloning https://github.com/JOSHCLUNE/LeanHammer
info: mathlib: checking out revision 'db52f0992d294d2273c2eff06bc4cfac13460b0c'
info: toolchain not updated; already up-to-date
info: Qq: URL has changed; deleting '/workspace/Toric/.lake/packages/Qq' and cloning again
info: Qq: cloning https://github.com/leanprover-community/quote4.git
info: Qq: checking out revision '2865ea099ab1dd8d6fc93381d77a4ac87a85527a'
info: premise-selection: cloning https://github.com/hanwenzhu/premise-selection
info: premise-selection: checking out revision 'd81f961f78ddfcb769e652da0c0e3923a9eab8e8'
info: Duper: cloning https://github.com/leanprover-community/duper.git
info: Duper: checking out revision '7179853dbd9b66e18258c438626e0704833923cf'
info: aesop: checking out revision '9264d548cf1ccf0ba454b82f931f44c37c299fc1'
info: batteries: checking out revision 'cb53cd3f2958ee503f97ea6162929cabaf96bde9'
info: auto: cloning https://github.com/leanprover-community/lean-auto.git
info: auto: checking out revision '9a558f49f4997d19d69e50a90c2bbc98faff2476'
info: mathlib: running post-update hooks
installing leantar 0.1.15
  % Total    % Received % Xferd  Average Speed   Time    Time     Time  Current
                                 Dload  Upload   Total   Spent    Left  Speed
  0     0    0     0    0     0      0      0 --:--:-- --:--:-- --:--:--     0
100 1075k  100 1075k    0     0  2962k      0 --:--:-- --:--:-- --:--:-- 2962k

Mathlib repository: leanprover-community/mathlib4
Attempting to download 6841 file(s) from leanprover-community/mathlib4 cache
Downloaded: 160 file(s) [attempted 6841/6841 = 100%] (2% success)
Warning: some files were not found in the cache.
This usually means that your local checkout of mathlib4 has diverged from upstream.
If you push your commits to a branch of the mathlib4 repository, CI will build the oleans and they will be available later.
Alternatively, if you already have pushed your commits to a branch, this may mean the CI build has failed part-way through building.
Decompressing 160 file(s)
Unpacked in 114 ms
Completed successfully!
info: auto: running post-update hooks
error: external command 'unzip' exited with code 255
error: auto: failed to download/setup `zipperposition`

[Thomas Zhu]

Riccardo Brasca said:

Thanks for all the work!! What is the typical use case and how does it overlap with grind? (Sorry if everything is explained in the paper, I will read it tomorrow)

Hi! Currently the typical use case will be 1-2 line short proofs (eg a have statement) that may depend on some previously defined lemmas. On a UI level, grind is a similar tool, but the technical implementations are completely different, and my current understanding is that grind does not yet have a premise selector while we do have one. In the long term, it may be possible to integrate grind into LeanHammer or integrate LeanHammer's premise selector into grind once both tools are ready/performant. (I believe the relationship with grind is not covered in the paper.)

[Thomas Zhu]

Yaël Dillies said:

I just tried installing the hammer in Toric and it fails with the following obscure error:

$ lake update
info: Hammer: cloning https://github.com/JOSHCLUNE/LeanHammer
info: mathlib: checking out revision 'db52f0992d294d2273c2eff06bc4cfac13460b0c'
info: toolchain not updated; already up-to-date
info: Qq: URL has changed; deleting '/workspace/Toric/.lake/packages/Qq' and cloning again
info: Qq: cloning https://github.com/leanprover-community/quote4.git
info: Qq: checking out revision '2865ea099ab1dd8d6fc93381d77a4ac87a85527a'
info: premise-selection: cloning https://github.com/hanwenzhu/premise-selection
info: premise-selection: checking out revision 'd81f961f78ddfcb769e652da0c0e3923a9eab8e8'
info: Duper: cloning https://github.com/leanprover-community/duper.git
info: Duper: checking out revision '7179853dbd9b66e18258c438626e0704833923cf'
info: aesop: checking out revision '9264d548cf1ccf0ba454b82f931f44c37c299fc1'
info: batteries: checking out revision 'cb53cd3f2958ee503f97ea6162929cabaf96bde9'
info: auto: cloning https://github.com/leanprover-community/lean-auto.git
info: auto: checking out revision '9a558f49f4997d19d69e50a90c2bbc98faff2476'
info: mathlib: running post-update hooks
installing leantar 0.1.15
  % Total    % Received % Xferd  Average Speed   Time    Time     Time  Current
                                 Dload  Upload   Total   Spent    Left  Speed
  0     0    0     0    0     0      0      0 --:--:-- --:--:-- --:--:--     0
100 1075k  100 1075k    0     0  2962k      0 --:--:-- --:--:-- --:--:-- 2962k

Mathlib repository: leanprover-community/mathlib4
Attempting to download 6841 file(s) from leanprover-community/mathlib4 cache
Downloaded: 160 file(s) [attempted 6841/6841 = 100%] (2% success)
Warning: some files were not found in the cache.
This usually means that your local checkout of mathlib4 has diverged from upstream.
If you push your commits to a branch of the mathlib4 repository, CI will build the oleans and they will be available later.
Alternatively, if you already have pushed your commits to a branch, this may mean the CI build has failed part-way through building.
Decompressing 160 file(s)
Unpacked in 114 ms
Completed successfully!
info: auto: running post-update hooks
error: external command 'unzip' exited with code 255
error: auto: failed to download/setup `zipperposition`

You may need to install 'unzip' in the command line. LeanHammer retrieves zipperposition's binary executable and unzips the file to run it.

[Thomas Zhu]

Also, @Yaël Dillies I found there is a name conflict with v4.21.0-rc3 that prevents LeanHammer from being built. I will look into this shortly (I believe this is easily fixable), but currently it might only work with all dependencies fixed at v4.20.0. Thank you!

[Sophie Morel]

I'm excited to try playing with it as soon as that conflict is fixed!

[Yaël Dillies]

When all you have is a hammer, everything looks like a :snail:

[Sophie Morel]

Nooooo I cry when people hurt snails... :sob:

[Yaël Dillies]

Ahahah, I was more thinking "everything else than the hammer is so slow"

[Justin Asher]

Just wanted to say that this looks super neat, and I am excited to play around with it for more general automated theorem proving tasks! Excited to see how this project evolves.

[Thomas Zhu]

@Sophie Morel @Yaël Dillies I pushed a temporary bump to LeanHammer at the branch temp-v4.21.0-rc3, which has a toolchain bump to v4.21.0-rc3. To use it add

[[require]]
name = "Hammer"
git = "https://github.com/JOSHCLUNE/LeanHammer"
rev = "temp-v4.21.0-rc3"

to your lakefile.toml.

This branch is to make the hammer at least compile on v4.21.0-rc3, so it might not be representative of the final expected performance, and I still encourage to fix dependencies at v4.20.0 if possible (I realize this is not always possible if e.g. you are porting theorems between Mathlib and Toric). We will wait until the proper tests are done/merged until the main branch of LeanHammer is bumped. In the meantime, if you run hammer on temp-v4.21.0-rc3, then you will likely see a warning

Found 2808 unindexed premises in the environment, which exceeds the maximum number of new premises (2048). Discarding premises beyond this limit

This is expected, because our premise selection server is still running on theorems extracted from v4.20.0. This also impacts Hammer's performance and speed by a little, which is why v4.20.0 is preferred for now.

[Jared green]

can Canonical and egg be integrated in the proof search?

[Asei Inoue]

nice! I think Mathlib should have lean hammer!

[Thomas Zhu]

Jared green said:

can Canonical and egg be integrated in the proof search?

My understanding is that they could be, but I am not qualified to give a good answer. LeanHammer is basically a new neural premise selector suggesting premises (lemmas/definitions) for proof search tactics. Currently the "proof search" part is done by Aesop + Lean-auto + Zipperposition + Duper, but in principle it is possible to use any proof search algorithm that accepts a list of premises, like grind, Canonical, and egg, and it would be interesting to see if they offer better performance (my intuition is they absolutely will solve some interesting theorems that LeanHammer currently can't!). In the short term we are more focused on extending to cvc5 + LeanSMT though. Conversely, you may also imagine generalizing the premise selection part from LeanHammer and integrating premise selection into these tactics.

[Thomas Zhu]

Asei Inoue said:

nice! I think Mathlib should have lean hammer!

Yes, the (long term) hope is that LeanHammer becomes a dependency of Mathlib!

[Kim Morrison]

@Thomas Zhu, could you fix the repository / package naming?

Adding require "JOSHCLUNE" / "LeanHammer" @ git "temp-v4.21.0-rc3" to the Mathlib lakefile, running lake update Hammer (or lake update LeanHammer) gives the error message

% lake update Hammer
info: JOSHCLUNE/Hammer: cloning https://github.com/JOSHCLUNE/LeanHammer
info: JOSHCLUNE/Hammer: checking out revision '4d987148ef9517838b7676ed5ab0d5021faa9dd2'
info: toolchain not updated; already up-to-date
error: mathlib: package 'Hammer' was required as 'LeanHammer'

I understand that the README advises using

require Hammer from git "https://github.com/JOSHCLUNE/LeanHammer" @ "temp-v4.21.0-rc3"

instead (which works), but if we're investigating how to get this installed in Mathlib, I would like this fixed regardless. :-)

[Kim Morrison]

Relatedly, could you ensure that the lake-manifest.json snippet:

  {"url": "https://github.com/hanwenzhu/premise-selection",
   "type": "git",
   "subDir": null,
   "scope": "",
   "rev": "d81f961f78ddfcb769e652da0c0e3923a9eab8e8",
   "name": "«premise-selection»",
   "manifestFile": "lake-manifest.json",
   "inputRev": "v4.20.0",
   "inherited": true,
   "configFile": "lakefile.toml"},

does not have french quotes? I know this is meant to be supported, but in practice not having plain ASCII names is a nightmare.

[Kim Morrison]

The first time I'm running hammer, I just get a yellow bar that persists a long time (about a minute so far). I'm _guessing_ that it is doing some sort of initialization, but I don't know.

Can you make sure that if it really is doing something, it prints an info message saying this is happening?

[Siddhartha Gadgil]

Thanks for this brilliant tool. I intend to use it a lot. There are instructions for using the cloud-based service and for training locally. How do I host locally the premise selector (so avoid overloading the cloud service) but use the trainining data that the cloud service uses?

[Thomas Zhu]

Kim Morrison said:

Thomas Zhu, could you fix the repository / package naming?

Adding require "JOSHCLUNE" / "LeanHammer" @ git "temp-v4.21.0-rc3" to the Mathlib lakefile, running lake update Hammer (or lake update LeanHammer) gives the error message

% lake update Hammer
info: JOSHCLUNE/Hammer: cloning https://github.com/JOSHCLUNE/LeanHammer
info: JOSHCLUNE/Hammer: checking out revision '4d987148ef9517838b7676ed5ab0d5021faa9dd2'
info: toolchain not updated; already up-to-date
error: mathlib: package 'Hammer' was required as 'LeanHammer'

I understand that the README advises using

require Hammer from git "https://github.com/JOSHCLUNE/LeanHammer" @ "temp-v4.21.0-rc3"

instead (which works), but if we're investigating how to get this installed in Mathlib, I would like this fixed regardless. :-)

Hi Kim, I think require "JOSHCLUNE" / "Hammer" @ git "temp-v4.21.0-rc3" works. I am not very familiar with this: does lake automatically resolve "JOSHCLUNE" / "Hammer" to the GitHub repo JOSHCLUNE/LeanHammer based on the package name Hammer? If this is a stable solution, then I think I can update README to use this notation instead.

[Thomas Zhu]

Kim Morrison said:

Relatedly, could you ensure that the lake-manifest.json snippet:

  {"url": "https://github.com/hanwenzhu/premise-selection",
   "type": "git",
   "subDir": null,
   "scope": "",
   "rev": "d81f961f78ddfcb769e652da0c0e3923a9eab8e8",
   "name": "«premise-selection»",
   "manifestFile": "lake-manifest.json",
   "inputRev": "v4.20.0",
   "inherited": true,
   "configFile": "lakefile.toml"},

does not have french quotes? I know this is meant to be supported, but in practice not having plain ASCII names is a nightmare.

I am not sure how to make lake update not output a name with French quotes, when there is a - in the package name. Is the intended solution to remove - from the package name of premise-selection? (A similar scenario holds for doc-gen4, e.g. here)

[Thomas Zhu]

Kim Morrison said:

The first time I'm running hammer, I just get a yellow bar that persists a long time (about a minute so far). I'm _guessing_ that it is doing some sort of initialization, but I don't know.

Can you make sure that if it really is doing something, it prints an info message saying this is happening?

I am pretty sure it really is doing something. The reason for the long init time is:

• The premise selection server stores information about Mathlib on v4.20.0, so here it tries to embed the new premises added to Mathlib between v4.20.0 and the current master. The result is cached by the server so the wait time will be shorter in the next initialization.
• In order to embed these new premises, Lean also needs to serialize the new premises into strings, which takes a little time. The result is cached per session, so the second hammer call will be shorter.

The suggestion to add an info message to say something is happening makes sense, thanks! I will put that on my to-do list.

[Thomas Zhu]

Siddhartha Gadgil said:

Thanks for this brilliant tool. I intend to use it a lot. There are instructions for using the cloud-based service and for training locally. How do I host locally the premise selector (so avoid overloading the cloud service) but use the trainining data that the cloud service uses?

Hi Siddhartha, thanks for the question! Here is the code and instructions to host a server yourself: https://github.com/hanwenzhu/lean-premise-server. In .env, you may specify your own dataset and/or your own trained model from Hugging Face, by DATA_* and MODEL_* (or just use ours). You may also want to use a CPU-only server, quantization, etc. (see the other entries in .env). Then you should be able to deploy a server by docker compose up. To use the server in Lean, you may do:

set_option premiseSelection.apiBaseUrl "http://my_api_url"

You can see the README of premise-selection and lean-premise-server for more information.

[Siddhartha Gadgil]

Thomas Zhu said:

Siddhartha Gadgil said:

Thanks for this brilliant tool. I intend to use it a lot. There are instructions for using the cloud-based service and for training locally. How do I host locally the premise selector (so avoid overloading the cloud service) but use the trainining data that the cloud service uses?

Hi Siddhartha, thanks for the question! Here is the code and instructions to host a server yourself: https://github.com/hanwenzhu/lean-premise-server. In .env, you may specify your own dataset and/or your own trained model from Hugging Face, by DATA_* and MODEL_* (or just use ours). You may also want to use a CPU-only server, quantization, etc. (see the other entries in .env). Then you should be able to deploy a server by docker compose up. To use the server in Lean, you may do:

set_option premiseSelection.apiBaseUrl "http://my_api_url"

You can see the README of premise-selection and lean-premise-server for more information.

I want to "just use" your trained models. Can you point to the link on Huggingface? Thanks.

[Thomas Zhu]

@Siddhartha Gadgil Currently it is https://huggingface.co/hanwenzhu/all-distilroberta-v1-lr2e-4-bs256-nneg3-ml-ne2/tree/v4.20.0, as indicated in the MODEL_ID in https://github.com/hanwenzhu/lean-premise-server/blob/main/.env.

[Thomas Zhu]

The plan is there will be a new branch per data revision, and the link above is very much subject to change.

[Siddhartha Gadgil]

Thanks. I will look up the link in the corresponding file.

[Kim Morrison]

I'm intermittently getting:

Lean.PremiseSelection.orElse: Premise selector failed with error:
Could not send API request to http://leanpremise.net/max-new-premises.

[Thomas Zhu]

Kim Morrison said:

I'm intermittently getting:

Lean.PremiseSelection.orElse: Premise selector failed with error:
Could not send API request to http://leanpremise.net/max-new-premises.

Thanks for reporting the error! We are currently using the cloud-based premise selector at leanpremise.net by default. The error is either a network error on your side (you may check if there is a good connection by going to http://leanpremise.net/max-new-premises in the browser; it should say 2048), or an error on the server side (e.g. server overloaded?). I am not sure where the issue is; on my side I can access the URL, and I don't see any errors in the server logs. (FYI, in this case as a fallback Hammer will use the MePo selector you wrote.)

[Thomas Zhu]

(I also put investigating this error in my to-dos. I realize intermittent errors can't really be reproduced, but if there is a MWE it would also really help. Thanks!)

[Malvin Gattinger]

Looks like a great tool! Is there an overview somewhere what sort of API or other online requests it makes? (I.e. is it leanpremise.net or also other things?) What are the ToC for those APIs And can I use LeanHammer completely offline? (Be it for privacy or because I'm on a train in Germany...)

[Thomas Zhu]

The only online request it currently makes (excluding one-time requests made during installation) is our cloud premise selector. For an overview, you can see this repository. Currently, for performance reasons, the server stores a cache of user premises not tied to user identity. But I cannot guarantee these are not subject to change (e.g. we may add a (strictly opt-in) option to let us collect usage data for training / user studies; we may add a cloud-based TPTP solver like what Sledgehammer does, etc). To not use this API, you should write

set_premise_selector Lean.PremiseSelection.mepoSelector

before any invocation of hammer or premises, to use the MePo selector instead, which is a selector that runs locally but has less accurate retrieval. If you are on a train and did not write the above line, then using the hammer or premises tactic will raise a warning that the connection failed and then fall back to this selector. Alternatively (especially if you have the time & resources to look into this), you can set up your own premise selection server e.g. at localhost, and write set_option premiseSelection.apiBaseUrl "http://localhost". The instructions can be found in the above link.

[Thomas Zhu]

(You can also check the source code of the premise selection server here.)

[Kim Morrison]

If it is helpful, I have just pushed a branch hammer to my fork (kim-em/mathlib4) of Mathlib. It adds the dependencies, imports Hammer early in Mathlib, and tries to call hammer just once, in Mathlib.Data.Nat.Factorial.Basic.

I've had mixed success, as the network error I've reported above it persistent for me.

If you would like to try this out (hopefully soon including at least a partial olean cache), you can run:

git remote add kim-em https://github.com/kim-em/mathlib4.git
git fetch kim-em
git checkout --track kim-em/hammer
lake build

(Note, I'm not planning to keep this up to date with master, or to fix all the many problems that are already present on this branch! Perhaps the hammer team might like to host their own fork that they keep up to date?)

[Kim Morrison]

This is really one for the authors of lean-auto, @Yicheng Qian: it seems lean-auto is incompatible with mathlib, in the sense that if lean-auto is imported, Mathlib builds fail with

error: Mathlib/Order/Interval/Set/Pi.lean:216:2: (kernel) application type mismatch
  Auto.One.ofOfNat1
argument has type
  OfNat ((j : ι) → α j) 0
but function has type
  [OfNat ((j : ι) → α j) 1] → Auto.One ((j : ι) → α j)

[Sophie Morel]

Thomas Zhu said:

temp-v4.21.0-rc3

I have a lakefile.lean, so instead I added a line

require Hammer from git "https://github.com/JOSHCLUNE/LeanHammer" @ "temp-v4.21.0-rc3lake "

before the require mathlib line. Then I did lake update and lake build, and I tried the test file from your git project. The import Hammer fails with the same

unknown module prefix 'Hammer'

error message that I was getting last week.

[Sophie Morel]

I am using v4.21.0-rc3. In fact if I type lean -v in a terminal, I get this:

Lean (version 4.21.0-rc3, x86_64-unknown-linux-gnu, commit 6741444a63ee, Release)

[Sophie Morel]

Wait, I had an extra space at the end of the require Hammer line. I removed it, did lake update + lake build again, and now I don't get the error message, but vscode is building a whole lot of things starting with Aesop and Batteries. (I thought lake build was supposed to bypass this? Anyway.) Will report on whether the hammer is able to prove True when it finishes building.

[Sophie Morel]

Nope, I get an error message telling me that Auto.Translation doesn't build. I also get a

warning: manifest out of date: git revision of dependency 'Hammer' changed; use `lake update Hammer` to update it

but when I try lake update Hammer, it says

/home/sophie/lean4/Appendix/.lake/packages/Hammer: revision not found 'temp-v4.21.0-rc3lake'

[Sophie Morel]

I feel like I'm missing something obvious here. Maybe I was supposed to import Hammer in a different way?

[Sophie Morel]

Tried again. Now lake update Hammer succeeds, but I still get the same error when I tryimport Hammer. (Telling me that Auto.Translation does not build.)
I'm giving up for now.

[Jared green]

so, what would it take for leanhammer to support full induction?(without the compromise of being more limited in what it can do when using induction)

[Mario Carneiro]

Thomas Zhu said:

Hi Kim, I think require "JOSHCLUNE" / "Hammer" @ git "temp-v4.21.0-rc3" works. I am not very familiar with this: does lake automatically resolve "JOSHCLUNE" / "Hammer" to the GitHub repo JOSHCLUNE/LeanHammer based on the package name Hammer? If this is a stable solution, then I think I can update README to use this notation instead.

Yes, this is very confusing because of the syntax but "JOSHCLUNE" / "Hammer" is referring to the github user/organization JOSHCLUNE and the lean package Hammer. The repo name is not included in the request. The way this works is that reservoir scrapes all applicable lean repos, finds JOSHCLUNE/LeanHammer among them, and upon building the repo finds that the package name is Hammer and adds "JOSHCLUNE" / "Hammer" to the reservoir index

[Thomas Zhu]

Kim Morrison said:

If it is helpful, I have just pushed a branch hammer to my fork (kim-em/mathlib4) of Mathlib. It adds the dependencies, imports Hammer early in Mathlib, and tries to call hammer just once, in Mathlib.Data.Nat.Factorial.Basic.

I've had mixed success, as the network error I've reported above it persistent for me.

If you would like to try this out (hopefully soon including at least a partial olean cache), you can run:

git remote add kim-em https://github.com/kim-em/mathlib4.git
git fetch kim-em
git checkout --track kim-em/hammer
lake build

(Note, I'm not planning to keep this up to date with master, or to fix all the many problems that are already present on this branch! Perhaps the hammer team might like to host their own fork that they keep up to date?)

Thank you very much! We will check your branch, and I will discuss this possibility of maintaining a fork with our team.

[Thomas Zhu]

Kim Morrison said:

This is really one for the authors of lean-auto, Yicheng Qian: it seems lean-auto is incompatible with mathlib, in the sense that if lean-auto is imported, Mathlib builds fail with

error: Mathlib/Order/Interval/Set/Pi.lean:216:2: (kernel) application type mismatch
  Auto.One.ofOfNat1
argument has type
  OfNat ((j : ι) → α j) 0
but function has type
  [OfNat ((j : ι) → α j) 1] → Auto.One ((j : ι) → α j)

(@Yicheng Qian For the record, this is probably occurring with my fork of lean-auto here and the newest Mathlib on v4.21.0-rc3.)

[Thomas Zhu]

Sophie Morel said:

Thomas Zhu said:

temp-v4.21.0-rc3

I have a lakefile.lean, so instead I added a line

require Hammer from git "https://github.com/JOSHCLUNE/LeanHammer" @ "temp-v4.21.0-rc3lake "

before the require mathlib line. Then I did lake update and lake build, and I tried the test file from your git project. The import Hammer fails with the same

unknown module prefix 'Hammer'

error message that I was getting last week.

It should be:

require Hammer from git "https://github.com/JOSHCLUNE/LeanHammer" @ "temp-v4.21.0-rc3"

(Note there is no lake at the end.)

[Thomas Zhu]

Jared green said:

so, what would it take for leanhammer to support full induction?(without the compromise of being more limited in what it can do when using induction)

Thank you for your interest! Generating induction proofs is currently not on our plan. If you need induction on e.g. n : Nat, you can manually do induction n first, and try hammer on each subgoal.

[Sophie Morel]

Thomas Zhu said:

Sophie Morel said:

Thomas Zhu said:

temp-v4.21.0-rc3

I have a lakefile.lean, so instead I added a line

require Hammer from git "https://github.com/JOSHCLUNE/LeanHammer" @ "temp-v4.21.0-rc3lake "

before the require mathlib line. Then I did lake update and lake build, and I tried the test file from your git project. The import Hammer fails with the same

unknown module prefix 'Hammer'

error message that I was getting last week.

It should be:

require Hammer from git "https://github.com/JOSHCLUNE/LeanHammer" @ "temp-v4.21.0-rc3"

(Note there is no lake at the end.)

:face_palm:
However, I fixed the lakefile.lean, I ran lake update, lake update hammer and lake build, reopened the lean file, and I still get the same mistake...

[Sophie Morel]

(I'm also trying it in a project that uses version 4.20.0, but there it decided to rebuild all of mathlib for some reason, and it still hasn't finished with that, so I can't tell whether 'Hammer' will work.)

[Thomas Zhu]

Sophie Morel said:

(I'm also trying it in a project that uses version 4.20.0, but there it decided to rebuild all of mathlib for some reason, and it still hasn't finished with that, so I can't tell whether 'Hammer' will work.)

Can you try putting the require Hammer before require mathlib in your lakefile?

[Thomas Zhu]

(The reason is that LeanHammer uses some pinned versions of dependencies like Aesop, Batteries that may differ from those in Mathlib, and that causes Mathlib to rebuild)

[Sophie Morel]

It is already before the require mathlib.

[Sophie Morel]

(In both of the projects. I just checked. This is the one thing I did not mess up.)

[Thomas Zhu]

Sophie Morel said:

:face_palm:
However, I fixed the lakefile.lean, I ran lake update, lake update hammer and lake build, reopened the lean file, and I still get the same mistake...

Can you try lake build Hammer?

[Sophie Morel]

I tried lake build Hammer, it failed with this error message:

✖ [1042/1089] Building Auto.Translation
trace: .> LEAN_PATH=/home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean:/home/sophie/lean4/Appendix/.lake/packages/Duper/.lake/build/lib/lean:/home/sophie/lean4/Appendix/.lake/packages/premise-selection/.lake/build/lib/lean:/home/sophie/lean4/Appendix/.lake/packages/Hammer/HammerCore/.lake/build/lib/lean:/home/sophie/lean4/Appendix/.lake/packages/batteries/.lake/build/lib/lean:/home/sophie/lean4/Appendix/.lake/packages/Qq/.lake/build/lib/lean:/home/sophie/lean4/Appendix/.lake/packages/aesop/.lake/build/lib/lean:/home/sophie/lean4/Appendix/.lake/packages/proofwidgets/.lake/build/lib/lean:/home/sophie/lean4/Appendix/.lake/packages/importGraph/.lake/build/lib/lean:/home/sophie/lean4/Appendix/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/home/sophie/lean4/Appendix/.lake/packages/plausible/.lake/build/lib/lean:/home/sophie/lean4/Appendix/.lake/packages/MD4Lean/.lake/build/lib/lean:/home/sophie/lean4/Appendix/.lake/packages/BibtexQuery/.lake/build/lib/lean:/home/sophie/lean4/Appendix/.lake/packages/UnicodeBasic/.lake/build/lib/lean:/home/sophie/lean4/Appendix/.lake/packages/Cli/.lake/build/lib/lean:/home/sophie/lean4/Appendix/.lake/packages/Hammer/.lake/build/lib/lean:/home/sophie/lean4/Appendix/.lake/packages/mathlib/.lake/build/lib/lean:/home/sophie/lean4/Appendix/.lake/packages/checkdecls/.lake/build/lib/lean:/home/sophie/lean4/Appendix/.lake/packages/doc-gen4/.lake/build/lib/lean:/home/sophie/lean4/Appendix/.lake/build/lib/lean /home/sophie/.elan/toolchains/leanprover--lean4---v4.21.0-rc3/bin/lean /home/sophie/lean4/Appendix/.lake/packages/auto/Auto/Translation.lean -R /home/sophie/lean4/Appendix/.lake/packages/auto -o /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto/Translation.olean -i /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto/Translation.ilean -c /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/ir/Auto/Translation.c --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Lib_Containers.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Lib_LevelExtra.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Lib_AbstractMVars.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Lib_ExprExtra.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Lib_DeCompile.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Lib_MonadUtils.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Lib_BoolExtra.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Lib_MessageData.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Lib_IsomType.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Lib_ListExtra.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Translation_Assumptions.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Lib_MetaExtra.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Translation_Reduction.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Translation_Inductive.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Translation_ReifM.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Translation_Preprocessing.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Lib_StringExtra.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Embedding_Lift.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Translation_Inhabitation.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Lib_MetaState.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Translation_SMTAttributes.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Translation_Monomorphization.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Lib_HEqExtra.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Lib_NatExtra.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Lib_HList.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_MathlibEmulator_Basic.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_MathlibEmulator_ToLevel.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_MathlibEmulator_DeriveToExpr.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_MathlibEmulator_ToExpr.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_MathlibEmulator.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Lib_OptionExtra.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Lib_Pos.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Lib_ToExprExtra.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Lib_BinTree.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Embedding_LCtx.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Lib_IntExtra.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Embedding_LamBase.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Translation_LamUtils.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Embedding_LamBVarOp.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Embedding_LamSystem.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Embedding_LamTermInterp.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Embedding_LamConv.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Embedding_LamInference.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Embedding_LamLCtx.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Embedding_LamPrep.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Embedding_LamBitVec.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Embedding_LamInductive.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Embedding_LamChecker.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Embedding_LamInhReasoning.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Translation_LamReif.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_IR_SMT.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Parser_NDFA.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Parser_LeanLex.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Parser_LexInit.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Parser_SMTParser.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Solver_SMT.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Translation_LamFOL2SMT.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_IR_TPTP__TH0.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Translation_Lam2TH0.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Translation_Lam2DAtomAsFVar.so --json
info: stderr:
libc++abi: terminating due to uncaught exception of type lean::exception: error loading plugin, initializer not found 'initialize_Auto_Translation_Monomorphization'
error: Lean exited with code 134
Some required builds logged failures:
- Auto.Translation
error: build failed

[Jireh Loreaux]

Thomas Zhu said:

(The reason is that LeanHammer uses some pinned versions of dependencies like Aesop, Batteries that may differ from those in Mathlib, and that causes Mathlib to rebuild)

Why isn't LeanHammer bumping those dependencies?

[Thomas Zhu]

Sophie Morel said:

✖ [1042/1089] Building Auto.Translation
trace: .> LEAN_PATH=/home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean:/home/sophie/lean4/Appendix/.lake/packages/Duper/.lake/build/lib/lean:/home/sophie/lean4/Appendix/.lake/packages/premise-selection/.lake/build/lib/lean:/home/sophie/lean4/Appendix/.lake/packages/Hammer/HammerCore/.lake/build/lib/lean:/home/sophie/lean4/Appendix/.lake/packages/batteries/.lake/build/lib/lean:/home/sophie/lean4/Appendix/.lake/packages/Qq/.lake/build/lib/lean:/home/sophie/lean4/Appendix/.lake/packages/aesop/.lake/build/lib/lean:/home/sophie/lean4/Appendix/.lake/packages/proofwidgets/.lake/build/lib/lean:/home/sophie/lean4/Appendix/.lake/packages/importGraph/.lake/build/lib/lean:/home/sophie/lean4/Appendix/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/home/sophie/lean4/Appendix/.lake/packages/plausible/.lake/build/lib/lean:/home/sophie/lean4/Appendix/.lake/packages/MD4Lean/.lake/build/lib/lean:/home/sophie/lean4/Appendix/.lake/packages/BibtexQuery/.lake/build/lib/lean:/home/sophie/lean4/Appendix/.lake/packages/UnicodeBasic/.lake/build/lib/lean:/home/sophie/lean4/Appendix/.lake/packages/Cli/.lake/build/lib/lean:/home/sophie/lean4/Appendix/.lake/packages/Hammer/.lake/build/lib/lean:/home/sophie/lean4/Appendix/.lake/packages/mathlib/.lake/build/lib/lean:/home/sophie/lean4/Appendix/.lake/packages/checkdecls/.lake/build/lib/lean:/home/sophie/lean4/Appendix/.lake/packages/doc-gen4/.lake/build/lib/lean:/home/sophie/lean4/Appendix/.lake/build/lib/lean /home/sophie/.elan/toolchains/leanprover--lean4---v4.21.0-rc3/bin/lean /home/sophie/lean4/Appendix/.lake/packages/auto/Auto/Translation.lean -R /home/sophie/lean4/Appendix/.lake/packages/auto -o /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto/Translation.olean -i /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto/Translation.ilean -c /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/ir/Auto/Translation.c --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Lib_Containers.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Lib_LevelExtra.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Lib_AbstractMVars.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Lib_ExprExtra.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Lib_DeCompile.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Lib_MonadUtils.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Lib_BoolExtra.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Lib_MessageData.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Lib_IsomType.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Lib_ListExtra.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Translation_Assumptions.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Lib_MetaExtra.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Translation_Reduction.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Translation_Inductive.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Translation_ReifM.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Translation_Preprocessing.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Lib_StringExtra.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Embedding_Lift.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Translation_Inhabitation.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Lib_MetaState.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Translation_SMTAttributes.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Translation_Monomorphization.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Lib_HEqExtra.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Lib_NatExtra.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Lib_HList.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_MathlibEmulator_Basic.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_MathlibEmulator_ToLevel.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_MathlibEmulator_DeriveToExpr.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_MathlibEmulator_ToExpr.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_MathlibEmulator.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Lib_OptionExtra.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Lib_Pos.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Lib_ToExprExtra.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Lib_BinTree.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Embedding_LCtx.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Lib_IntExtra.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Embedding_LamBase.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Translation_LamUtils.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Embedding_LamBVarOp.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Embedding_LamSystem.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Embedding_LamTermInterp.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Embedding_LamConv.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Embedding_LamInference.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Embedding_LamLCtx.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Embedding_LamPrep.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Embedding_LamBitVec.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Embedding_LamInductive.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Embedding_LamChecker.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Embedding_LamInhReasoning.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Translation_LamReif.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_IR_SMT.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Parser_NDFA.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Parser_LeanLex.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Parser_LexInit.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Parser_SMTParser.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Solver_SMT.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Translation_LamFOL2SMT.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_IR_TPTP__TH0.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Translation_Lam2TH0.so --plugin /home/sophie/lean4/Appendix/.lake/packages/auto/.lake/build/lib/lean/Auto_Translation_Lam2DAtomAsFVar.so --json
info: stderr:
libc++abi: terminating due to uncaught exception of type lean::exception: error loading plugin, initializer not found 'initialize_Auto_Translation_Monomorphization'
error: Lean exited with code 134
Some required builds logged failures:
- Auto.Translation
error: build failed

Maybe try deleting the entire .lake and try again? Also were there errors during lake update?

[Thomas Zhu]

Jireh Loreaux said:

Thomas Zhu said:

(The reason is that LeanHammer uses some pinned versions of dependencies like Aesop, Batteries that may differ from those in Mathlib, and that causes Mathlib to rebuild)

Why isn't LeanHammer bumping those dependencies?

Sorry, I just realized that is our mistake. I will bump a version so that LeanHammer @ main and @ v4.20.0 uses everything pinned at v4.20.0

[Sophie Morel]

lake build runs with no errors. I am, quite frankly, not an expert with these things and I'm afraid totally mess up my project if I start deleting stuff willy-nilly. I think I'll wait until there's a version that is truly compatible with v4.21.0.

[Sophie Morel]

In my other project, the one using v4.20.0, I was finally able to make the import Hammer command work, and Hammer now succesfully proves True. However following the instructions on the git site was not enough, I also had to run lake build Hammer on the command line.

[Thomas Zhu]

Sophie Morel said:

In my other project, the one using v4.20.0, I was finally able to make the import Hammer command work, and Hammer now succesfully proves True. However following the instructions on the git site was not enough, I also had to run lake build Hammer on the command line.

Thanks! I will see if our README instructions need to be updated.

[Thomas Zhu]

Thomas Zhu said:

Sorry, I just realized that is our mistake. I will bump a version so that LeanHammer @ main and @ v4.20.0 uses everything pinned at v4.20.0

This should now be done.

[Thomas Zhu]

Sophie Morel said:

lake build runs with no errors. I am, quite frankly, not an expert with these things and I'm afraid totally mess up my project if I start deleting stuff willy-nilly. I think I'll wait until there's a version that is truly compatible with v4.21.0.

Just for the record, I also had a project in which I was messing around with lakefile, and it triggered the same libc++abi: terminating due to uncaught exception of type lean::exception: error loading plugin, initializer not found 'initialize_Auto_Translation_Monomorphization' error as you saw. It was fixed by rm -rf .lake and trying everything again (lake update then lake build). I am not sure what is causing it.

[Sophie Morel]

You're talking to the person who once accidentally pushed mathlib4 into a branch of mathlib3. I am cursed and all my computers are cursed. (More seriously, I have only the vaguest idea of what most of these commands are doing, and they are like dark magic incantations to me.)

[Jared green]

if someone was to try to train a model just for lemma synthesis, could it be integrated into this(at test/use time) or would it have to be running side by side(calling hammer on the lemmas and goal until the goal succeeds or time runs out, and keeping those that the proof uses)

[Thomas Zhu]

Jared green said:

if someone was to try to train a model just for lemma synthesis, could it be integrated into this(at test/use time) or would it have to be running side by side(calling hammer on the lemmas and goal until the goal succeeds or time runs out, and keeping those that the proof uses)

In principle lemma/have-synthesis is orthogonal to solving the lemmas. You can let a model synthesize some lemma a : B := by sorry and replace sorry by hammer to see if it works. (On a related note, please don't use our server for massive machine learning experiments, it will break.)

[Thomas Zhu]

You may check the "Draft, Sketch, and Prove" paper for an implementation of this in Isabelle with Sledgehammer.

[Jared green]

i see. though the lemma synthesis of which i am thinking would depend on what proof searching the hammer can do, some lemmas will be pointless when certain tactics are being called by the hammer yet necessary without it. my thinking is to reinforce only the lemmas actually used by a successful proof so we dont get a model splitting a proof into too many very small steps like deepseek-prover v2 does

[Jared green]

and i dont have the resources to do it myself, but i think it can be done.

[Jared green]

how do you get the latest revisions of all dependencies (and mathlib) that were on 4.20.0(after changing the lean-toolchain)?

[Yicheng Qian]

Kim Morrison said:

This is really one for the authors of lean-auto, Yicheng Qian: it seems lean-auto is incompatible with mathlib, in the sense that if lean-auto is imported, Mathlib builds fail with

error: Mathlib/Order/Interval/Set/Pi.lean:216:2: (kernel) application type mismatch
  Auto.One.ofOfNat1
argument has type
  OfNat ((j : ι) → α j) 0
but function has type
  [OfNat ((j : ι) → α j) 1] → Auto.One ((j : ι) → α j)

@Kim Morrison @Thomas Zhu I've been trying to fix the issue. I've modified some files in Lean-auto and update the Lean version to v4.20.0. There are some wierd issues popping up when I ran evaluation of Lean-auto, and I plan to fix them later (hopefully just importing Lean-auto doesn't crash Mathlib). I would recommend first modifying the version of Lean-auto you have by removing Auto/MathlibEmulator/Basic.lean and modifying the imports of Auto/MathlibEmulator.lean. If it doesn't work try using the latest version of Lean-auto. If it still doesn't work please let me know.

[Thomas Zhu]

@Yicheng Qian Thanks! By the way, LeanHammer is using the hammer branch of Lean-auto, which is already on v4.20.0. I will look into removing Auto.MathlibEmulator.Basic. (or feel free to push to the hammer branch if it is a safe change)

[Thomas Zhu]

Jared green said:

how do you get the latest revisions of all dependencies (and mathlib) that were on 4.20.0(after changing the lean-toolchain)?

You can specify the dependency revisions in lakefile, and then run lake update.

[Siddhartha Gadgil]

A rather silly comment, but would it not be more consistent to call the tactic hammer? (I actually ran it to see that it has a TryThis)?

[Siddhartha Gadgil]

(deleted)

[Jared green]

how do you specify the revision?

[Jared green]

(deleted)

[Jared green]

(deleted)

[Jared green]

(i have lakefile.toml)

[Jared green]

how do you dun lake update without it changing the toolchain?

[Bolton Bailey]

Is there something different about the "Try this" mechanism for hammer? I got it to find a proof, but I can't just click on the successful proof and have it automatically be edited into my file like other ? tactics.

[Siddhartha Gadgil]

Normally lake update does not change the toolchain. Only mathlib updates it to its toolchain.

[Siddhartha Gadgil]

Using the mathlib tagged with the correct toolchain should be fine

[Jared green]

yet that is what is happening

[Jared green]

and im getting build errors now

[Thomas Zhu]

Bolton Bailey said:

Is there something different about the "Try this" mechanism for hammer? I got it to find a proof, but I can't just click on the successful proof and have it automatically be edited into my file like other ? tactics.

Hmm, that is the intended behavior, but I am seeing the same issue. I will check what is causing this! (See below)

[Thomas Zhu]

Siddhartha Gadgil said:

A rather silly comment, but would it not be more consistent to call the tactic hammer? (I actually ran it to see that it has a TryThis)?

I think the reason is we don't have a corresponding non-TryThis option, since it's infeasible to leave any hammer invocation (which depends on network connection, system setup, timeout in seconds, etc) in the proof. I think this aspect is similar to polyrith which also doesn't have a question mark.

[Jared green]

after running lake exe cache get and multiple vscode restarts, i get this:

`c:\Users\jared\.elan\toolchains\leanprover--lean4---v4.21.0-rc3\bin\lake.exe setup-file C:/Users/jared/lean projects/polysat2/Polysat2/hammer_test.lean Init Hammer` failed:

stderr:
✖ [785/1090] Building Duper.Util.AbstractMVars
trace: .> LEAN_PATH=C:\Users\jared\lean projects\polysat2\.lake\packages\auto\.lake\build\lib\lean;C:\Users\jared\lean projects\polysat2\.lake\packages\Duper\.lake\build\lib\lean;C:\Users\jared\lean projects\polysat2\.lake\packages\premise-selection\.lake\build\lib\lean;C:\Users\jared\lean projects\polysat2\.lake\packages\Hammer\HammerCore\.lake\build\lib\lean;C:\Users\jared\lean projects\polysat2\.lake\packages\Cli\.lake\build\lib\lean;C:\Users\jared\lean projects\polysat2\.lake\packages\batteries\.lake\build\lib\lean;C:\Users\jared\lean projects\polysat2\.lake\packages\Qq\.lake\build\lib\lean;C:\Users\jared\lean projects\polysat2\.lake\packages\aesop\.lake\build\lib\lean;C:\Users\jared\lean projects\polysat2\.lake\packages\proofwidgets\.lake\build\lib\lean;C:\Users\jared\lean projects\polysat2\.lake\packages\importGraph\.lake\build\lib\lean;C:\Users\jared\lean projects\polysat2\.lake\packages\LeanSearchClient\.lake\build\lib\lean;C:\Users\jared\lean projects\polysat2\.lake\packages\plausible\.lake\build\lib\lean;C:\Users\jared\lean projects\polysat2\.lake\packages\Hammer\.lake\build\lib\lean;C:\Users\jared\lean projects\polysat2\.lake\packages\mathlib\.lake\build\lib\lean;C:\Users\jared\lean projects\polysat2\.lake\packages\Canonical\.lake\build\lib\lean;C:\Users\jared\lean projects\polysat2\.lake\build\lib\lean c:\Users\jared\.elan\toolchains\leanprover--lean4---v4.21.0-rc3\bin\lean.exe C:\Users\jared\lean projects\polysat2\.lake\packages\Duper\Duper\Util\AbstractMVars.lean -R C:\Users\jared\lean projects\polysat2\.lake\packages\Duper -o C:\Users\jared\lean projects\polysat2\.lake\packages\Duper\.lake\build\lib\lean\Duper\Util\AbstractMVars.olean -i C:\Users\jared\lean projects\polysat2\.lake\packages\Duper\.lake\build\lib\lean\Duper\Util\AbstractMVars.ilean -c C:\Users\jared\lean projects\polysat2\.lake\packages\Duper\.lake\build\ir\Duper\Util\AbstractMVars.c --plugin C:\Users\jared\lean projects\polysat2\.lake\packages\Duper\.lake\build\lib\lean\Duper_Util_Misc.dll --plugin C:\Users\jared\lean projects\polysat2\.lake\packages\Duper\.lake\build\lib\lean\Duper_Util_Reduction.dll --json
error: Duper/Util/AbstractMVars.lean:139:37: 'numMVars' is not a field of structure 'AbstractMVarsResult'
error: Duper/Util/AbstractMVars.lean:139:7: fields missing: 'mvars'
error: Duper/Util/AbstractMVars.lean:152:37: 'numMVars' is not a field of structure 'AbstractMVarsResult'
error: Duper/Util/AbstractMVars.lean:152:7: fields missing: 'mvars'
error: Duper/Util/AbstractMVars.lean:184:37: 'numMVars' is not a field of structure 'AbstractMVarsResult'
error: Duper/Util/AbstractMVars.lean:184:7: fields missing: 'mvars'
error: Lean exited with code 1
✖ [935/1090] Building Auto.Lib.AbstractMVars
trace: .> LEAN_PATH=C:\Users\jared\lean projects\polysat2\.lake\packages\auto\.lake\build\lib\lean;C:\Users\jared\lean projects\polysat2\.lake\packages\Duper\.lake\build\lib\lean;C:\Users\jared\lean projects\polysat2\.lake\packages\premise-selection\.lake\build\lib\lean;C:\Users\jared\lean projects\polysat2\.lake\packages\Hammer\HammerCore\.lake\build\lib\lean;C:\Users\jared\lean projects\polysat2\.lake\packages\Cli\.lake\build\lib\lean;C:\Users\jared\lean projects\polysat2\.lake\packages\batteries\.lake\build\lib\lean;C:\Users\jared\lean projects\polysat2\.lake\packages\Qq\.lake\build\lib\lean;C:\Users\jared\lean projects\polysat2\.lake\packages\aesop\.lake\build\lib\lean;C:\Users\jared\lean projects\polysat2\.lake\packages\proofwidgets\.lake\build\lib\lean;C:\Users\jared\lean projects\polysat2\.lake\packages\importGraph\.lake\build\lib\lean;C:\Users\jared\lean projects\polysat2\.lake\packages\LeanSearchClient\.lake\build\lib\lean;C:\Users\jared\lean projects\polysat2\.lake\packages\plausible\.lake\build\lib\lean;C:\Users\jared\lean projects\polysat2\.lake\packages\Hammer\.lake\build\lib\lean;C:\Users\jared\lean projects\polysat2\.lake\packages\mathlib\.lake\build\lib\lean;C:\Users\jared\lean projects\polysat2\.lake\packages\Canonical\.lake\build\lib\lean;C:\Users\jared\lean projects\polysat2\.lake\build\lib\lean c:\Users\jared\.elan\toolchains\leanprover--lean4---v4.21.0-rc3\bin\lean.exe C:\Users\jared\lean projects\polysat2\.lake\packages\auto\Auto\Lib\AbstractMVars.lean -R C:\Users\jared\lean projects\polysat2\.lake\packages\auto -o C:\Users\jared\lean projects\polysat2\.lake\packages\auto\.lake\build\lib\lean\Auto\Lib\AbstractMVars.olean -i C:\Users\jared\lean projects\polysat2\.lake\packages\auto\.lake\build\lib\lean\Auto\Lib\AbstractMVars.ilean -c C:\Users\jared\lean projects\polysat2\.lake\packages\auto\.lake\build\ir\Auto\Lib\AbstractMVars.c --json
error: Auto/Lib/AbstractMVars.lean:135:37: 'numMVars' is not a field of structure 'AbstractMVarsResult'
error: Auto/Lib/AbstractMVars.lean:135:7: fields missing: 'mvars'
error: Auto/Lib/AbstractMVars.lean:148:37: 'numMVars' is not a field of structure 'AbstractMVarsResult'
error: Auto/Lib/AbstractMVars.lean:148:7: fields missing: 'mvars'
error: Auto/Lib/AbstractMVars.lean:183:37: 'numMVars' is not a field of structure 'AbstractMVarsResult'
error: Auto/Lib/AbstractMVars.lean:183:7: fields missing: 'mvars'
error: Lean exited with code 1
Some required builds logged failures:
- Duper.Util.AbstractMVars
- Auto.Lib.AbstractMVars
error: build failed

[Thomas Zhu]

@Jared green Can you try specifying rev = "temp-v4.21.0-rc3" for LeanHammer in your lakefile.toml?

[Jared green]

that does not change the error message except to give a warning

warning: manifest out of date: git revision of dependency 'Hammer' changed; use `lake update Hammer` to update it

[Thomas Zhu]

Yes, you can follow the instruction and try lake update Hammer first.

[Thomas Zhu]

Bolton Bailey said:

Is there something different about the "Try this" mechanism for hammer? I got it to find a proof, but I can't just click on the successful proof and have it automatically be edited into my file like other ? tactics.

I think the try-this suggestion is given twice in Infoview: once in the "Suggestions" tab and once in the "Messages" tab. You can click on the one in the Suggestions tab, but the one in the Messages tab is not interactive.

image.png

[Jared green]

i did, twice

[Thomas Zhu]

Jared green said:

i did, twice

Does the warning warning: manifest out of date: git revision of dependency 'Hammer' changed; use `lake update Hammer` to update it persist after you run lake update? If so, it looks like a lake issue and maybe you can rm -rf .lake and try again.

[Jared green]

it does

[Jared green]

that line doesnt work

[Jared green]

PS C:\Users\jared\lean projects\polysat2> rm -rf .lake
PS C:\Users\jared\lean projects\polysat2> rm -rf .lake
Remove-Item : A parameter cannot be found that matches parameter name 'rf'.
At line:1 char:4
+ rm -rf .lake
+    ~~~
    + CategoryInfo          : InvalidArgument: (:) [Remove-Item], ParameterBindingException
    + FullyQualifiedErrorId : NamedParameterNotFound,Microsoft.PowerShell.Commands.RemoveItemCommand

[Thomas Zhu]

I mean could you remove the .lake directory in your project? I don't know what the equivalent command on Windows is.

[Bolton Bailey]

Screenshot 2025-06-18 at 2.37.37 PM.png

This is what I see. Neither "try this" is clickable

[Kevin Buzzard]

@Jared green that looks like an issue with your shell. rm -rf X means "recursive force removal of X and all subdirectories" in most shells but apparently not in yours? Try git bash or something?

[Thomas Zhu]

Bolton Bailey said:

Screenshot 2025-06-18 at 2.37.37 PM.png

This is what I see. Neither "try this" is clickable

Just wondering — are you trying LeanHammer inside Mathlib?

[Bolton Bailey]

No I am trying it inside an external project importing both mathlib and leanhammer

[Thomas Zhu]

And are you running the temp-v4.21.0-rc3 revision? (or what is your Lean version?)

[Bolton Bailey]

My leantoolchain is leanprover/lean4:v4.21.0-rc3. My lakefile.toml is

name = "workspace-4-20"
version = "0.1.0"
keywords = ["math"]
defaultTargets = ["Workspace420"]

[leanOptions]
pp.unicode.fun = true # pretty-prints `fun a ↦ b`
autoImplicit = false

[[require]]
name = "Hammer"
git = "https://github.com/JOSHCLUNE/LeanHammer"
rev = "temp-v4.21.0-rc3"

[[require]]
name = "mathlib"
scope = "leanprover-community"

[[lean_lib]]
name = "Workspace420"

[Thomas Zhu]

I see. Thanks for the report! I think I can reproduce it, it seems an error that only occurs > v4.20.0. Maybe it's related to some recent change in TryThis in Lean core. I will look into it

[Thomas Zhu]

@Bolton Bailey I think I found the issue. It's not specific to LeanHammer: for example, the following TryThis also fails on Mathlib v4.21.0-rc3 but not v4.20.0.

import Mathlib

example : Continuous (id : ℝ → ℝ) := by
  continuity?

Here, continuity? is a macro for some aesop? ....

[Thomas Zhu]

I am not sure how to fix this. But presumably once continuity? is fixed, the fix should be possible to port to hammer (we also use something like a substitution with aesop?).

[Bolton Bailey]

Nice find! Do you want to file an issue or shall I?

[Thomas Zhu]

You can file the issue if it's convenient for you. Thanks!

[Jared green]

in lieu of a dedicated lemma synthesis model, does anyone have recommendations for how we might do lemma synthesis instead?(asking for the best way, with what is available, without writing new code for it)

[Chase Norman]

It would need to be language model based, so prompt engineering for Lean (most popular DTT language) would be the way. But I care greatly that a proper lemma synthesis model is trained

[Jared green]

in this chat there is a prompt for that. i didnt put much effort into it.
https://chatgpt.com/share/6854822e-ee38-8002-b107-11a11d0ffa61

[Alessandro Sosso]

Hi all, I am encountering some issues in importing LeanHammer: lake appears to download it and build it just fine (at "v4.20.0"), yet upon importing it raises the error invalid option declaration 'lazyReduce.skipProof', option already exists. Any suggestions on how to fix this? Thanks

[Alex Gu]

I am also having some trouble getting LeanHammer to work. My lean-toolchain is version leanprover/lean4:v4.20.0, and here is my lakefile.lean:

...
require Hammer from git "https://github.com/JOSHCLUNE/LeanHammer" @ "main"

require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git" @ "v4.20.0"
...

When I do lake build and lake update everything is fine, but something like import Hammer gives me this:

test.lean:1:0: error: unknown module prefix 'Hammer'

No directory 'Hammer' or file 'Hammer.olean' in the search path entries:
path_to_home/lean/mathlib-4-20/.lake/packages/auto/.lake/build/lib/lean

Any ideas? I can also open an issue on GitHub if that's preferred to asking here :)

[Thomas Zhu]

Alex Gu said:

I am also having some trouble getting LeanHammer to work. My lean-toolchain is version leanprover/lean4:v4.20.0, and here is my lakefile.lean:

...
require Hammer from git "https://github.com/JOSHCLUNE/LeanHammer" @ "main"

require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git" @ "v4.20.0"
...

When I do lake build and lake update everything is fine, but something like import Hammer gives me this:

test.lean:1:0: error: unknown module prefix 'Hammer'

No directory 'Hammer' or file 'Hammer.olean' in the search path entries:
path_to_home/lean/mathlib-4-20/.lake/packages/auto/.lake/build/lib/lean

Any ideas? I can also open an issue on GitHub if that's preferred to asking here :)

Hi Alex, can you try lake build Hammer? (This shouldn't be needed but we can see if it works first) Also does import Mathlib work?

[Thomas Zhu]

Alessandro Sosso said:

Hi all, I am encountering some issues in importing LeanHammer: lake appears to download it and build it just fine (at "v4.20.0"), yet upon importing it raises the error invalid option declaration 'lazyReduce.skipProof', option already exists. Any suggestions on how to fix this? Thanks

Hi Alessandro, I haven't seen the error before. Can you show your lakefile or provide a MWE? (Alternatively you can open an issue on our GitHub).

[Alessandro Sosso]

Thomas Zhu said:

Alessandro Sosso said:

Hi all, I am encountering some issues in importing LeanHammer: lake appears to download it and build it just fine (at "v4.20.0"), yet upon importing it raises the error invalid option declaration 'lazyReduce.skipProof', option already exists. Any suggestions on how to fix this? Thanks

Hi Alessandro, I haven't seen the error before. Can you show your lakefile or provide a MWE? (Alternatively you can open an issue on our GitHub).

Surely! In a blank project I have lean-toolchain

leanprover/lean4:v4.20.0

and lakefile.lean

import Lake
open Lake DSL

package «LeanHammer» where
  -- add any additional package configuration options here

require Hammer from git "https://github.com/JOSHCLUNE/LeanHammer" @ "main"

Everything builds just fine running lake update and lake build Hammer, yet a simple lean file

import Hammer

raises the error LeanHammer.lean:1:0: invalid option declaration 'lazyReduce.skipProof', option already exists.

I may also open the GitHub issue if that's more convenient to you

[Alex Gu]

Thomas Zhu said:

Alex Gu said:

I am also having some trouble getting LeanHammer to work. My lean-toolchain is version leanprover/lean4:v4.20.0, and here is my lakefile.lean:

...
require Hammer from git "https://github.com/JOSHCLUNE/LeanHammer" @ "main"

require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git" @ "v4.20.0"
...

When I do lake build and lake update everything is fine, but something like import Hammer gives me this:

test.lean:1:0: error: unknown module prefix 'Hammer'

No directory 'Hammer' or file 'Hammer.olean' in the search path entries:
path_to_home/lean/mathlib-4-20/.lake/packages/auto/.lake/build/lib/lean

Any ideas? I can also open an issue on GitHub if that's preferred to asking here :)

Hi Alex, can you try lake build Hammer? (This shouldn't be needed but we can see if it works first) Also does import Mathlib work?

Yes, thanks! A combination of this and other things (deleting .lake, rebuilding, etc) managed to fix the issue. Great tool, congrats :smile:

[Thomas Zhu]

@Alessandro Sosso Sorry, I might only be able to look at this in a few days. Can you copy paste what you wrote in a new issue for LeanHammer, so that I can keep track of the issue? Thank you so much! In the meantime, I have a working demo repo here: https://github.com/hanwenzhu/hammer-demo-irrational-two, so maybe you can start from this repo first if you are interested!

[Thomas Zhu]

@Alex Gu Thanks for trying our tool! It's still in early development, and has some rough edges. The intention is to improve it over time as a long term project, similar to Sledgehammer in Isabelle.

[Alessandro Sosso]

Thomas Zhu said:

Alessandro Sosso Sorry, I might only be able to look at this in a few days. Can you copy paste what you wrote in a new issue for LeanHammer, so that I can keep track of the issue? Thank you so much! In the meantime, I have a working demo repo here: https://github.com/hanwenzhu/hammer-demo-irrational-two, so maybe you can start from this repo first if you are interested!

Yes, will do that right away. Thanks for the demo repo!

[Alex Gu]

When I do something like lake env lean xxx.lean and there are multiple hammer's in the file, it will give me a string of "Try this"'s, each corresponding to one hammer. Is there an easy way for me to modify this so that it shows exactly which "hammer" each "Try this" is corresponding to, like line and position? I guess the quick hack is probably to enumerate the positions and then enumerate the "Try this" blocks and match them?

Try this:
  some commands
Try this:
  some commands

[Alessandro Sosso]

Alex Gu said:

When I do something like lake env lean xxx.lean and there are multiple hammer's in the file, it will give me a string of "Try this"'s, each corresponding to one hammer. Is there an easy way for me to modify this so that it shows exactly which "hammer" each "Try this" is corresponding to, like line and position? I guess the quick hack is probably to enumerate the positions and then enumerate the "Try this" blocks and match them?

Try this:
  some commands
Try this:
  some commands

lake env lean xxx.lean --json returns all lean messages in json format, which contain "pos" entries that allow you to retrieve the corresponding hammer invocation

[Alex Gu]

Thanks! Exactly what I'm looking for :)

[Thomas Zhu]

The v4.21.0 revision of LeanHammer is ready to use. You may write in your lakefile.toml:

[[require]]
name = "Hammer"
git = "https://github.com/JOSHCLUNE/LeanHammer"
rev = "v4.21.0"

to use it! For best results, please pin all versions of dependencies and the Lean version to v4.21.0.

[Alex Gu]

Do you happen to have a script that takes the output of LeanHammer and sticks the found code back into the proof? Shouldn't be hard to write one, but thought you might already have one accounting for all the potential parsing edge cases from your benchmarking efforts :)

[Thomas Zhu]

Unfortunately we don't have such a script. For our benchmarking, we simply tested the performance of "by hammer" and never substituted the found proof into the source. I imagine the easiest way to do this would be a simple Python script (taking into account indentation etc)?

[Alex Gu]

I saw sometimes the output will be a set of tactics and then a sorry, what is the heuristic for deciding that it's making partial progress (rather than just report a sorry)?

[Thomas Zhu]

This behavior is from Aesop. Currently, when it fails it would insert a sorry and throw an error. For example you can see the same thing with example (h : 1 + 1 = 2) : False := by aesop?

[Fred Rajasekaran]

I was reading the LeanHammer paper, and in section D.2 it mentions that there was an error when testing it on the Carleson split of miniCTX. Can you comment a bit more on that? And is there anything I should be looking out for while using LeanHammer to avoid/deal with the error?

[Thomas Zhu]

Hi @Fred Rajasekaran, I do not remember exactly the reason we did not test it, but now there should be no such problems anyway. That was back when we had a Python wrapper around a custom metaprogramming tactic benchmark, and now we have a simple tactic interface via hammer.

[Thomas Zhu]

I just tested LeanHammer on Carleson. For example, it can solve this (trivial) problem by retrieving a relevant premise defined earlier within the same file in Carleson!
image.png

[Yicheng Qian]

Can we change "hammer" to "ground" because it's what people would use if grind fails?

[Yicheng Qian]

Imagine you're a user, if you type "grind" and it fails, you just type "ground"

[Alex Gu]

Sporadically I get this error, is it because I am trying to run too many hammer queries at once? :laughter_tears:

testtest.lean:13:4: error: Could not send API request to http://leanpremise.net/max-new-premises. curl exited with code 127:

(never mind, I saw this error was already reported above, probably an overload with the leanpremise.net API)

[Elizaveta Pertseva]

Hello! Question about about auto-smt (maybe specifically for @Yicheng Qian ), when running on a gaol with vectors and ZMod data types I get the following type error Auto.Lemma.rewriteUMonoRigid? :: Motive fun _a => fv1[0].val ≤ 1 is not type correct . Does anyone know what could be causing it/ how one would go about fixing it? Below is a minimal example that causes the issue :

example (fv1 : Vector f 8)  (h1: ZMod.val fv1[0]  <= 1) (h2: ZMod.val fv1[1] <= 1) :
  (ZMod.val fv1[0])*(1- ZMod.val fv1[1])+ (ZMod.val fv1[1])*(1-ZMod.val fv1[0]) <= 1:= by
  auto

[Yicheng Qian]

Which version of Mathlib are you using (check you lake-manifest.json)? I'm getting

Application type mismatch: In the application
  ZMod.val fv1[0]
the argument
  fv1[0]
has type
  f : outParam (Type ?u.1632)
but is expected to have type
  ZMod ?m.13192 : Type

on my side, using mathlib rev 308445d7985027f538e281e18df29ca16ede2ba3.
I assume you mean

example
  (fv1 : Vector (ZMod f) 8) (h1 : ZMod.val fv1[0] <= 1) (h2 : ZMod.val fv1[1] <= 1) :
  (ZMod.val fv1[0]) * (1 - ZMod.val fv1[1]) + (ZMod.val fv1[1])*(1 - ZMod.val fv1[0]) <= 1:= by
  auto

because this gives the same error as the one you got.

[Elizaveta Pertseva]

Yes sorry I accidentally had f set as a ZMod value . I am using Mathlib version v4.21.0

[Yicheng Qian]

@Elizaveta Pertseva Can you open an issue on lean-auto's github repo?

[Elizaveta Pertseva]

Yes!

[Yicheng Qian]

Thanks!

[Siddhartha Gadgil]

Is the update to v4.22.0 imminent? When upgrading a project using LeanHammer I am getting the following build failures:

Some required builds logged failures:
- Auto.Lib.ListExtra
- Auto.Lib.AbstractMVars
- Duper.Expr
- Duper.Util.Misc

[Jeremy Avigad]

@Thomas Zhu and @Josh Clune are working on it, and hope to have it in ready by the end of the week. Both are still busy with summer internships, which poses challenges.

[Siddhartha Gadgil]

Thanks a lot. Looking forward to using grind and hammer together.

[Jeremy Avigad]

Thanks for bearing with us. @Thomas Zhu and @Josh Clune have updated premise selection and the hammer to Lean and Mathlib v4.22.0.

We have also updated the README in the repository to clarify that the hammer is only expected to work with tagged releases of Lean / Mathlib. (We now have versions for v4.20.0, v4.21.0, and v4.22.0.) The dependencies break quickly as Lean changes.

[Kim Morrison]

Could we have a hammer-v4.22.0 tag of Mathlib, that gives us a copy of Mathlib with Hammer added to the requires, and imported early on?

[Kim Morrison]

This would mean that using the hammer is hopefully as simple as checking out a tag/branch of Mathlib, running lake exe cache get, opening a file and typing hammer somewhere.

[Jeremy Avigad]

It seems that there are two issues you are trying to address:

• It's easier to add one dependency (mathlib with rev="hammer-v4.22.0") than two (mathlib, Hammer).
• It would be nice not to have to wait a few minutes for the hammer to build the first time you import it.
  Do I understand the goal of your suggestion correctly?

My (imperfect) understanding is that there isn't an easy workaround for the second. For performance, Duper has to be compiled, and if I understand correctly, there is no way to cache something that is platform specific. Canonical and LeanSMT interact with compiled tools through the FFI, but Duper is built on top of Lean, since it constructs Lean proofs. Is there a better way?

[Sebastian Ullrich]

GitHub releases can be used for that; it looks like auto already has that set up but it is not used when building LeanHammer master because it references an unreleased version
https://github.com/leanprover-community/lean-auto/blob/main/lakefile.lean#L6
https://github.com/leanprover-community/lean-auto/blob/main/.github/workflows/build.yml#L62

[Siddhartha Gadgil]

Kim Morrison said:

Could we have a hammer-v4.22.0 tag of Mathlib, that gives us a copy of Mathlib with Hammer added to the requires, and imported early on?

Personally I would like this very much, and the main motivation is a setup that is tested to work out of the box.

[Kim Morrison]

Yeah, I don't particularly mind the build time.

I just want to be able to experiment with the hammer with the following steps:

git clone https://github.com/leanprover-community/mathlib4
cd mathlib
git checkout hammer-v4.22.0
lake exe cache get
lake build   # happy if this means :coffee:

then open a file in VSCode and type hammer in a proof.

Anything else is too hard. :-)