fix: link libLeanExport.a into executables that link Lake

[Kha]

This PR fixes a link failure in downstream packages that build an executable: libLake.a references LeanExport symbols, but -lLeanExport was missing from the static link line, so linking failed with undefined initialize_LeanExport_Parse, runtime_initialize_LeanExport_Parse and l_LeanExport_parseStream.

lake challenge made Lake depend on LeanExport, and LAKESHARED_LINKER_FLAGS was updated accordingly, but LEANC_STATIC_LINKER_FLAGS was not. Lean core libs are linked statically into executables on every platform but Windows (see LeanExe.sharedLean), so this affected essentially every downstream executable importing Lake. The new linkLake Lake test builds and runs such an executable, importing Lake.All so that all of Lake's cross-library references are exercised.

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2026-08-29 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-29 11:20:46)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-08-29 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-08-29 11:20:48)