feat: lake: improved platform information & control

[tydeu]

This combines a few platform-related changes:

• Add a ternary platformIndependent Lean configuration option to assert whether Lake should assume Lean code is platform-independent. If true, Lake will exclude platform-independent objects like external libraries or dynlibs created through precompileModules from module traces. If false, Lake will add the platform to module traces. If none (the default), Lake will retain the current behavior (modules are platform-dependent if and only if it depends on native objects).
• Use System.Platform.target from feat: System.Platform.target #3207 as the platform descriptor in Lake for the configuration file trace, the cloud release archive, and as the platform trace in Lean modules and native artifacts (e.g., object files, and static and shared libraries).
• Do not add the platform descriptor into custom build archive names (i.e., a user-set buildArchive configuration). This allows users to create cross-platform / platform-independent archives via a name override should they so desire.

Closes #2754.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-3226 build failed against this PR. (2024-01-29 17:31:09) View Log
• 💥 Mathlib branch lean-pr-testing-3226 build failed against this PR. (2024-01-29 18:12:04) View Log
• 💥 Mathlib branch lean-pr-testing-3226 build failed against this PR. (2024-01-30 16:41:00) View Log
• ✅ Mathlib branch lean-pr-testing-3226 has successfully built against this PR. (2024-01-31 00:53:00) View Log
• ✅ Mathlib branch lean-pr-testing-3226 has successfully built against this PR. (2024-01-31 02:07:56) View Log
• ✅ Mathlib branch lean-pr-testing-3226 has successfully built against this PR. (2024-01-31 22:43:32) View Log
• ✅ Mathlib branch lean-pr-testing-3226 has successfully built against this PR. (2024-02-01 00:25:58) View Log

[kim-em]

Can we verify that

git checkout lean-pr-testing-3226
elan toolchain uninstall leanprover/lean4-pr-releases:pr-release-3226 # make sure we have the latest PR toolchain
lake exe cache get

works in Mathlib before merging this? It seems to not retrieve any oleans at present.

[tydeu]

@semorrison I am confused, how would this prevent cache from downloading oleans? It is my understanding the cache uses it own custom traces for oleans. If this broke anything, I would think it would be lake build rebuilding mathlib.

[kim-em]

@semorrison I am confused, how would this prevent cache from downloading oleans? It is my understanding the cache uses it own custom traces for oleans. If this broke anything, I would think it be lake build rebuilding mathlib.

I suspect it is just that you force pushed just recently, so no update to date oleans are available right now anyway. So not an indication of a problem, just a request that we run this check successfully at least once before merging!

(I don't want to have something hit nightly on release day that could conceivably break the cache, without checking!)

[tydeu]

@semorrison I just tested (now the cache is uploaded) and lake exe cache get && lake build works for me. Does it work for you as well (testing on each of our different platforms seems wise)?

[tydeu]

!bench

[leanprover-bot]

Here are the benchmark results for commit c49da9a.
There were no significant changes against commit 5f59d7f.