Docs for Compiler Development

Stream: lean4

[Rohan Ganapavarapu]

Hi guys,
I am looking to hack on the lean compiler, I followed the docs to build the compiler but I am sort of lost/don't see where to start to try and see the pipeline and different parts/stages of the compiler. I am curious to see if I missed some docs.

I am trying to write a tokenizer for lean so I want to take advantage of the parser already in lean, but right now I am just trying to see how the compiler works on a higher level. I am looking for docs like this (example from Agda): https://github.com/agda/agda/blob/dc3cae6d3876346f81fe4ded348192f9c7ad8c2b/notes/compiler-pipeline.md.

[Notification Bot]

This topic was moved here from #new members > Docs for Compiler Development by Mario Carneiro.

[Shreyas Srinivas]

This is the build pipeline: https://lean-lang.org/lean4/doc/make/index.html

[Shreyas Srinivas]

Below you'll find how lean is bootstrapped : https://lean-lang.org/lean4/doc/dev/bootstrap.html