lean hammer install failing for 4.24

Stream: general

[Frederick Pu]

I'm trying to add lean hammer to my 4.24 project and i get the folowing error:

✖ [37/163] Building Batteries.Tactic.Alias
trace: .> LEAN_PATH=C:\Users\pufre\Downloads\CodingProjects\utm-leannotes\.lake\packages\Cli\.lake\build\lib\lean;C:\Users\pufre\Downloads\CodingProjects\utm-leannotes\.lake\packages\proofwidgets\.lake\build\lib\lean;C:\Users\pufre\Downloads\CodingProjects\utm-leannotes\.lake\packages\importGraph\.lake\build\lib\lean;C:\Users\pufre\Downloads\CodingProjects\utm-leannotes\.lake\packages\LeanSearchClient\.lake\build\lib\lean;C:\Users\pufre\Downloads\CodingProjects\utm-leannotes\.lake\packages\plausible\.lake\build\lib\lean;C:\Users\pufre\Downloads\CodingProjects\utm-leannotes\.lake\packages\auto\.lake\build\lib\lean;C:\Users\pufre\Downloads\CodingProjects\utm-leannotes\.lake\packages\batteries\.lake\build\lib\lean;C:\Users\pufre\Downloads\CodingProjects\utm-leannotes\.lake\packages\aesop\.lake\build\lib\lean;C:\Users\pufre\Downloads\CodingProjects\utm-leannotes\.lake\packages\Duper\.lake\build\lib\lean;C:\Users\pufre\Downloads\CodingProjects\utm-leannotes\.lake\packages\premise-selection\.lake\build\lib\lean;C:\Users\pufre\Downloads\CodingProjects\utm-leannotes\.lake\packages\Qq\.lake\build\lib\lean;C:\Users\pufre\Downloads\CodingProjects\utm-leannotes\.lake\packages\Hammer\HammerCore\.lake\build\lib\lean;C:\Users\pufre\Downloads\CodingProjects\utm-leannotes\.lake\packages\mathlib\.lake\build\lib\lean;C:\Users\pufre\Downloads\CodingProjects\utm-leannotes\.lake\packages\Hammer\.lake\build\lib\lean;C:\Users\pufre\Downloads\CodingProjects\utm-leannotes\.lake\build\lib\lean c:\Users\pufre\.elan\toolchains\leanprover--lean4---v4.24.0\bin\lean.exe C:\Users\pufre\Downloads\CodingProjects\utm-leannotes\.lake\packages\batteries\Batteries\Tactic\Alias.lean -o C:\Users\pufre\Downloads\CodingProjects\utm-leannotes\.lake\packages\batteries\.lake\build\lib\lean\Batteries\Tactic\Alias.olean -i C:\Users\pufre\Downloads\CodingProjects\utm-leannotes\.lake\packages\batteries\.lake\build\lib\lean\Batteries\Tactic\Alias.ilean -c C:\Users\pufre\Downloads\CodingProjects\utm-leannotes\.lake\packages\batteries\.lake\build\ir\Batteries\Tactic\Alias.c --setup C:\Users\pufre\Downloads\CodingProjects\utm-leannotes\.lake\packages\batteries\.lake\build\ir\Batteries\Tactic\Alias.setup.json --json
error: Batteries/Tactic/Alias.lean:116:27: Application type mismatch: The argument
  declMods.docString?
has type
  Option (TSyntax `Lean.Parser.Command.docComment × Bool)
but is expected to have type
  Syntax
in the application
  addDocString' declName declMods.docString?
error: Batteries/Tactic/Alias.lean:152:25: Application type mismatch: The argument
  declMods.docString?
has type
  Option (TSyntax `Lean.Parser.Command.docComment × Bool)
but is expected to have type
  Syntax
in the application
  addDocString' declName declMods.docString?
error: Lean exited with code 1
⚠ [87/202] Built Aesop.Rule.Name
warning: Aesop/Rule/Name.lean:25:27: `Aesop.PhaseName.toCtorIdx` has been deprecated: Use `Aesop.PhaseName.ctorIdx` instead
warning: Aesop/Rule/Name.lean:25:40: `Aesop.PhaseName.toCtorIdx` has been deprecated: Use `Aesop.PhaseName.ctorIdx` instead
warning: Aesop/Rule/Name.lean:46:27: `Aesop.ScopeName.toCtorIdx` has been deprecated: Use `Aesop.ScopeName.ctorIdx` instead
warning: Aesop/Rule/Name.lean:46:40: `Aesop.ScopeName.toCtorIdx` has been deprecated: Use `Aesop.ScopeName.ctorIdx` instead
warning: Aesop/Rule/Name.lean:72:27: `Aesop.BuilderName.toCtorIdx` has been deprecated: Use `Aesop.BuilderName.ctorIdx` instead
warning: Aesop/Rule/Name.lean:72:40: `Aesop.BuilderName.toCtorIdx` has been deprecated: Use `Aesop.BuilderName.ctorIdx` instead
⣾ [355/5055] Running Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes (+ 16 more⣷ [355/5055] Running Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes (+ 16 more⣯ [355/5055] Running Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes (+ 16 more⣟ [355/5055] Running Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes (+ 16 more⡿ [355/5055] Running Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes (+ 16 more⢿ [355/5055] Running Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes (+ 16 more⣻ [355/5055] Running Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes (+ 16 more⣽ [355/5055] Running Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes (+ 16 more✖ [423/7128] Building Batteries.Data.String.Lemmas
trace: .> LEAN_PATH=C:\Users\pufre\Downloads\CodingProjects\utm-leannotes\.lake\packages\Cli\.lake\build\lib\lean;C:\Users\pufre\Downloads\CodingProjects\utm-leannotes\.lake\packages\proofwidgets\.lake\build\lib\lean;C:\Users\pufre\Downloads\CodingProjects\utm-leannotes\.lake\packages\importGraph\.lake\build\lib\lean;C:\Users\pufre\Downloads\CodingProjects\utm-leannotes\.lake\packages\LeanSearchClient\.lake\build\lib\lean;C:\Users\pufre\Downloads\CodingProjects\utm-leannotes\.lake\packages\plausible\.lake\build\lib\lean;C:\Users\pufre\Downloads\CodingProjects\utm-leannotes\.lake\packages\auto\.lake\build\lib\lean;C:\Users\pufre\Downloads\CodingProjects\utm-leannotes\.lake\packages\batteries\.lake\build\lib\lean;C:\Users\pufre\Downloads\CodingProjects\utm-leannotes\.lake\packages\aesop\.lake\build\lib\lean;C:\Users\pufre\Downloads\CodingProjects\utm-leannotes\.lake\packages\Duper\.lake\build\lib\lean;C:\Users\pufre\Downloads\CodingProjects\utm-leannotes\.lake\packages\premise-selection\.lake\build\lib\lean;C:\Users\pufre\Downloads\CodingProjects\utm-leannotes\.lake\packages\Qq\.lake\build\lib\lean;C:\Users\pufre\Downloads\CodingProjects\utm-leannotes\.lake\packages\Hammer\HammerCore\.lake\build\lib\lean;C:\Users\pufre\Downloads\CodingProjects\utm-leannotes\.lake\packages\mathlib\.lake\build\lib\lean;C:\Users\pufre\Downloads\CodingProjects\utm-leannotes\.lake\packages\Hammer\.lake\build\lib\lean;C:\Users\pufre\Downloads\CodingProjects\utm-leannotes\.lake\build\lib\lean c:\Users\pufre\.elan\toolchains\leanprover--lean4---v4.24.0\bin\lean.exe C:\Users\pufre\Downloads\CodingProjects\utm-leannotes\.lake\packages\batteries\Batteries\Data\String\Lemmas.lean -o C:\Users\pufre\Downloads\CodingProjects\utm-leannotes\.lake\packages\batteries\.lake\build\lib\lean\Batteries\Data\String\Lemmas.olean -i C:\Users\pufre\Downloads\CodingProjects\utm-leannotes\.lake\packages\batteries\.lake\build\lib\lean\Batteries\Data\String\Lemmas.ilean -c C:\Users\pufre\Downloads\CodingProjects\utm-leannotes\.lake\packages\batteries\.lake\build\ir\Batteries\Data\String\Lemmas.c --setup C:\Users\pufre\Downloads\CodingProjects\utm-leannotes\.lake\packages\batteries\.lake\build\ir\Batteries\Data\String\Lemmas.setup.json --json
error: Batteries/Data/String/Lemmas.lean:6:0: object file 'c:\Users\pufre\.elan\toolchains\leanprover--lean4---v4.24.0\lib\lean\Std\Classes\Ord\String.olean' of module Std.Classes.Ord.String does not exist
error: Lean exited with code 1
⣯ [531/7312] Running Batteries.Classes.Deprecated (+ 16 more)

here is my lake toml:

name = "utm-leannotes"
version = "0.1.0"
defaultTargets = ["utm-leannotes"]

[[lean_lib]]
name = "UtmLeannotes"

[[lean_exe]]
name = "utm-leannotes"
root = "Main"


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

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

[Kim Morrison]

This may be on @Josh Clune's radar, or maybe you could try the upgrade yourself.

[Frederick Pu]

wdym by try the upgrade

[Frederick Pu]

like patch lean hammer?

[Josh Clune]

It is on my radar (sorry for the delay). Most of LeanHammer’s dependencies have been updated to v4.24.0, but there’s been a delay in updating the premise selection server because the compute cluster we use for training was temporarily down. I can send another message in this thread once the whole of LeanHammer has been updated to be compatible with v4.24.0.

[Josh Clune]

LeanHammer has been updated to v4.24.0. Apologies again for the delay.

[Kim Morrison]

Great. @Josh Clune (also cc @Patrick Massot as they've requested this), what do you think about creating a LeanHammer branch of Mathlib, which adds LeanHammer as a require statement?

You can follow #30953 (trying to add Canonical) or #29953 (successfully adding Reap) as models to see what needs to be done.

You will need to start the branch from v4.24.0 tag of Mathlib, as I see that auto (at least) is incompatible with v4.25.0-rc2.

We know from experience that there are non-trivial integration problems getting these packages working with Mathlib. I expect LeanHammer is going to be even harder than these, but we need to be trying!

[Josh Clune]

I should have some time later this week to look into this. I can send an update once I do to let you know how it goes.

[Kim Morrison]

Oh, I realised a difficulty you will run into: you will need to merge something like #30952 to master first, but master is already on v4.25.0-rc2. I guess you can make the analogue of #30952 now, and then be able to proceed once v4.25.0 lands and you've updated everything to that. Or, get a head start and update everything to v4.25.0-rc2 right now, so you can work with Mathlib master.

[Frederick Pu]

does lean hammer have any .so files cause @Dhyan Aranha and I are running into an issue integrating it into lean repl and im not sure what the source of it is

[Siddhartha Gadgil]

@Kim Morrison It is very nice to have all these branches (LeanHammer, Reap etc) but what is the intended solution if one wants more than one of these? Should there be a AI branch?

[Kim Morrison]

These branches are mostly intending as staging, to work out what engineering work is still needed to make any of these usable. Currently only reap is usable with Mathlib.

My hope is that these branches will actually be merged to master.

[Josh Clune]

Frederick Pu said:

does lean hammer have any .so files cause Dhyan Aranha and I are running into an issue integrating it into lean repl and im not sure what the source of it is

Some of LeanHammer's dependencies require precompileModules := true to operate efficiently. I believe that .so and .dylib files can be generated by lake as a consequence of that.

[Josh Clune]

Kim Morrison said:

Great. Josh Clune (also cc Patrick Massot as they've requested this), what do you think about creating a LeanHammer branch of Mathlib, which adds LeanHammer as a require statement?

Update on this: I've made some headway towards this goal. I have a local build of mathlib which depends on LeanHammer where it's possible to experiment anywhere in mathlib just by adding import Hammer. I've also added github workflows so that starting from v4.25.0, users shouldn't need to rebuild/recompile the hammer locally. Further progress, and in particular, a PR analogous to #30953 or #29953 that successfully passes mathib's CI checks, will probably have to wait until v4.25.0 lands.

[Kim Morrison]

@Josh Clune, could you arrange, like in the canonical branch, so that import Hammer happens in Mathlib.Tactic.Common, please?

[Kim Morrison]

In the meantime you'll also need to make a PR analogous to #30818 in order for CI to be able to upload LeanHammer oleans.

[Josh Clune]

Kim Morrison said:

Josh Clune, could you arrange, like in the canonical branch, so that import Hammer happens in Mathlib.Tactic.Common, please?

Yes, I've already done so. You can see the PR here, though it currently fails CI due to differences between v4.24.0 and v4.25.0-rc2 (locally, it builds fine so long as lake update is not used to modify the lake-manifest or lean-toolchain files).

Kim Morrison said:

In the meantime you'll also need to make a PR analogous to #30818 in order for CI to be able to upload LeanHammer oleans.

Happy to do this, though I'm a bit unclear how exactly isPartOfMathlibCache works and how to extend it to support LeanHammer. In particular, I'm unclear whether I should be adding:

• Just the name `Hammer
• The set of projects that LeanHammer depends on which have precompileModules set to true
• The set of all projects that LeanHammer depends on, regardless of how precompileModules is or isn't set

[Kim Morrison]

The last of those.

[Josh Clune]

Okay, thanks for the clarification. #31327 should do it.

[Josh Clune]

Josh Clune said:

You can see the PR here, though it currently fails CI due to differences between v4.24.0 and v4.25.0-rc2 (locally, it builds fine so long as lake update is not used to modify the lake-manifest or lean-toolchain files).

Update on this: LeanHammer has been updated to v4.25.0, resolving the issue that was previously preventing the CI from building. However, the PR now is encountering a different error in which the exception unknown module prefix 'PremiseSelection' is being thrown during the Attempting to fetch olean for Mathlib/Init.lean from cache... phase of the CI. This appears to be because .lake/packages/premise-selection is not being included as part of the phase's LEAN_SRC_PATH, though I'm unclear as to why this is the case (Duper, Auto, and LeanHammer's other dependencies are being added to this LEAN_SRC_PATH without issue). For additional context, #31327 was successfully merged and the branch the PR is based on builds locally without issue, so I don't know how to troubleshoot this. If you have any thoughts as to what might be causing this issue, please let me know and I'd be happy to look further into it.