LeanInk kept up to date?

Stream: lean4

[McCoy R. Becker]

Is LeanInk being kept up with stable Lean? Wonder if anyone has any tricks for getting this to work (LeanInk, for alectryon) -- or if I should be considering something else for "literate Lean" files

I'm on e.g. up-to-date Lean4 stable (v4.4.0) which is now ahead of LeanInk for alectryon.

[Mario Carneiro]

no, I think it is not being maintained unfortunately

[McCoy R. Becker]

unfortunate. alectryon + leanink is the closest tool I've seen for literate style Lean tutorials

[McCoy R. Becker]

Successfully got it working on stable with some elbow grease :laughing:

[Utensil Song]

v4.4.0 has some breaking changes that require upgrading LeanInk, and I have a PR to address this and using it. Glad to learn there are other interested users, and my personal goal is to keep it working for my personal project (very casual, not very strict so it works fine for my simple use cases) and fix serious issues reported by interested users if I can (so, no promises, and I hope someone with more serious use case could revive it further).

Also note that doc-gen4 uses an older version of LeanInk and works fine for the part it depends on, but rendering annotated Lean code is not part of it (disabled).

See leanprover/LeanInk#55 and more discussions here.