building with depencies

Stream: lean4

[Patrick Massot]

I'm trying to have two local Lean packages. One is a library and the other is a program. I want them to be in different folder, managed by different git repositories. In the program lakefile I use require MyLib from ".."/"my-lib" and it works just fine in VSCode. Then I lake build and there is no complain. But when I try to run the executable then it complains about "unknown package MyLib".

[Sebastian Ullrich]

Building a Lean executable will not include all the .olean files in the binary, or make them available in any other way. I assume you are already calling initSearchPath, you need to pass the path to MyLib to it manually

[Patrick Massot]

Thanks, that was enough to get me going. But one day I'll have to understand this for real.

[Patrick Massot]

Is there any documentation for simple use cases like? I can't find the string "initSearchPath" in the lake README.

[Sebastian Ullrich]

Building a Lean metaprogram, something that reads and analyzes/manipulates Lean programs and proofs, is far from a simple use case. The most appropriate place to document this would probably be in the metaprogramming book, but I don't see it there yet.

[Patrick Massot]

I guess I probably don't need this then, because I'm not trying to do something complicated.

[Sebastian Ullrich]

Now I'm a bit confused. You should only get that error from your program if you're trying to do something complicated/"meta".

[Patrick Massot]

To be honest, I don't quite remember what I'm doing. I'm resuming work on a project that I abandoned for one month because term started and then I had a conference deadline :flushed: