Thanks for your work here -- this is a really cool project!!
I found it pretty nontrivial to get this to work with GPU support. Since I am on nixos, dependencies like openblas are difficult to compile without finnicking a bunch with (due to things like weird dynamic linker). It is much easier for me to pass a pre-built openblas and have lean link against that.
My feature request would be to add a configuration where building only tries to download models instead of also building system dependencies from source. I took an extreme approach to this and nuked all the dependency build steps.
This would unblock me (and probably any other nixos users) from packaging the c++ parts of this project and just having lean link directly against the packaged libraries.
I did eventually get this working. For others on nixos trying to get this to work:
There were some further issues probably caused by running on lean version v4.26.0. I had to stub out a bunch of definitions in ct2.ccp for the extern definitions defined in lean that weren't found when running a sample project. Also, the GPU allocator seems to segfault on free for some reason (probably a bug I made in these additions to ct2.ccp). My current solution to this is to...just not call free. Maybe not an amazing solution haha but it seems to work. When I make calls to the copilot lib, I get proofs detected by leanls.
I also had to pass in the built c++ shared object files of this project using LD_PRELOAD when building the lean portion (I'm not exactly sure why lean isn't picking up on LD_LIBRARY_PATH or rpath). But that's a bit easier to deal with comparatively.
Thanks for your work here -- this is a really cool project!!
I found it pretty nontrivial to get this to work with GPU support. Since I am on nixos, dependencies like openblas are difficult to compile without finnicking a bunch with (due to things like weird dynamic linker). It is much easier for me to pass a pre-built openblas and have lean link against that.
My feature request would be to add a configuration where building only tries to download models instead of also building system dependencies from source. I took an extreme approach to this and nuked all the dependency build steps.
This would unblock me (and probably any other nixos users) from packaging the c++ parts of this project and just having lean link directly against the packaged libraries.
I did eventually get this working. For others on nixos trying to get this to work:
There were some further issues probably caused by running on lean version v4.26.0. I had to stub out a bunch of definitions in ct2.ccp for the extern definitions defined in lean that weren't found when running a sample project. Also, the GPU allocator seems to segfault on free for some reason (probably a bug I made in these additions to ct2.ccp). My current solution to this is to...just not call free. Maybe not an amazing solution haha but it seems to work. When I make calls to the copilot lib, I get proofs detected by leanls.
I also had to pass in the built c++ shared object files of this project using LD_PRELOAD when building the lean portion (I'm not exactly sure why lean isn't picking up on LD_LIBRARY_PATH or rpath). But that's a bit easier to deal with comparatively.