The clang command line with all ~15,000 Mathlib .c.o.export

Stream: lean4

[Kevin Sullivan]

Need precompiled mathlib from .c.o's. But this. Help? Thank you!

[Kevin Sullivan]

Mathlib cache ships Linux .so shared libs but not macOS .dylib files, so precompileModules on macOS always triggers a full Mathlib re-link that exceeds MacOS ARG_MAX, coming in at just a few K over the limit. Can someone who knows for sure confirm or disconfirm re: no Mac .dylib build in distributed cache? Thank you!

[Personal note: I can build in a Linux environment, so this is not a blocker for me, but it could be for others. Probably a well known issue, but anyway, we each learn at our own rate :-)

[Kim Morrison :bot:]

Lake already has response file support for this, but it was gated to Windows only. lean#12540 enables it on all platforms.