Evaluate Alectryon extensibility about leanink HOT 11 CLOSED

The current implementation of Alectryon's json support seems limited:
Following features are allowed using json format:

• minimal json format (each line of coq program as entry of json, basically array of program lines) -> evaluated json format (each line evaluated with tactics, goals, etc.)

• (min or eval) json format -> snippets-html (each evaluated coq line is presented in <pre> tags, with usually hints, etc. from alectryon)

• (min or eval) json format -> snippets-latex (similar to html, just with latex)

from leanink.

There are two starting points on how to implement the interaction with LeanInk. We'll maybe use both for best user experience.

1. Add a new frontends for lean4 in Alectryon. This frontend will call LeanInk to analyze portions/excerpts of Lean4 and return the hints and tactics for Alectryon to generate the webpage. As the current json format is a bit restricted for use, we either define our own interaction protocol between Alectryon and LeanInk or extend the current json format.

2. Implement a generate command for LeanInk to use LeanInk as the main interface for generation. As we do not want to implement the html, etc. generation ourselves, LeanInk would call Alectryon and help it with the analysis of the Lean4 code. There are two ways to help Alectryon here:

• We may analyze the Lean4 code before calling Alectryon. The downside of this would be that we have to implement our own parsing for .rst and .md files. Additionally we would need to find a way to tell Alectryon a mapping between evaluation info and the individual code snippets.
• Similar to 1. we would simply call the respective frontend of Alectryon and let it summon another instance of LeanInk.

from leanink.

I would suggest using option 1. + 2.2, for the initial prototype. Clearly we would recommend the interface for Lean users to use our CLI for generation. We may also want to allow LeanInk to be used within other LeanInk programs, which should be easily possible with Lake as a dependency manager.

from leanink.

Interesting note: Alectryon uses pygments for syntax highlighting.

from leanink.

Files we have to adjust/add functionality to, so Alectryon supports Lean4:

• Create lean4.py for our custom Lean 4 driver. This is basically just an interface that communicates with LeanInk and sends LeanInk the file for analysis. Probably the easiest to just tell LeanInk the FilePath to the .lean file. We actually get chunks of the file here. We could get the whole file if we adjust the pipeline for lean4 in cli.py, we could also write the chunks to a fresh file instead.
• cli.py register the new frontend lean4 and update add new pipelines if necessary. We must also decide how we make sure Alectryon chooses the right lean frontend when given a .lean file.
• transform.py needs some transforms ??? I actually did not dig deep into what transform do and why they are used but, we should probably have to do something here as well
• literate.py we need a converter for .rst to .lean (Lean 4) and the other way around. For the latter they implement a simple Lean parser.
• docutils.py some smaller adjustments to Pipeline APIs?
• pygments... for syntax highlighting

from leanink.

* We actually get `chunks` of the file here.

That's all the chunks at once, right? Then passing that list (e.g. as JSON) to LeanInk, fully processing it there, and then writing back the results seems like the most robust solution to me, if we don't want to e.g. parse .rst ourselves.

from leanink.

* We must also decide how we make sure Alectryon chooses the right lean frontend when given a `.lean` file.

I'd say let's just always assume Lean 4 for now. Lean 4 might be much closer to supplanting Lean 3 when we are done.

from leanink.

* We actually get `chunks` of the file here.

That's all the chunks at once, right? Then passing that list (e.g. as JSON) to LeanInk, fully processing it there, and then writing back the results seems like the most robust solution to me, if we don't want to e.g. parse .rst ourselves.

Yeah exactly.

If we provide Alectryon a simple .lean code file, then the driver will get a single chunk with the whole source code of the file. However if we provide a preprocessed .json or some .rst file or so it may split up some parts of it into separate chunks, tho every chunk is expected to be a valid .lean program.

In the case of an .rst file every chunk we get is a literate code block. So if we want them to be analyzed as a whole, because they may have common definitions and depend on each other, we could also merge all chunks into a single chunk, which we then write to a .lean file we can analyze directly instead of using .json as an intermediate format. This is actually the approach Alectryon uses in the coqc driver.
The benefits of this are that we don't need to care about all the escaping stuff in json (ideally this is already solved by the json library in Python and Lean 4), as well as that LeanInk can actually use independent .lean files as inputs instead of a special format.

from leanink.

* We must also decide how we make sure Alectryon chooses the right lean frontend when given a `.lean` file.

I'd say let's just always assume Lean 4 for now. Lean 4 might be much closer to supplanting Lean 3 when we are done.

Does Lean 4 support the .lean4 extension similar to Lean 3 .lean3?

from leanink.

This is actually the approach Alectryon uses in the coqc driver.

I see, then I suppose it should work for us as well. I had imagined that it would make transforming positions back to the source document harder.

from leanink.

Does Lean 4 support the .lean4 extension similar to Lean 3 .lean3?

Unfortunately no, they both use .lean only.

from leanink.