Implement Lean 4 support #76

insightmind · 2021-12-09T01:38:42Z

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.

alectryon/docutils.py

alectryon/lean4.py

alectryon/literate.py

cpitclaudel · 2021-12-09T04:07:08Z

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 · 2021-12-09T04:10:29Z

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.

alectryon/core.py

recipes/literate_lean4.lean

Kha · 2021-12-09T11:07:53Z

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 · 2021-12-23T01:27:54Z

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 · 2022-02-11T13:38:15Z

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

Slightly later ping :)

cpitclaudel

This looks excellent! I've been delaying this review for much too long because I thought it'd need quite a bit of time, and it took just 30 minutes to go through everything. Congrats!!

I left a few small comments. None of them should be time consuming to fix up.

Have you run the code through make lint to see if any complaints pop up?

Also, let's update the changelog, and make a release soon after we merge this.

Again, exceptional work! Thanks :)

cpitclaudel · 2022-02-28T01:13:13Z

alectryon/cli.py

@@ -378,6 +378,7 @@ def write_file(ext, strip):

 EXTENSIONS_BY_LANGUAGE = {
    "coq": (".v",),
+    "lean4": (".lean",),
    "lean3": (".lean", ".lean3"),


With .lean appearing under both lean3 and lean4 lists the CODE_EXTENSIONS list below will contain .lean twice, which may cause issues. A quick review suggests that CODE_EXTENSIONS could simply be turned into a set. We should review other uses of EXTENSIONS_BY_LANGUAGE, too, like in the definition of FRONTENDS_BY_EXTENSION. It may be enough to remove the lean3 entry from that explicitly after constructing the list.

Would removing the .lean extension from the .lean3 case be enough?

Yes, let's do that.

Ok, adjusted it.

README.rst

alectryon/cli.py

cpitclaudel · 2022-02-28T01:42:43Z

alectryon/docutils.py

+    .. lean4::
+
+        #check Nat
+


Let's remove these three examples; that will be one less spot to update when we add other languages

alectryon/docutils.py

alectryon/lean4.py

cpitclaudel · 2022-02-28T01:46:33Z

alectryon/lean4.py

+
+    def annotate(self, chunks):
+        document = EncodedDocument(chunks, "\n", encoding="utf-8")
+        self.resolve_lake_arg()


Is this function needed now that there is a top-level argument this file?

Yeah, it is required in order for us to figure out the working directory of LeanInk so all external references are loaded correctly. This behavior is partially handled by the Lean 4 driver.

cpitclaudel · 2022-02-28T01:46:51Z

alectryon/lean4.py

+        self.resolve_lake_arg()
+        result = self.run_leanInk_document(document)
+
+        if not result:


What does this case correspond to?

It's a guard statement to prevent an error that would happen when accessing the last element of an empty array.

cpitclaudel · 2022-02-28T01:47:27Z

alectryon/lean4.py

+        last = result[-1]
+
+        # Sometimes we require an additonal \n and sometimes not. I wasn't really able to
+        # find out exactly when, but this workaround seems to work for almost all cases.


Would it work to ensure that there's a newline at the end of every fragment?

I'm not sure if that is enough or correct tbh because we can't be sure if a single newline at the end of a fragment is enough, for example if we have a fragment that has two or more new lines at the end.
However LeanInk should ensure that fragments are generated so that there are no missing characters in between them, so these cases shouldn't be an issue.

I suspect that either the encoding or decoding process of LeanInks input or output causes the issue, or the Lean compiler trims the end of the file in some cases, which would cause the missing new line character.

recipes/_output/literate_lean4.lean.rst

insightmind · 2022-03-07T23:33:02Z

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?

alectryon/literate.py

recipes/literate_lean4.lean

cpitclaudel

OK, a few very minor things, and I think we're ready to merge :) Thanks again for this excellent work!

README.rst

Changes the literate opening token from `/-|` to `/-!`.

cpitclaudel · 2022-06-12T02:30:49Z

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 · 2022-06-12T02:31:31Z

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 · 2022-06-18T11:17:18Z

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

insightmind changed the title ~~WIP: Implement Lean 4 support~~ Implement Lean 4 support Dec 9, 2021

cpitclaudel reviewed Dec 9, 2021

View reviewed changes

alectryon/docutils.py Outdated Show resolved Hide resolved

cpitclaudel reviewed Dec 9, 2021

View reviewed changes

alectryon/lean4.py Outdated Show resolved Hide resolved

cpitclaudel reviewed Dec 9, 2021

View reviewed changes

alectryon/literate.py Show resolved Hide resolved

Kha reviewed Dec 9, 2021

View reviewed changes

alectryon/core.py Outdated Show resolved Hide resolved

recipes/literate_lean4.lean Outdated Show resolved Hide resolved

insightmind marked this pull request as ready for review December 15, 2021 19:19

insightmind requested a review from cpitclaudel December 23, 2021 01:27

cpitclaudel approved these changes Feb 28, 2022

View reviewed changes

Kha reviewed Mar 26, 2022

View reviewed changes

alectryon/literate.py Outdated Show resolved Hide resolved

cpitclaudel reviewed Apr 3, 2022

View reviewed changes

recipes/literate_lean4.lean Show resolved Hide resolved

cpitclaudel approved these changes Apr 3, 2022

View reviewed changes

README.rst Outdated Show resolved Hide resolved

README.rst Outdated Show resolved Hide resolved

README.rst Outdated Show resolved Hide resolved

README.rst Outdated Show resolved Hide resolved

README.rst Outdated Show resolved Hide resolved

insightmind added 13 commits June 11, 2022 18:54

lean4: Initial import

601174b

lean4: Propagate lean chunks to leanInk

d2b1d6d

literate: Add basic LEAN4 LangDef

fc46803

docutils: Define RSTLean4Parser

56c564a

transforms: Add first few lean4 transforms

26fc587

lean4: Make Lean4 driver workable

48b2100

lean4: Decode LeanInk result

f14e2b3

cli: Forward lakefile to Lean4 driver

64dd444

lean4: Use lakefile location as working directory

118b54e

lean4: Set working directory in CLIDriver.run_cli

8fe8862

cli: Forward --debug to leanInk

cc1b6db

lean4: Recover chunks after leanInk analysis

e8d8822

recipes: Add literate_lean4.lean recipe

0a98b93

insightmind added 18 commits June 11, 2022 18:54

lean4: Fix compilation of files with non-.lean extension

1b84b41

literate: Add .lean extension to standalone CLI

42cce17

readme: Document Lean 4 support

f361226

lean4: Remove outdated TODO comments

b427d02

lean4: Fix recover_chunks failing due to missing \n

83bc346

lean4: Apply review comments

6ce97cd

lean4: Work around missing \n in last chunk

17489e1

literate: Change lean4 close tag from |-/ to -/

d0c57e3

recipes: Add Lean4 examples

a5918d2

lean4: Fix linter warnings

02552c0

readme: Move lean 4 chapter above lean 3 chapter

fa21b9b

docutils: Remove language examples from module docstring

0556561

lean4: Add transforms for nested tactics support

8f68de2

recipes: Use Lean 4 in polyglot.rst

57fabe5

literate: Adjust Lean 4 opening token

53f7248

Changes the literate opening token from `/-|` to `/-!`.

cli: Remove .lean inferred extension for Lean 3

35d044c

readme: Apply review comments

5c01921

literate: Adjust Lean 3 literate opening token

032166f

cpitclaudel force-pushed the lean4 branch from 2fff628 to 032166f Compare June 12, 2022 02:22

cpitclaudel merged commit 032166f into cpitclaudel:master Jun 12, 2022

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Implement Lean 4 support #76

Implement Lean 4 support #76

insightmind commented Dec 9, 2021 •

edited

Loading

cpitclaudel commented Dec 9, 2021

cpitclaudel commented Dec 9, 2021

Kha commented Dec 9, 2021

insightmind commented Dec 23, 2021

Kha commented Feb 11, 2022

cpitclaudel left a comment

cpitclaudel Feb 28, 2022

insightmind Mar 7, 2022

cpitclaudel Apr 3, 2022

insightmind Apr 4, 2022

cpitclaudel Feb 28, 2022

insightmind Mar 7, 2022

cpitclaudel Feb 28, 2022

insightmind Mar 7, 2022

cpitclaudel Feb 28, 2022

insightmind Mar 7, 2022

cpitclaudel Feb 28, 2022

insightmind Apr 4, 2022

insightmind commented Mar 7, 2022

cpitclaudel left a comment

cpitclaudel commented Jun 12, 2022

cpitclaudel commented Jun 12, 2022

Kha commented Jun 18, 2022

Implement Lean 4 support #76

Implement Lean 4 support #76

Conversation

insightmind commented Dec 9, 2021 • edited Loading

General

Usage

Lean code files

Literate files

New Recipes

Important notes

Feedback

cpitclaudel commented Dec 9, 2021

cpitclaudel commented Dec 9, 2021

Kha commented Dec 9, 2021

insightmind commented Dec 23, 2021

Kha commented Feb 11, 2022

cpitclaudel left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

insightmind commented Mar 7, 2022

cpitclaudel left a comment

Choose a reason for hiding this comment

cpitclaudel commented Jun 12, 2022

cpitclaudel commented Jun 12, 2022

Kha commented Jun 18, 2022

insightmind commented Dec 9, 2021 •

edited

Loading