Additional architectural overview of the lean ecosystem #468
Description
What question should the reference manual answer?
How does the architectural overview for lean4 look like? In particular, what is the minimal set/tooling needed to talk to the kernel. How can I very seemlessly "export" the lean4 context/environment?
Additional context
So I have read the full reference manual and I was quite impressed at the details. After that I could get a better grasp of how the system works and what makes the grids turn correctly.
In particular I would like to work a little bit on understanding the FFI as I would like to have additional tooling like debugging with breakpoints, and access to the rich rust ecosystem.
Here is my current (incomplete and maybe wrong) understanding of how the architecture works.
- In VSCode, there is a multithreaded language server that works on a per file and per line basis.
- The elaborator parses the file, resolves inputs and communicates with the kernel. Given a theorem, if the kernel succeeds in the typecheck, then the kernel adds the theorem to the environment.
- Note to the point above, I might be wrong here but after a longer search I couldn't find who (Kernel, Elaborator, LSP Process) has the ultimate authority over the environment. It could a priori be that the kernel has the authority. Then the elaborator sends the stuff to the kernel and has no worries. Or it could also be that the elaborator keeps the environment and it asks the kernel if everything is good.
- If the kernel holds the environment, then it should be possible to export all theorems and proofs. This assumes that
- The environment stores the proof terms. It appears that the print macro can display proofs. I don't know which process is responsible for storing the proofs.
It would be helpful if I could understand this as this would allow me setting up debugging. I think the debugging currently is limited to printf and traces, as there is no debugging in lean directly. Thus there is no easy way to set breakpoints and inspect the running memory in lean.
Goals I want to solve
Given a .lean file containing some theorems and proofs I want to have a simple executable transfering the environment to rust so that I can inspect the environment from there. I want to be able to set breakpoints and inspect the running memory (this one may not be so important).