stage0

Stream: lean4

[Julian Berman]

What's the stage0/src directory used for? From the name I guess some thing that handles early parts of the startup process? diff -r stage0/src src shows it's nearly but not exactly a hard copy of the src/ directory?

[Sebastian Ullrich]

See https://leanprover.github.io/lean4/doc/make/index.html#lean-build-pipeline

[Julian Berman]

Thank you!