Zulip Chat Archive

Stream: lean4

Topic: stage0


view this post on Zulip Julian Berman (Mar 04 2021 at 15:30):

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?

view this post on Zulip Sebastian Ullrich (Mar 04 2021 at 15:35):

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

view this post on Zulip Julian Berman (Mar 04 2021 at 15:37):

Thank you!


Last updated: May 18 2021 at 22:15 UTC