Importing Lean from Std and Init

Stream: lean4

[Henrik Böving]

Eric Wieser said:

I think at one point Init was not allowed to import Lean, and so it would be impossible to write the json% elaborator solely within Init. Maybe that rule has been relaxed now.

This is not about being allowed this is about technical impossibilities as it would import the Lean of a previous stage since the Lean of its current stage would not be compiled yet.

[Eric Wieser]

I don't follow, isn't the requirement just that the individual imports don't form a cycle? The bootstrapping surely doesn't care what the first component of the module names are?

[Henrik Böving]

Eric Wieser said:

I don't follow, isn't the requirement just that the individual imports don't form a cycle? The bootstrapping surely doesn't care what the first component of the module names are?

If you are in stageN compiling Init the Lean of stageN does not exist yet, it is yet to be compiled as stageN Lean depends on importing stageN Init. So the only way to pull in a Lean at this point would be to import Lean from stageN-1, you should not do that (and in fact as stage0 does not have .olean but only .c artefacts can't even do it for stage1 though technically for stage2)

[Henrik Böving]

In general the dependency chain goes Lean -> Std -> Init so not only can Init not import Lean but Std can also not do it. This is one of the reasons that the compiler has funky meta programming things like builtin_ for building features that can be used in Init/Std after rebootstrapping.

[Eric Wieser]

I still don't understand the bootstrapping argument; why can't I consider a pseudolibrary core = Init + Std + Lean, and bootstrap core incrementally as one large unit?

[Eric Wieser]

My hunch would be that if lake is now in stage0 and used to build stage1 (replacing the old makefile), you get this behavior for free

[Notification Bot]

A message was moved here from #lean4 > upstreaming Mathlib.Lean.Json by Eric Wieser.

[Henrik Böving]

No this would be incredibly inconvenient:

1. You would have to carry .olean files for everything around in stage0 to be able to compile properly which is not only going to enlarge stage0 but also has potential cross platform issues so you might even need to store multiple .olean files.
2. Literally every PR would need to update-stage0 as the import statements in stage1 would refer to .olean from stage0 but you want to have the changes that you made be effective in stage1 already not only stage2

The workflow as it exists in core right now is simple, you get the import chain I described, you can develop just normally, you don't need to update-stage0 often. If you actually need to add some meta feature that is used in Init and can't be programmed with the macro system that is already set up there you can use builtin_ stuff + rebootstrap to get it into there.

[Eric Wieser]

I'm not suggesting that stage 1 import lean files from stage 0

[Henrik Böving]

But that's what has to happen if you want to be able to access import Lean from Init? Where else would the .olean you get when running import Lean in an Init file be coming from?

[Henrik Böving]

Or are you suggesting that we build all of these as a big dependency graph? In that case: Why should Lean not be able to enjoy the freedom to just import everything from Init (which is very common, after all the majority of Init is imported in Lean) in favor of having the ability to import Lean in some files of Init that don't cause a cycle, just to implement an elaborator there (a very rare use case). After all we already have the ability to get custom elaborators usable in Init through the builtin_ mechanism.

[Eric Wieser]

Yes, I'm suggesting the big dependency graph option

[Eric Wieser]

Henrik Böving said:

After all we already have the ability to get custom elaborators usable in Init through the builtin_ mechanism.

Not if if you need access to the Lean. API to implement those elaborators.

[Henrik Böving]

Of course we do

[Henrik Böving]

You implement the elaborator within Lean, mark it as builtin_, update-stage0 and you can use it in Init.

[Henrik Böving]

That's how every tactic that we have ends up being usable in Init.

[Eric Wieser]

But the consequence here is:

• Things like Json end up in the Lean rather than Std imports
• You have to rebootstrap after each new elaborator you want in Init/Std

The big dependency graph is indeed more of a mental burden to manage, but has neither of these shortcomings

[Eric Wieser]

I can see a purity argument over leaving Init be, but letting Std and Lean co-import each other in one graph would be quite convenient

[Henrik Böving]

• Things like Json end up in the Lean rather than Std imports

Sure, that's how things already are, bv_decide is almost fully implemented in Std but I don't see the issue with this? After all the meta part is part of the Lean code.

• You have to rebootstrap after each new elaborator you want in Init

Yes but that is only a very rare occurence, as I explained above this potentially has the issue of making live painful when you want to import something from Init in Lean. As someone that has fixed a non trivially long dependency cycle in Init alone because of the limited meta capability that already exists there I can tell you that this is not fun :P