Literate programming in Lean4 / Lean4 + Org mode

Stream: lean4

[Anand Rao]

Is there currently a way to do literate programming in Lean4, maybe using something like Org mode? I suspect that getting the full info-view working in a literate programming environment will be a challenge, but I was wondering if it there is a way to just have some code blocks and run #eval for the time being.

[Sebastian Ullrich]

Alectryon has support for switching between code-in-reST and reST-comments-in-code, and there is a Lean 4 backend in development: https://github.com/insightmind/LeanInk

[Anand Rao]

Okay, thank you. I will look into LeanInk.

[Patrick Massot]

What are the latest news about LeanInk? Is it close to implementing everything that was planned?

[Sebastian Ullrich]

Yes!

[Daniel Fabian]

@Sebastian Ullrich please fix the broken link on the homepage for the repo. :-P In the usage section, the example json points to nowhere: https://github.com/insightmind/LeanInk/blob/main/LeanInk/Output/Alectryon.lean

[Patrick Massot]

Does it allow links between files or is it still a single Lean file tool?

[Sebastian Ullrich]

No, there is no support for links of any kind yet in Alectryon https://github.com/cpitclaudel/alectryon/issues/27. We considered it, but we had to make a cut somewhere for a bachelor's thesis.

[Patrick Massot]

I understand the cut need. That's why I wrote this morning "Is it close to implementing everything that was planned?". I don't want to miss the time where I'll need to pester someone else to continue that job. But I don't want to do it too early because I don't want to interfere with the thesis.

[Sebastian Ullrich]

I met with @Niklas Bülow today and we are definitely open to external contributions at this point. We will likely transfer ownership of the repo when the thesis is done.

[Patrick Massot]

Great! Is the documentation up to date?

[Sebastian Ullrich]

Niklas did at least fix the wrong link Dany noticed just now :) . If anything else is wrong or missing, best open an issue for it. But the most thorough documentation will of course be the thesis itself, which will take a few more weeks.

[Patrick Massot]

Ok, I'll probably wait for the thesis then.

[Arthur Paulino]

This is a rather simple and rudimentary script (not specific to Lean 3 nor 4), but worth mentioning in case it's enough for you:
https://github.com/Julian/lftim/blob/main/lean2md.py
It turns this into this. So you can write the Lean code in your preferred Lean env