too many exported symbols

Stream: new members

[Sampo Siitonen]

When I try to build a simple Lean program which basically only imports from Mathlib and runs a hello world,lake buildspits out the following linker error:

error: > c:\Users\Sampo\.elan\toolchains\leanprover--lean4---nightly-2023-07-12\bin\leanc.exe -o .\build\bin\lean_exports.exe .\build\ir\Main.o .\lake-packages\mathlib\build\ir\Mathlib\Mathport\Rename.o .\lake-packages\std\build\ir\Std\Util\ExtendedBinder.o ...[MANY MORE .o FILES]
error: stderr:
ld.lld: error: too many exported symbols (got 68151, max 65535)
clang: error: linker command failed with exit code 1 (use -v to see invocation)
error: external command `c:\Users\Sampo\.elan\toolchains\leanprover--lean4---nightly-2023-07-12\bin\leanc.exe` exited with code 1

The VSCode lean4 extension typechecks the code perfectly fine however. Is there some way to decrease the number of symbols or link more than $2^{16}$ symbols?

[Scott Morrison]

Could you show us a #mwe?

[Sampo Siitonen]

The only thing I have done is added mathlib as a dependency, following these instructions, and imported one module from it. The error only happens on Windows; I tried compiling on Linux which worked fine.

Running these command reproduces the issue on my machine:

lake new lean-too-many-symbols
cd lean-too-many-symbols
echo "import Lake
open Lake DSL

require mathlib from git
  ""https://github.com/leanprover-community/mathlib4""

package «lean-too-many-symbols»

@[default_target]
lean_exe «lean-too-many-symbols» {
  root := ``Main
}" > lakefile.lean
echo "import Mathlib.Data.Vector

def main : IO Unit := pure ()" > Main.lean
curl -L https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain
lake update
lake build

Additional context:

> elan --version
elan 2.0.0 (001eb2cfe 2023-07-03)
> lake --version
Lake version 4.1.0-pre (Lean version 4.0.0-nightly-2023-07-12)
> lean --version
Lean (version 4.0.0-nightly-2023-07-12, commit 6e904421304c, Release)

[Kyle Miller]

From what I found online, it sounds like DLL files have a limit of 65535 exported symbols. I don't know if there's an easy solution to this.

[Scott Morrison]

@Sampo Siitonen, could you please open an issue on the Lean 4 repository, with your reproduction?

[Sampo Siitonen]

done