chore: USE_LAKE: integrate into CMake

[Kha]

Proof of concept built while at GPN. With USE_LAKE=ON, only linking is now left to the Makefile.

• Moved lib/temp/lib*.a.export to lib/lean/ as Lake puts both versions in the same place, excluded from install with a glob instead
• Mostly eliminated leanc.sh as Lake expects bin/leanc, used only as a trivial wrapper in stage0/bin now.

TODO:

• include stage 0 changes in Lake's trace. This is an issue already on master but prevents us from using this PR to put .oleans in an Actions cache.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Batteries CI can not be attempted yet, as the nightly-testing-2024-06-16 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Batteries CI should run now. (2024-06-16 20:02:30)