Adding Lake itself as a dependency?

Stream: lean4

[Chris Lovett]

I'm trying to lake build a project containing this code (using lean nightly-2021-12-28)

import Lake
#eval Lake.leanVersionString

but I'm getting a link error :

error: ld.lld: error: undefined symbol: initialize_Lake

My .elan\toolchains\leanprover--lean4---nightly-2021-12-28\lib\lean folder contains Lake.olean and a Lake folder full of more .oleans, are these not found automatically? How does one add them as a dependency in a Lake package file?

[Sebastian Ullrich]

We do not ship with native static or shared libraries for Lake yet (we would probably want both, so there is a non-negligble space overhead in doing so). Do you actually want to create an executable from it, given that you do not have a main function? Lake change the default build action compared to Leanpkg from building .oleans to building executables, though I feel like this might not be the most sensible choice given the expected average Lean 4 project.

[Chris Lovett]

Right I meant to include a main function in my sample, but I see that .oleans are not enough, one has to also provide the .a libraries... I guess we can't yet jit the .a libraries from .olean files... given that we now ship clang, could we jit them instead of shipping them? Might be able to get better performing libraries if they are jitted on the user's CPU...

[Sebastian Ullrich]

That should technically be possible, but lean does not currently allow for generating .c directly from .olean files.

Might be able to get better performing libraries if they are jitted on the user's CPU...

That should always be opt-in since generated binaries should be distributable by default.

[Mac]

Sebastian Ullrich said:

That should technically be possible, but lean does not currently allow for generating .c directly from .olean files.

Having learned a bit more since the last time we discussed this, it seems to me like this would not be that difficult to support. One could just import the olean and then running the C code emitter, right? The C code emitter just works of the IR and I believe the environment details necessary for the getting the IR are preserved in the .olean, correct?