too many exported symbols linker error on Windows
#2346
Comments
|
It would be nice to be able to "unexport" |
|
I get the same problem when building https://github.com/paulcadman/lean4-leetcode on a similar Windows machine with a slightly newer toolchain. Happy to provide details if they would help. |
|
If ayone could check whether there is a simple linker flag that avoids this issue, that would be very helpful! I hope at least |
|
Happy to try it. How can I change the linker flags? I'm currently using lake to drive the build. (As you can guess, I'm not very familiar with the lean toolchain.) |
|
Thanks! If you run |
|
|
|
I tried appending |
|
Mmh, that's disappointing, but thanks for checking. I would really hope there is some other combination of flags but I'm not that familiar with MinGW linking. |
|
An easier way of doing what I did is to edit the lakefile, adding the following line: to the |
|
As disscussed here on zulip this issue might also be manifesting itself as |
Looks like clang v11.1.0 was the last version that did not include this check (see commit info) I have naively tried to run the raw clang command using clang v11.0.0 and and it still failed with: |
|
The check is not the problem here, it is there for a good reason: The DLL format itself does not support more than 65536 entries. If you backtrack to before the error message was added, you will just get a silently corrupted DLL file or similar. |
|
Just linking to another place someone has encountered this. That example doesn't even require Mathlib. :-( |
|
We really should fix that then. I see two possibilities:
|
|
In my "Native Windows GHC" I've solved a similar problem. The ONLY viable long-term solution (I've thoroughly analyzed all the previous, all failed, attempts to solve the problem) is to NOT use the standard windows symbols exporting scheme. So I've devised my own one. GHC case is much, MUCH more complicated than the Lean one, and I believe it won't be that hard to port the whole idea to Lean. The idea is simple: we build our own table of Lean-generated exported symbols, and only export this single table symbol (along with standard exports from C++ code). We also generate a stub for each Lean-generated exported symbol, and also the tiny patcher function, which puts an actual address into this stub. All these patchers are put into constructors section, and c-runtime runs them all before any of them is used. This how static linking against such a DLL works (and I used some tricks to make a client exe link ONLY those stubs and patchers, that are used by the exe). To make dynamic loading from such a DLL possible, we shall add some metadata, mapping each symbol name to its offset in the table. All of this is about This particular issue is resolved trivially: since no object files contains any We also won't need #3601 and won't need separate Also, I believe, it will help to solve #1148. But having said that I wonder how you ever build Lean on Windows? Msys2 doc looks outdated (and wrong). I managed to configure things looking into ci scripts. But it first failed with Then it failed with And now it finally fails with But how is it possible if we have |
|
@awson That is useful to know but it seems like a solution we would like to avoid if at all possible |
Prerequisites
Description
Trying to build an executable with a sizeable dependency (mathlib) fails with a linker error.
Steps to Reproduce
Expected behavior: I expected Lean to succesfully build an executable.
Actual behavior: The following linker error is produced:
Running the
leanccommand with-v, the actualld.lldinvocation is:Reproduces how often: This problem reproduces every time on my Windows machine. On Linux, the problem does not occur.
Versions
Windows 10 Home 22H2
Additional Information
The symbol limit check was added to
ld.lldin https://reviews.llvm.org/D86701.The text was updated successfully, but these errors were encountered: