Lean prelude doesn’t build on Lean 4.22.0-rc2; case tags mismatch (inv1)

[klausnat]

Hi!

I’m trying to use the hax Lean backend as part of a Rust→hax→Lean verification pipeline, and I need to build the hax Lean prelude against Lean leanprover/lean4:v4.22.0-rc2 (this is the toolchain pinned by CompPoly / mathlib stack in our environment).

Problem: the hax Lean prelude fails to compile on Lean 4.22.0-rc2.

Error (minimal):

error: HaxLib/Hax/Lib.lean:540:2: Case tag 'inv1' not found.
Available tags: 'inv', 'step', 'pre1', 'post.success', 'post.except'
error: HaxLib/Hax/Lib.lean:582:2: Case tag 'inv1' not found.
Available tags: 'inv', 'step', 'pre1', 'post.success', 'post.except'

I also attempted a local patch replacing inv1 with inv, but then Lean reports additional tag mismatches (vc1.step, vc2.pre) and an “invalid constructor ⟨...⟩” error, suggesting a broader incompatibility with the Std.Do.Triple cases/tags in 4.22.

Reproduction steps:

• Use toolchain leanprover/lean4:v4.22.0-rc2
  

• Add the hax Lean prelude (proof-libs/lean) to a lake project as a lean_lib
  

• Run lake build → fails in Hax/Lib.lean with the errors above.
  

Question: is there a pinned Lean version / tag of the hax Lean prelude that is known to work with Lean 4.22.*, or should we treat Lean 4.22 support as WIP?

Happy to provide a minimal repo reproducer if helpful.

[maximebuyse]

Hi!
We are pinned to 4.23 since #1696. The lean backend is evolving fast so using a version from 3 months ago will probably be quite limiting.
We have seen a big sensitivity to lean versions so we made the decision to support only one lean version, so it is probably more work than you would like to make the current hax compatible with both 4.22 and 4.23.
Unfortunately this means we don't have an easy solution for your problem, maybe @abentkamp will have more suggestions on Monday.

[klausnat]

Thank you, this makes sense.

[abentkamp]

Hi @klausnat,

I have tried to make the library work with 4.22.0-rc2 just now, but the error you reported is not the only one I ran into. It's just too much work for us to support old versions of Lean.

I would be happy to upgrade to newer versions, though, if this is an option for you. Maybe CompPoly could be upgraded to newer versions as well? If we all keep upgrading from time to time, this also has the advantage that we can benefit from the latest Lean and Mathlib changes.

[klausnat]

Hi @abentkamp,

Yes, newer versions would be good and they have the goal of updating ArkLib too, to 4.26.0, so if we can get hax to 4.26.0 we may have some stability for the workflow.

What do you think about 4.26.0 ?

[abentkamp]

Sounds great, I will start working on it.

[dhsorens]

just want to second this request @abentkamp , thanks!! we're looking to update some of our specs in https://github.com/Verified-zkEVM to 4.26.0 soon and would love to be able to use the Hax backend with those specs, all on the same version :)

[abentkamp]

Sorry, while upgrading I discovered this bug in mvcgen: leanprover/lean4#12048
It's fixed now, but it will take a while until there is an official Lean release with this bug fix. I tried to work around it, but could not make it work.

So here is my suggestion: As soon as the bug fix is released in a nightly, I will create a Hax branch depending on that nightly. Would that work for you?

[abentkamp]

Okay, I found a way to work around it now: #1880

Not sure if we want to merge this, though. It's not pretty and there might be more places where I would need to work around the bug.

[klausnat]

Okay if you think it is not a good idea to merge... please work on your own schedule and merge when you think it's ready. The main goal is to ensure all three projects can eventually fit together into a unified pipeline.

Let me discuss it with team

[klausnat]

we can run Hax from your branch for now!

[abentkamp]

@klausnat The latest release candidate of Lean has the bug fix we needed. So here is a PR for Lean v4.28.0-rc1: #1900. I assume we can merge this soon.