fix: do not dllexport symbols in core static libraries

[Kha]

On Windows, we now compile all core .os twice, once with and without dllexport, for use in the shipped dynamic and static libraries, respectively. On other platforms, we export always as before to avoid the duplicate work.

[Kha]

TODO to definitely resolve #2346: do the same for user code in Lake

[tydeu]

I noticed we are running this for both the C and LLVM backend. I don't imagine this -D actually does anything when compiling the bc file. We will need to change the LLVM emitter instead:

lean4/src/Lean/Compiler/IR/EmitLLVM.lean

Lines 496 to 507 in 5302b78

	-- we must now set symbol visibility for global.
	if ps.isEmpty then
	if isClosedTermName env decl.name then LLVM.setVisibility global LLVM.Visibility.hidden -- static
	else if isExternal then pure () -- extern (Recall that C/LLVM funcs are extern linkage by default.)
	else LLVM.setDLLStorageClass global LLVM.DLLStorageClass.export -- LEAN_EXPORT
	else if !isExternal
	-- An extern decl might be linked in from a different translation unit.
	-- Thus, we cannot export an external declaration as we do not define it,
	-- only declare its presence.
	-- So, we only export non-external definitions.
	then LLVM.setDLLStorageClass global LLVM.DLLStorageClass.export
	return global

However, this may be a TODO for later, as configuring this to emit both the export file and the non-export is more difficult as this is part of Lean elaboration rather than a separate step.

[Kha]

Oh yes, I meant to flag this to @bollu @hargoniX but forgot. I don't see this being addressed before we move code generation out of the main lean invocation

[Kha]

@tydeu I believe the only remaining issue is that supportInterpreter test binaries now fail on Windows as we've now basically implemented our own -rdynamic distinction! So Lake would need to include LEANC_SHARED_LINKER_FLAGS when building a supportInterpreter executable on Windows.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 09bc477016caffe11da2fac58051c59161445ae3 --onto ae492265fec103aa834d897bf9f68c94d10f0785. (2024-03-08 20:44:38)
• ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 1151d73a551e45303495f73d59cd3f617d49fd9d --onto 317adf42e92a4dbe07295bc1f0429b61bb8079fe. (2024-03-14 18:22:55)

[tydeu]

I believe I have fixed everything I can on the Lake side and everything now can function, so I will hand this back to you @Kha.

[tydeu]

@Kha Added the release note. Feel free to merge when convenient.