Lake on Windows error: Too many exported symbols

Stream: lean4

[Josh Clune]

I'm working on a project that can take awhile to build, so I was hoping to upload built packages (e.g. using lake upload) to a Github release. I'm able to build the project on Mac, Linux, and in
VSCode on any platform, but encountered an unexpected error when I attempt to build it in Windows.

When I navigate to my project's folder in Windows PowerShell and run lake build, I get the error ld.lld: error: too many exported symbols (got 78102, max 65535) which prevents the project from successfully building. Given that VSCode can build the project on Windows, I assume there's some way to get around this problem, but it's unclear to me how to do so.

My main questions are:

1. What does VSCode do differently from lake build in PowerShell that allows VSCode to succeed where lake build in PowerShell fails? And is there a different command or set of commands I can use in PowerShell to achieve the same effect?
2. How should I interpret the "too many exported symbols" error? And is there anything I can do to better understand why my project has so many exported symbols and if there's anything I can do to fix the error?

[Scott Morrison]

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

[Scott Morrison]

Unfortunately this is a known problem on Windows, and we don't yet have a solution.

[Mac Malone]

This is concerning. Is Std by itself now too big? I just realized its CI does not test a Windows build, so it would be interesting to give that a try. (I may do that myself sometime soon if no one else does.) If not, how many symbols is it?

[Mario Carneiro]

This has always been an issue, even for Lean

[Scott Morrison]

(oops, I thought this only affected projected importing mathlib, my mistake)

[Mac Malone]

@Mario Carneiro I'm with @Scott Morrison, I was pretty sure we had managed to keep Lean below this threshold. I know I can build it on Windows.

[Mario Carneiro]

I recall measuring these numbers to find out where the problem is coming from and Lean already has too many symbols by some count

[Mario Carneiro]

either way it's uncomfortably close to the limit before we even get to user code

[Josh Clune]

It's comforting (for me) to know that this is a known issue and not one that specifically arose due to something I did in my project.

Perhaps the only thing I can do is let it be and trust that the issue will be resolved at some point, but, just in case, I'm wondering whether there's anything I can do on my end to reduce the number of symbols generated by my project. For those who have experience measuring those numbers for Lean itself, would it be possible to point me to the tools and/or references you used so I can see whether there's low-hanging fruit I can fix in my project for now? Or would you say this is an inadvisable course of action and that the best thing for me to do is leave it be in the short term?

[Utensil Song]

You may want to take a look at the discussion here and try the workaround to make it export less symbols.

[Josh Clune]

Thanks for the link, I missed that discussion. I'll take a look.