perf: initialize only the core modules `leanchecker-paranoid` needs (#14936)

This PR shrinks `leanchecker-paranoid` from 78 MB to 7 MB (18.9 MiB to
2.0 MiB compressed) by not initializing the whole Lean library in a
binary that never elaborates Lean source.

`lean_initialize` calls `initialize_Lean`, which transitively
initializes every module of the library. That makes all of `Lean`
reachable from `main`, so `--gc-sections` cannot drop any of it and a
statically linked binary carries the elaborator, the tactic frameworks
and the language server whatever it uses.

Only `src/initialize/init.cpp` varies with this, so `initialize_minimal`
compiles a second copy of it under `LEAN_MINIMAL_CORE_INIT`, listing
instead the modules that define the exported Lean functions the C++ side
calls. That list is derived from the symbols `libleancpp.a` and
`libleanrt.a` reference but do not define, which is exactly what this
binary links. The archive is listed ahead of `libleancpp.a` so that its
`lean_initialize` wins, the same ordering the hardened mimalloc already
relies on, and it is `EXCLUDE_FROM_ALL` so no other target pays for it.

Binaries that call into elaboration (must) still call `initialize_Lean`,
and there would be no size advantage for them not to do so as they are
all linked against `libleanshared` anyway.
4 files changed