error building windows exe proj

Stream: mathlib4

[Somo S.]

On window 10, I cannot successfully build even the simplest lean_exe project when it depends on mathlib4.
I get "unspecified system_category error (error code: 87)"

TLDR: Clone this repo and run lake build on windows 10.

To reproduce my issue here are the details.

Project has three simple files:

lean-toolchain

leanprover/lean4:v4.0.0

lakefile.lean

import Lake
open Lake DSL

package «try_math_exec» {}

-- mathlib v4.0.0 is at commit d56176f.
require mathlib from git "https://github.com/leanprover-community/mathlib4.git"@"d56176f12b78a0cf8454d9c2a6e9e8d4954dc58a"

@[default_target]
lean_exe «try_math_exec» {}

try_math_exec.lean

import Mathlib.Data.Real.Basic

#check Real
def main : IO Unit := IO.println "Hello World"

I then run

 lake update && lake exe cache get && lake build

Expecting a successful build and executable output at ./build/bin/try_math_exec.exe which when run should just output "Hello World".

However, I have instead been getting the following error output:

...
[1267/1289] Compiling Mathlib.Algebra.Order.Floor
[1268/1289] Compiling Mathlib.Data.Rat.Floor
[1269/1289] Compiling Mathlib.Algebra.Order.Archimedean
[1271/1289] Compiling Mathlib.Data.Real.Basic
[1272/1289] Building try_math_exec
stdout:
Real : Type
[1283/1289] Compiling try_math_exec
[1289/1289] Linking try_math_exec.exe
error: failed to execute `c:\Users\makombo\.elan\toolchains\leanprover--lean4---v4.0.0\bin\leanc.exe`: unspecified system_category error (error code: 87)

I have tried this for both v4.0.0 and v4.1.0-rc..

It's all consistently working fine in ubuntu (wsl) ... builds and runs hello-world succesfully.

Is this an already known issue or perhaps I am doing something wrong?

may be related to earlier report https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/unspecified.20system_category.20errors

/cc @Scott Morrison

[Mario Carneiro]

Could you minimize the imports? Does this happen if you only import Std (keeping the require mathlib as is)?

[Somo S.]

@Mario Carneiro do you mean if I import Std but require mathlib in lakefile (as before).. or do you mean I should change the lakefile requirement to Std itself?

[Mario Carneiro]

the former

[Scott Morrison]

(Minor datapoint: this repo works fine on macos.)

[Somo S.]

@Mario Carneiro said:

Could you minimize the imports? Does this happen if you only import Std (keeping the require mathlib as is)?

changed the relevant lines of try_math_exec.lean to :

import Std.Data.Rat.Basic

#check Rat

And this works fine.

[Mario Carneiro]

okay, so now the challenge is to find out which of your 1289 imports are causing the problem

[Mario Carneiro]

I'm guessing you can get rid of the #check line

[Somo S.]

Mario Carneiro said:

I'm guessing you can get rid of the #check line

yes.. turns out this is the case.

[Somo S.]

when I merely change the import to import Mathlib.Data.Nat.Basic
I get different error :

ld.lld: error: too many exported symbols (got 70485, max 65535) clang: error: linker command failed with exit code 1 (use -v to see invocation) error: external command "c:\Users\makombo\.elan\toolchains\leanprover--lean4---v4.0.0\bin\leanc.exe"

Here is truncated log

[392/423] Compiling Mathlib.Data.Prod.Basic
[393/423] Compiling Mathlib.Algebra.Group.Defs
[397/423] Compiling Mathlib.Data.Nat.Cast.Defs
[397/423] Compiling Mathlib.Algebra.GroupWithZero.Defs
[399/423] Compiling Mathlib.Data.Int.Cast.Defs
[401/423] Compiling Mathlib.Order.Basic
[404/423] Compiling Mathlib.Algebra.Ring.Defs
[405/423] Compiling Mathlib.Data.Nat.Basic
[406/423] Building try_math_exec
[419/423] Compiling try_math_exec
[423/423] Linking try_math_exec.exe
error: > c:\Users\makombo\.elan\toolchains\leanprover--lean4---v4.0.0\bin\leanc.exe -o .\build\bin\try_math_exec.exe .\build\ir\try_math_exec.o .\lake-packages\std\build\ir\Std\Lean\Command.o .\lake-packages\std\build\ir\Std\Tactic\Unreachable.o .\lake-packages\std\build\ir\Std\Linter\UnreachableTactic.o .\lake-packages\std\build\ir\Std\Lean\TagAttribute.o .\lake-
...
packages\std\build\ir\Std\Lean\Meta\Basic.o .\lake-packages\std\build\ir\Std\Lean\Tactic.o .\lake-packages\std\build\ir\Std\Tactic\Basic.o .\lake-packages\std\build\ir\Std\Lean\NameMapAttribute.o .\lake-packages\std\build\ir\Std\Tactic\Lint\Basic.o .\lake-packages\std\build\ir\Std\Data\List\Init\Lemmas.o .\lake-packages\std\build\ir\Std\Data\Array\Init\Basic.o .\lake-packages\std\build\ir\Std\Data\Ord.o .\lake-packages\std\build\ir\Std\Data\Array\Basic.o .\lake-packages\std\build\ir\Std\Tactic\Lint\Misc.o .\lake-packages\std\build\ir\Std\Logic.o .\lake-packages\std\build\ir\Std\Data\Nat\Init\Lemmas.o .\lake-packages\std\build\ir\Std\Classes\Dvd.o .\lake-
...
packages\std\build\ir\Std\Lean\Meta\DiscrTree.o .\lake-packages\std\build\ir\Std\Tactic\Ext\Attr.o .\lake-packages\std\build\ir\Std\Util\LibraryNote.o .\lake-packages\std\build\ir\Std\Tactic\Lint\Simp.o .\lake-packages\std\build\ir\Std\Tactic\Lint\TypeClass.o .\lake-packages\std\build\ir\Std\Tactic\Lint\Frontend.o .\lake-packages\std\build\ir\Std\Tactic\Lint.o .\lake-packages\std\build\ir\Std\Control\ForInStep\Basic.o .\lake-packages\std\build\ir\Std\Control\ForInStep\Lemmas.o .\lake-packages\std\build\ir\Std\Data\Option\Lemmas.o .\lake-packages\std\build\ir\Std\Classes\BEq.o .\lake-packages\std\build\ir\Std\Tactic\Ext.o .\lake-packages\std\build\ir\Std\Lean\Meta\LCtx.o .\lake-packages\std\build\ir\Std\Tactic\Simpa.o .\lake-packages\std\build\ir\Std\Data\List\Lemmas.o .\lake-packages\std\build\ir\Std\Data\List\Count.o .\lake-packages\mathlib\build\ir\Mathlib\Lean\Meta.o .\lake-
...
packages\std\build\ir\Std\Data\String\Basic.o .\lake-packages\mathlib\build\ir\Mathlib\Tactic\RunCmd.o .\lake-packages\mathlib\build\ir\Mathlib\Lean\Linter.o .\lake-packages\mathlib\build\ir\Mathlib\Tactic\Simps\Basic.o .\lake-packages\mathlib\build\ir\Mathlib\Tactic\ToAdditive.o .\lake-packages\mathlib\build\ir\Mathlib\Init\ZeroOne.o .\lake-packages\mathlib\build\ir\Mathlib\Util\CompileInductive.o .\lake-packages\mathlib\build\ir\Mathlib\Init\Data\Nat\Basic.o .\lake-packages\mathlib\build\ir\Mathlib\Init\Data\Nat\Div.o .\lake-packages\std\build\ir\Std\WF.o .\lake-packages\std\build\ir\Std\Classes\Cast.o .\lake-packages\std\build\ir\Std\Classes\Order.o .\lake-packages\std\build\ir\Std\Data\Nat\Gcd.o
...
packages\std\build\ir\Std\CodeAction\Misc.o .\lake-packages\std\build\ir\Std\CodeAction.o .\lake-packages\std\build\ir\Std\CodeAction\Deprecated.o .\lake-packages\std\build\ir\Std\Control\ForInStep.o .\lake-packages\std\build\ir\Std\Data\AssocList.o .\lake-packages\std\build\ir\Std\Data\BinomialHeap\Basic.o .\lake-packages\std\build\ir\Std\Data\BinomialHeap\Lemmas.o .\lake-packages\std\build\ir\Std\Data\BinomialHeap.o .\lake-packages\std\build\ir\Std\Data\DList.o .\lake-packages\std\build\ir\Std\Data\Fin\Basic.o .\lake-packages\std\build\ir\Std\Data\Fin\Lemmas.o .\lake-packages\std\build\ir\Std\Data\HashMap\Basic.o .\lake-packages\std\build\ir\Std\Data\HashMap\WF.o .\lake-packages\std\build\ir\Std\Data\HashMap.o .\lake-
...
packages\mathlib\build\ir\Mathlib\Init\Order\LinearOrder.o .\lake-packages\mathlib\build\ir\Mathlib\Tactic\Cases.o .\lake-packages\mathlib\build\ir\Mathlib\Init\Data\Nat\Lemmas.o .\lake-packages\mathlib\build\ir\Mathlib\Init\Core.o .\lake-packages\mathlib\build\ir\Mathlib\Tactic\LabelAttr.o .\lake-packages\mathlib\build\ir\Mathlib\Tactic\Attr\Register.o .\lake-packages\mathlib\build\ir\Mathlib\Init\Function.o .\lake-packages\mathlib\build\ir\Mathlib\Tactic\LeftRight.o .\lake-
...
packages\mathlib\build\ir\Mathlib\Algebra\Group\Defs.o .\lake-packages\mathlib\build\ir\Mathlib\Logic\Nontrivial\Defs.o .\lake-packages\mathlib\build\ir\Mathlib\Algebra\GroupWithZero\Defs.o .\lake-packages\mathlib\build\ir\Mathlib\Data\Nat\Cast\Defs.o .\lake-packages\mathlib\build\ir\Mathlib\Data\Int\Cast\Defs.o .\lake-packages\mathlib\build\ir\Mathlib\Util\AssertExists.o .\lake-packages\mathlib\build\ir\Mathlib\Algebra\Ring\Defs.o .\lake-packages\mathlib\build\ir\Mathlib\Tactic\Conv.o .\lake-packages\mathlib\build\ir\Mathlib\Tactic\PushNeg.o .\lake-packages\mathlib\build\ir\Mathlib\Tactic\Use.o .\lake-packages\mathlib\build\ir\Mathlib\Data\Nat\Basic.o
error: stderr:
ld.lld: error: too many exported symbols (got 70485, max 65535)
clang: error: linker command failed with exit code 1 (use -v to see invocation)
error: external command `c:\Users\makombo\.elan\toolchains\leanprover--lean4---v4.0.0\bin\leanc.exe` exited with code 1

[Scott Morrison]

This is https://github.com/leanprover/lean4/issues/2346

[Scott Morrison]

I would guess this is the underlying cause of your original error.

[Scott Morrison]

Unfortunately we don't have a fix for this issue as yet. :-(

[Somo S.]

Scott Morrison said:

Unfortunately we don't have a fix for this issue as yet. :-(

thanks for the feedback

[Scott Morrison]

Can I ask for an #xy? While we do want to work out what is going wrong here, actually compiling (i.e. to an executable) all of mathlib, rather than just building it (i.e. to oleans) seems of dubious usefulness.

[Mario Carneiro]

I think it's not an unreasonable ask to be able to compile an exe in the presence of mathlib

[Mario Carneiro]

for example mathport is such an exe

[Scott Morrison]

Sure. But mathport is a bit of an unusual beast. I definitely agree this needs fixing, I was just curious if it was obstructing something.

[Somo S.]

Scott Morrison said:

Sure. But mathport is a bit of an unusual beast. I definitely agree this needs fixing, I was just curious if it was obstructing something.

No you are not obscuring something at right this moment.. Perhaps in the future ... As I have been learning lean I have been setting up my projects this way as a litmus just to have confidence that I set everything up correctly. I just had imagined building some software that I would write and prove correct in lean, but whose proofs would require the use of some concept or another that's already been proven in mathlib. For example I saw that mathlib has proofs for quicksort and mergesort. So imagining one of those sorting algorithms being a part of some larger software certification project.

[Mario Carneiro]

Scott Morrison said:

Sure. But mathport is a bit of an unusual beast. I definitely agree this needs fixing, I was just curious if it was obstructing something.

Well it does imply that mathlib is incompatible with writing programs, which I don't think we are intending to be the case!

[Mario Carneiro]

It's great that std exists now, but there are still many programs that use things from mathlib and I don't think we should have to make a choice between proving correctness of the program and being able to compile it

[Mario Carneiro]

Plus, I think mathport does count as a current project being affected - it implies that you can't build and use mathport on windows, which is news to me

[Scott Morrison]

Hmm... I remember someone trying this at Banff, but I don't think they even got as far as running into lean4#2346.

[Somo S.]

Mario Carneiro said:

Well it does imply that mathlib is incompatible with writing programs, which I don't think we are intending to be the case!

more generally, it implies whatever it is that caused mathlib to have that problem _is_ incompatible with writing programs... what i mean here is if some other library author creates some library in the future (even if it doesnt depend on mathlib) it its possible their lean_exe users who depend on that library might run into these errors if that library is written in such a way that it shares the same/similar underlying thing (architecture?,bug? ..) that's causing this mathlib

[Mario Carneiro]

the thing that causes the error in lean4#2346 is too many exported symbols, as the error message implies

[Mario Carneiro]

I think this just means number of def definitions, give or take

[Mario Carneiro]

and 65536 is not that many defs

[Mario Carneiro]

I think mathlib has somewhere in the range of 500000 defs (EDIT: 528262)

[Somo S.]

yeah so its possible for some other library author to have that issue in their library in the future, if they don't already have it (even if they dont depend on mathlib at all).. so an ideal solution to this solves it for them as well

[Mario Carneiro]

the good news is that you have to be at mathlib scale before this becomes a big issue

[Mario Carneiro]

well, even import Std apparently has 163820 defs

[Mario Carneiro]

it's possible that this isn't an exact match for things that become exported symbols at link time

[Somo S.]

Mario Carneiro said:

and 65536 is not that many defs

isnt this the maximum size of a 32 bit int? i am naive on this topic but is it not possible to increase this to an int64 somewhere..

[Mario Carneiro]

it's the maximum size of a 16 bit int

[Mario Carneiro]

but this is a linker limitation, I don't think we can do anything about it (unless someone gets lucky and finds a "it's not 1980 anymore" flag somewhere in the linker)

[Somo S.]

Mario Carneiro said:

well, even import Std apparently has 163820 defs

I can confirm that import Std is producing the same "too many exported symbols" error

[Mario Carneiro]

and import Lean has 145543 defs... I don't understand how anything works

[Sebastian Ullrich]

Mario Carneiro said:

I don't understand how anything works

https://github.com/search?q=repo%3Aleanprover%2Flean4+export+symbols+windows&type=pullrequests

[Sebastian Ullrich]

Note that this is also a regular issue for LLVM itself

[Somo S.]

Mario Carneiro said:

it's the maximum size of a 16 bit int

Looks like clang v11.1.0 was the last version that did not include this max check

I have naively tried to run the raw clang command using clang v11.0.0 and and it still failed (i didn't expect it would work anyway).

[Sebastian Ullrich]

This is a Windows limitation, not LLVM's

[Eric Wieser]

Why do these symbols need to be exported anyway?

[Eric Wieser]

Can't you just tell the C compiler "don't export anything at all"?

[Eric Wieser]

(this is "export" in the shared library sense, right?)

[Sebastian Ullrich]

You can, but then you can't turn it into a DLL. So we would have to recompile the .c files depending on what our ultimate linking target is, which at least so far is not a control flow that exists. And then you still end up with exported symbols from core, which at some point might not fit into a single binary either (but also just don't import Lean)

[Somo S.]

i had tested import Lean and it worked fine.. I'll check again

[Sebastian Ullrich]

Note the "at some point"

[Somo S.]

gotchya

[Sebastian Ullrich]

If someone could open an lld issue in the LLVM repo about this, that would be great. It feels like there should be some way to unexport all symbols when linking an executable, as we usually don't care about exports there.

[Somo S.]

i would, but I don't know much about llvm and all this

/cc @Luis O'Shea

[Eric Wieser]

Isn't this the role of a linker script, as described here?

[Sebastian Ullrich]

Maybe!

[Somo S.]

by the way, is it possible to cross compile from linux (say wsl) to windows by passing some flags to lake build or perhaps by reconfiguring one's lakefile?

[Sebastian Ullrich]

Not out of the box. It is technically feasible (we already cross-compile Lean to ARM in CI) but at the very least you will need headers and libraries from the Lean Windows release as well. We can't bundle Lean with big libraries for all platforms.

[Martin Dvořák]

I just got the same error.

[Reid Barton]

This is/was a problem for GHC on Windows too. Maybe this page has some useful information:
https://gitlab.haskell.org/ghc/ghc/-/wikis/windows-dynamic-linking
I see something about --retain-symbols-file that sounds promising. (Does a Lean executable typically need any exported symbols besides _start or whatever it's called? e.g. does the RTS try to dlsym() anything?)

[Reid Barton]

(I don't really know anything about Windows but I assume that for now the issue is not that we really want to support shared libraries on Windows, but just that executables are being built in some way that retains the whole symbol table.)

[Reid Barton]

To clarify, what was an issue for GHC on Windows was AFAIK just supporting shared Haskell libraries. I'm not aware of any issue if you just wanted to create an ordinary executable (that was statically linked against all Haskell dependencies).

[Reid Barton]

Is the issue maybe that even on Windows, Lean is hoping to use dynamic libraries and that's why all the symbols are marked for export?

[Reid Barton]

Does Lean use dynamic loading for running tactics or for server mode or something?

[Mario Carneiro]

Reid Barton said:

(Does a Lean executable typically need any exported symbols besides _start or whatever it's called? e.g. does the RTS try to dlsym() anything?)

I think this is what supportInterpreter is about, since the interpreter uses dlsym or something like it to load compiled definitions

[Thomas Browning]

Is it still the case that you can't both write programs and depend on mathlib? For instance, if I'm doing Project Euler and want to write code to count primes, is it currently not possible to prove the correctness of that program without rewriting elementary number theory from scratch?

[Scott Morrison]

Yes, this is still the case (on Windows). :-(

[Utensil Song]

Eric Wieser said:

Isn't this the role of a linker script, as described here?

It seems passing the version script option via lake (via moreLinkArgs in the package block) is feasible for a user. It could be the workaround for now.