Non-builtin parser aliases

Stream: lean4

[Mario Carneiro]

Is it possible to declare a parser alias like withoutPosition(p) in user code? I get an error aliases can only be registered during initialization which I think means I need to use builtin_initialize, but if I do then it appears to have no effect.

[Sebastian Ullrich]

I don't think anyone tried or even thought about that yet. initialize doesn't work?

[Mario Carneiro]

it doesn't

[Mario Carneiro]

also, apparently there is both IO.initializing and initializing and they aren't the same thing

[Mario Carneiro]

haha lol if I just delete the error message then it works

[Eric Wieser]

I think this doesn't work so well after all; if you register the alias with initialize, then you get a crash if you load a module using that alias with withImportModules (as we do in many CI scripts), as the initializer will not have run.

[Eric Wieser]

So we need to do one of:

• Not use add_parser_alias in initialize (i.e. by using builtin_initialize and precompiling parts of mathlib)
• Not using withImportModules, and instead using Lean.enableInitializersExecution and importModules. batteries #1047 and import-graph#44 implement this approach
• Change how parser aliases are registered to avoid a crash if a syntax references a parser alias that is not configured

[Kim Morrison]

batteries#1047

[Eric Wieser]

As far as I can tell this also means that it is no longer possible to call withModules twice in the same process with different imports, as the initialize that runs add_parser_alias won't run the second time.

[Mario Carneiro]

Regarding the bullets above, it was my understanding that it is part of setting up a lean elaborator process that you have to call enableInitializersExecution first (only once, usually right at the start of main)

[Eric Wieser]

If this is the case, then what is the intended application of docs#Lean.withImportModules ?

[Eric Wieser]

That function segfaults for me if used with enableInitializersExecution (hence dropping it in batteries#1047), presumably because it tried to free the compacted regions

[Mario Carneiro]

well that doesn't really answer the question, of course it is freeing the compacted regions but why does that cause a segfault?

[Mario Carneiro]

The comment is clear that this happens when you hold on to a reference to a lean object past that boundary, so the question is who is doing that

[Mac Malone]

Mario Carneiro said:

Regarding the bullets above, it was my understanding that it is part of setting up a lean elaborator process that you have to call enableInitializersExecution first (only once, usually right at the start of main)

Only if you want to invoke (non-builtin) initializers. If you have a cusotm frontend executable that elaborates files with a known set of imports that are already initialized in the executable, this is unnecessary (and may be counterproductive). For example, Lake does not currently use enableInitializersExecution.

[Mac Malone]

enableInitializersExecution also only effects non-builtin initializers that are imported by the elabroator. Initializers (builtin or otherwise) in modules imported by an executable will always be run at the start of the executable.

[Mac Malone]

Eric Wieser said:

As far as I can tell this also means that it is no longer possible to call withModules twice in the same process with different imports, as the initialize that runs add_parser_alias won't run the second time.

The idea is that initializers should only need to be run once. The alias is added to the (global executable) aliases reference and is thus available to all future elaboration. Thus, the danger is not that the alias won't exist in the second withModules but rather that will even if the new set of modules does not include the module which adds it.

[Mac Malone]

More generally, the Lean elaborator is currently meant to be a one-enviroment / one-import set per process. Doing otherwise will pose risks.

[Eric Wieser]

Mac Malone said:

Thus, the danger is not that the alias won't exist in the second withModules but rather that will even if the new set of modules does not include the module which adds it.

If the first call imports [`A], and the second call imports [`A, `B], then I believe the initializers in A will be run once (as expected) but the initializers in B will never be run?

[Eric Wieser]

Mario Carneiro said:

The comment is clear that this happens when you hold on to a reference to a lean object past that boundary, so the question is who is doing that

Is the parser alias itself such a reference?

[Mac Malone]

Eric Wieser said:

If the first call imports [`A], and the second call imports [`A, `B], then I believe the initializers in A will be run once (as expected) but the initializers in B will never be run?

If you call enableInitializersExecution before each (so twice), the initializers for A for should be run in the first withImportModules and the iniitializers for B should be run in the second.