feat: fat static libraries with all transitive dependencies

[bollu]

Adapted from this zulip thread titled 'reverse FFI: building a "fat" static library'

---

The motivation is to enable more reverse-FFI use-cases. End users should be able to build a single static library that can be linked against. This library should include all (transitive) dependencies of the Lean library. This enables easy static linking.

My personal use-case is to link a lean+mathlib+batteries library against a rust project. This is accomplished by building a static library as proposed, and linking against this in the build.rs build script.

---

The larger part of the PR is to add an example that showcases how to use it in a new example in a library with a dependency, which has been adapted from the already existing example of reverse-ffi. We add a new test that checks that reverse FFI does indeed include transitive dependencies by grepping for the _initialize_ function of the dependency.

[bollu]

awaiting-review

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase d3ee0be9080f4572ad3be32e94da906d53dc8987 --onto b0c1112471a3f38859d9738184d21132b7d9cd0c. (2024-05-24 22:40:21)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase d3ee0be9080f4572ad3be32e94da906d53dc8987 --onto bedcbfcfeed429428c3e7f008b6984fc8c2b2b76. (2024-06-15 14:59:49)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase d3ee0be9080f4572ad3be32e94da906d53dc8987 --onto 1cf71e54cf268e87cf5c43c830d953f5c88e6c39. (2024-06-17 14:01:05)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase d3ee0be9080f4572ad3be32e94da906d53dc8987 --onto 62b6e5878981d1bb6d414f21b0c6f8d8a36e6834. (2024-06-27 10:33:11)

[tydeu]

Suggested change

	self.pkg.nativeLibDir / nameToStaticLib s!"{self.config.libName}Fat"
	self.pkg.nativeLibDir / self.staticLibFileName.addExtension "fat"

I would be inclined to give this extension .a.fat like the export and noexport variants. When Is there a reason you avoided that approach?

[bollu]

@tydeu I didn't want to hamper the default behaviour of ld searching for -lfoo as libfoo.a, so I preferred to keep the .a as the rightmost extension.

[tydeu]

@bollu My thought process is that I wouldn't expect a user to be shipping all 3 different variants of the static library but instead just distribute the appropriate one as libfoo.a. Internally, in Lake, the full name can be easily used without concern.

One problem with having a suffix just for this version of the library is that it can conflict with a library name ending in a normal library ending with the same suffix. For example, a Lean library named BigFat's normal static library would conflict with the Lean library Big's fat static library. As this would be a very confusing issue for a user to debug, it would probably be best to ensure all static libraries have non-overlapping suffixes (or none) to avoid this.

[tydeu]

Should the fat library really have exported symbols? Exported symbols are generally only for dynamic libraries. Statically linking a library will cause symbol resolution regardless of export.

Suggested change

	mod.nativeFacets (shouldExport := true) |>.mapM fun facet => fetch <| mod.facet facet.name
	mod.nativeFacets (shouldExport := false) |>.mapM fun facet => fetch <| mod.facet facet.name

If the exported symbols are expected to be needed, then it may be necessary to have export / noexport variants of the fat library just like the standard static library. With exported symbols, it is easy for a fat library to surpass Windows symbol limits.

[tydeu]

I have finally reviewed this PR. My apologies for taking so long! 🙏

There are some elements that need discussion and potential rework -- see the line-by-line comments for details. However, overall, I think you are on the right track, and I would be happy to see this PR merged!

[digama0]

I think it is a bit misleading to call this a "fat library", and suggest using the term "statically linked" instead. "fat binaries" are the usual term for binaries which simultaneously contain code from multiple architectures (e.g. x86 and ARM), with some header information so that they can be correctly run in multiple environments. The technique is fairly rarely used; a notable recent application of the technique is in Apple binaries during the ARM transition period. See also Fat binary.

[tydeu]

@digama0

I think it is a bit misleading to call this a "fat library", and suggest using the term "statically linked" instead.

Statically linked is too general for this. The standard static library Lake produces is also statically linked (as would be any static library). Furthermore, it is perfectly normal for a static library to not contain symbols from other (public) libraries, so it would weird to use the general term for the currently name "fat" version.

Maybe we could call this a "standalone" static library instead of a "fat" one?