fix: link `libLeanExport.a` into executables that link Lake

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 is 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.
5 files changed