Format Lean

Stream: general

[Eyesomorphic]

Is the library 'Format lean' here still in active development? I can't seem to get it to work on windows. After I follow the steps, no binaries are produced :(

[Eyesomorphic]

If there's any newer method of performing the same thing (Converting a lean file with comments into an interactable html file or similar), I'd love to hear about them!

[Kim Morrison]

Your link is misformatted. You meant https://github.com/leanprover-community/format_lean

[Kim Morrison]

This is definitely not actively developed. :-)

[Kim Morrison]

In particular it is for Lean 3, which is end of life.

[Eyesomorphic]

Scott Morrison said:

Your link is misformatted. You meant https://github.com/leanprover-community/format_lean

Ah thank you, I didn't notice it was Lean 3! Would you happen to know of any Lean 4 alternatives?

[Mario Carneiro]

I think this project was never really completed, but @Patrick Massot will know best what state it is in

[Patrick Massot]

It was completed in the sense that it did everything I need it to do. But it was indeed a Lean 3 thing. Verso should become a Lean 4 version of this and much more.

[Mario Carneiro]

Is this the same project as the one you demoed here? I thought it was but maybe this is something else

[Mario Carneiro]

As far as I know this project was never properly released

[Patrick Massot]

No, this has nothing to do with this.

[Patrick Massot]

We are talking about a quick hack I wrote 5 years ago for my lecture notes.

[Patrick Massot]

It’s the tool that created https://www.imo.universite-paris-saclay.fr/~patrick.massot/mdd154/

[Patrick Massot]

(go to the bottom of that web page)

[Mario Carneiro]

ah yes, I can see why you say verso would replace it now

[Patrick Massot]

It shows Lean code with human generated comments and the tactic state