feat: basic support for reinitialization

[digama0]

See Zulip for context. This allows lean to be able to call the frontend more than once per process, by keeping track of modules that have been initialized and not calling their initializers again. This is possibly duplicating state because the C code also keeps this information in _G_initialized private static booleans in each module, but I think only compiled modules have this, while we need it here for all modules (compiled and interpreted).

Because lean already does enough accounting to avoid multiple initialization of modules, there is no need during a normal elaboration session to collect this state, so the enableReinitialization function lazily initializes the state when requested (e.g. by a tool that is planning to call the frontend from the interpreter, or a tool that will call the frontend many times in the same process).

[semorrison]

I'm excited to have a play around with this! For "library scale" tools (e.g. do something at every goal) this could be really useful.

[Kha]

If the interpreter doesn't sufficiently accurately simulate the native generated code, I would consider that a bug in the interpreter.

[digama0]

Currently, the divergence is that when you call runModInit you either get true meaning native code was run (and this will automatically do nothing if the initializer was previously run), or you get false if there is no native code, in which case registerInitAttrUnsafe goes on to manually run the initializers, without any reinitialization guard (that's what this PR fixes). This is fine for the lean core use case since the list of modules to init is already prepared in dependency order and only run once per module, while the native initializers directly call each other along the import structure and hence have to avoid double-calling in practice. But it does mean that the latter kind of initialization breaks if initialization is called twice.

[semorrison]

I am going to write up a clearer account of what it is that I would like to do with a frontend, and how that relates to the problem addressed here. I added the missing RFC label to indicate this PR should wait on (at least) that.

[Kha]

I feel strongly that this is not the correct way to fix/work around this issue, so closing. Let's continue in the issue, where we have a no-change workaround and addition concerns about enabling this posted.