Importing a `Lean` module inflates binary size

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

The modules Lean.Data.AssocList, Lean.Data.Name, Lean.Data.LBool and Lean.Data.LOption are all very simple and do not import any non-prelude files. Still, importing any of these without using them causes the binary size to change from ~6M to ~86M. When copying the relevant file into the project and importing that instead, the blowup does not happen.

Context

There was some Zulip discussion a while ago, but there no one noticed that even importing a single file can lead to the blowup.

Steps to Reproduce

Start with the following file:

def main : IO Unit :=
  return ()

1. Compile via lake build. Executable size is ~6.1M
2. Add import import Lean.Data.AssocList and compile via lake build. Executable size is ~86M
3. Copy Lean/Data/AssocList.lean into the project and import that instead. Compile via lake build. Executable size is ~6.1M

Expected behavior: Importing a tiny file and not using it should not inflate binary size.

Actual behavior: Importing a tiny file and not using it inflates binary size.

Versions

4.12.0-nightly-2024-09-05
Linux markus-z16 6.10.6-200.fc40.x86_64 #1 SMP PREEMPT_DYNAMIC Mon Aug 19 14:09:30 UTC 2024 x86_64 GNU/Linux

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start by reproducing the minimal main example with lake build, comparing the executable sizes for no import, import Lean.Data.AssocList, and a copied AssocList.lean. Inspect how these imports affect compilation and linking. Done means importing an unused tiny module no longer causes the reported binary-size increase.