Fix loaded native code execution

[Kha]

This PR fixes two related bugs:

• When using --plugin, [init] functions might be run twice: once when loading the plugin, and once in [init]'s afterImport
• When using --load-dynlib, constants (nullary functions) that are not [init] are never initialized. The interpreter does initialize constants lazily, but only when there is no native symbol for them (since it doesn't know what code has been loaded dynamically).

To fix this, we now run the [init] functions only for modules that do not have native code, and run the module initializer function (initialize_Init etc.) for any other imported module. We extend the module initializer with a new boolean flag builtin that prevents --load-dynlib from running builtin_initialize commands as intended.
Note that the module initializer only exists in native code, so we cannot interpret it. Note also that in contrast to --plugin, --load-dynlib can still accept shared libraries that contain code of multiple, possible unrelated Lean modules - it is the imported modules that determine the module initializers to be run (since code of a non-imported module should be unreachable from the interpreter). Thus we can still produce big shared libraries of entire packages and load them whenever any of their modules are imported without additional overhead other than relocation.

[leodemoura]

@Kha Could you please copy the PR comment in the code itself? I am not sure what the best place it, but I think lean_run_mod_init is a good spot. What do you think?

[Kha]

Yes, there's no perfect place in the code. I extended the initializers section in ffi.md instead, since that one already describes parts of the Lean ABI not strictly relevant for FFI. What do you think?