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.
This is the repository for Lean 4.
See Install Lean.
Please read our Contribution Guidelines first.
See Building Lean.