virtual file environment

Stream: Is there code for X?

[Asei Inoue]

Is it possible to create an environment within the same file as if the files were switched?

For example, is it possible to virtually ensure that a name defined with the private command is invisible to another file within the same file?

[Mario Carneiro]

No, not really. Every elaborator session runs in a separate process, and lean uses a lot of global variables so you can't just pause elaboration, recursively call the frontend on a completely separate file, and then go back to elaborating the original file. Lean could plausibly support features that act as though it was in a separate module, like changing the mainModule name in the elaborator state or removing private declarations from name resolution, but there is not currently much need for this (it would be a significant amount of work) and it would probably have to come with a significant amount of other design.

For what it's worth, this feature does exist in Rust, in the form of module blocks: you normally use mod foo; and then put the code in the foo.rs file but you can also use mod foo { ... } and put all the code in the ... instead, and it acts exactly the same as if it was a separate file.

[Asei Inoue]

@Mario Carneiro Thank you!!

[Notification Bot]

Asei Inoue has marked this topic as resolved.

[Eric Wieser]

This would be a useful feature for testing things with initialize, which currently resist attempts to capture in a single-file mwe

[Notification Bot]

Asei Inoue has marked this topic as unresolved.

[Asei Inoue]

@Eric Wieser what is initiatile? I dont know the command

[Eric Wieser]

Typo, sorry