Implement Lean 4 support

[insightmind]

General

This pull request adds support for Lean 4 using LeanInk.

In order to do so, it introduces a new driver lean4.py for handling communication between Alectryon and LeanInk. LeanInk takes a .lean file as its input and analyzes it using direct access to the Lean 4 compilers AST. It returns an output file that contains all fragments (Text and Sentences) in Alectryon's json format.

Usage

Lean code files

Lean 4 usage is equivalent to any other supported language. You can use the lean4 or lean4+rst driver to explicitly specify Lean 4. With this PR .lean files will also automatically be inferred as Lean 4 files instead of Lean 3.

alectryon --frontend lean4 plain-lean4.lean

To print the debug output of LeanInk you can do the following:

alectryon --frontend lean4 plain-lean4.lean --debug

If you want to use Alectryon with a Lean 4 file that uses the Lake package manager you can provide the lakefile to Alectryon:

alectryon --frontend lean4 plain-lean4.lean --lake lakefile.lean

Literate files

Lean 4 is also supported in literate files using the lean4:: directive for reStructuredText and {lean4} for MyST markdown files.

Finally we also added a short explainer section about Lean 4 support in the readme.

New Recipes

We have added a few new recipes to test and showcase the Lean 4 support:

• plain-lean4.lean
• literate-lean4.lean
• lean4-tactics.rst
• lean4-tactics-myst.md

These files make up most of the added files.

Important notes

To support Lean 4 we had to make minor changes to the implementation of Lean 3 support. We renamed the recipe plain.lean to plain-lean3.lean. Additionally .lean files will automatically be inferred as Lean 4 files instead of Lean 3 because it has a higher precedence.

Feedback

Feedback on the implementation is always welcome. Especially if you can spot rough issues or find features that are not yet supported.

Most line additions are due to new recipe files. If you take a look at the python files, the actual implementation is very small.

[cpitclaudel]

Excellent work @insightmind! I will make a detailed review this week-end, most likely on Sunday (please ping me Saturday evening if you haven't heard back by then). I just had a quick read-through and everything looks very reasonable, so I don't think there will be much to change before merging :)

[cpitclaudel]

Btw, since Lean support line comments, we could consider using line comments for literate programming in Lean. That's how I did it in F* a while back, see https://github.com/FStarLang/fstar-mode.el/tree/master/etc/fslit/ . If you think that would be a good fit for Lean then we could import the state machine from fslit.

Oh, and feel free to suggest something better than /-|, I chose the | in Coq because it was relatively easy to type with (* and because (**, (*!, and (*+ were already taken.

[Kha]

Oh, and feel free to suggest something better than /-|, I chose the | in Coq because it was relatively easy to type with (* and because (**, (*!, and (*+ were already taken.

I don't mind /-|, though for consistency with docstrings /-- ... -/ and module docstrings /-! ... -/, it would be nice to use plain -/ as the terminator.

[insightmind]

Btw, since Lean support line comments, we could consider using line comments for literate programming in Lean. That's how I did it in F* a while back, see https://github.com/FStarLang/fstar-mode.el/tree/master/etc/fslit/ . If you think that would be a good fit for Lean then we could import the state machine from fslit.

Oh, and feel free to suggest something better than /-|, I chose the | in Coq because it was relatively easy to type with (* and because (**, (*!, and (*+ were already taken.

We discussed the idea recently and came to the conclusion that multiline comments are a better fit for Lean. The reason we think so is that Lean already supports docstrings and module docstrings, as described above, using multiline comments. Literate programming using multiline comments is therefore more consistent with the current language.

[Kha]

please ping me Saturday evening if you haven't heard back by then

Slightly later ping :)

[insightmind]

Thank you so much for your thorough review.

I resolved the linter warnings, and adjusted the code based on your review + responded to the comments.

I have also added two new transforms in the transform.py file for Lean 4. This is because of a recent change within LeanInk to support nested tactics. Therefore I also regenerated the output files of all Lean 4 recipe examples.

Also let me know if there's anything else that might need some adjustments.

P.S.: Do you want to update the changelog after the merge or should I already update it in this PR?

[cpitclaudel]

Hi folks, I finally found the time to go through the PR for a final cleanup, and to merge it! :) I had to rebase a few things, so I saved a copy of the unrebased branch to lean4-before-rebase in this repository.

@insightmind , big congratulations! :) And @Kha and @insightmind , thanks both a lot for your patience.

@insightmind , I've sent you an invitation to get you the commit bit, so if you want to make further changes to the lean part you should feel free to either make a PR or push directly to master.

Cheers!

[cpitclaudel]

I've installed Lean4 locally to test things, so I'm fairly confident that they work, but I'd love a last go-ahead from either of you before I make a release ^^

[Kha]

diff says output is unchanged on the Lean 4 doc examples, looks good :)