Lake native libraries include main symbol

[SchrodingerZhu]

see the issue at digama0/lean-sys#5.

lean4/src/lake/lakefile.lean

Line 6 in 63d2bdd

lean_lib Lake

In lake, it seems that, when Main resides in the lib source directory, the main symbol will also live inside the lib. Is this by design?

[Kha]

No, this was not intended. @tydeu This is a bit of a problem, lean.mk identifies package files by folder, not import graph. So there is no easy way to exclude everything not reachable from Lake.lean from libLake.a. We can add this to the list of things that would be made easier by building the Lean libraries with Lake but for now we could simply move Lake/Main.o out of the archive manually after the fact.

[digama0]

I'm not sure it would be correct to leave out everything not reachable from Lake.lean from libLake.a either, because that file was optimized for import Lake to be usable in lakefiles, while libLake.a should also include functions for interacting with lake's data structures. I previously requested to @tydeu that they split lake into a library and an executable, but they declined, so just deleting Lake/Main.o seems like the lowest-maintenance approximation to this.

[tydeu]

I'm not sure it would be correct to leave out everything not reachable from Lake.lean from libLake.a either, because that file was optimized for import Lake to be usable in lakefiles, while libLake.a should also include functions for interacting with lake's data structures.

The things missing from Lake.lean are Lake.CLI (except Lake.CLI.Actions) and Lake.Load. This could be solved with a separate Lake/LibMain.lean that imports these and is used as the build source for lean_lib Lake (if Lake is built with Lake).