Zulip Chat Archive

Stream: general

Topic: VSCode Lean Notebook API

Naveen (Jun 26 2021 at 08:01):

https://leanprover.zulipchat.com/#narrow/stream/113486-announce/topic/Alectryon.20port.20summer.20project/near/243955447

Hi,
From what I understand, Alectryon is analogous to Python's version of Jupyter Notebooks, but here, an interactive way to read and verify proofs. If this is the case, VS Code now has a notebook API, which I think is fairly easy to integrate using Lean LSP just to provide this kind of functionality. And exporting to web shouldn't be a difficult process from here.

Naveen (Jun 26 2021 at 08:12):

I also see, there are already attempts for literate style of Lean

Last updated: Dec 20 2023 at 11:08 UTC