Is Std intended to be bootstrapped?

Stream: lean4

[Eric Wieser]

I noticed today that Std is now in the stage0 folder. Is this intentional, and an indication that the Lean and Init libraries are permitted to depend on Std in future?

[Markus Himmel]

The intended dependency chain is Lean -> Std -> Init. In fact, Lean will start to depend on Std very soon, once lean4#4917 lands.