Incompatible Lean Version

[Oscario0]

• Noticed Loom is ran on Lean4:v4.23
• I currently run v4.25.0-rc2
• Could we please update the toolchain file.
• Also, could we make this a recurring event when Lean Zulip puts out another version lean4? So that this issue does not get raised repeatedly.

[alok]

huh, this is the sorta thing that claude code in ci would be good for (like a nightly run).

…

On Fri, Dec 19, 2025 at 3:02 PM Oscar M ***@***.***> wrote: *Oscario0* created an issue (verse-lab/loom#28) <#28> - Noticed Loom is ran on Lean4:v4.23 - I currently run v4.25.0-rc2 - Could we please update the toolchain file. - Also, could we make this a recurring event when Lean Zulip puts out another version lean4? So that this issue does not get raised repeatedly. — Reply to this email directly, view it on GitHub <#28>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AB7QUTGCZMGBOLJ3P4UBSLL4CR7WTAVCNFSM6AAAAACPSY6RNOVHI2DSMVQWIX3LMV43ASLTON2WKOZTG42DSMJXGI2TOOA> . You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

[Oscario0]

Ohh, good idea.

[alok]

Hmm maybe lean-action should have a script for that, to help out the community at large. There’s a pr for a Claude tactic in the compiler rn.

…

On Fri, Dec 19, 2025 at 16:25 Oscar M ***@***.***> wrote: *Oscario0* left a comment (verse-lab/loom#28) <#28 (comment)> Ohh, good idea. — Reply to this email directly, view it on GitHub <#28 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AB7QUTBTALGQCTNXB7H26CT4CSJO5AVCNFSM6AAAAACPSY6RNOVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZTMNZXGA3TKMBQHA> . You are receiving this because you commented.Message ID: ***@***.***>

[Oscario0]

i created a PR for this issue, there may be some incompatibilities that I can't touch though, if the merge is accepted

[Oscario0]

@alok do you mind reviewing some of my changes?

[alok]

Sure. Links?

[volodeyka]

Hey @Oscario0 and @alok. Sorry for a super late response, I was on vacation and immediately after that was travelling for the conference. Also, many things are happening right now -- we are planning a major rewrite and releasing Velvet 2.0 in a different repo in the future, that's why support for this repo is kinda low now.
That's said, I am in the middle of updating this repo to v4.27 -- it requires fixing metatheory. Planning to ship it next week.

[Oscario0]

@alok sent