LeanCopilot Setup

Stream: Machine Learning for Theorem Proving

[Daniel Rehsmann]

Im trying to get LeanCopilot running, in order to obtain some help when learning LEAN.
However I have some troubles to get it running. So my question is addressed at someone who is actually working with this CoPilot.

My Environment.
OS: Fedora 41
Editor: neovim0.10.4
Lean version: 4.18.0-rc1
Lake version: 5.0.0-69a1d04

When trying to build, I obtain following messages:

info: stderr:
libc++abi: terminating due to uncaught exception of type lean::exception: error loading library, libctranslate2.so.4: cannot open shared object file: No such file or directory
error: Lean exited with code 134

I have included
moreLinkArgs = ["-L./.lake/packages/LeanCopilot/.lake/build/lib", "-lctranslate2"]
at the top of my toml. It seams to me that this is the source of error.

And get it using

[[require]]
name = "LeanCopilot"
git = "https://github.com/lean-dojo/LeanCopilot.git"
rev = "main"

The library libctranslate2.so.4, is present at /.lake/packages/LeanCopilot/.lake/build/lib/
But a folder /.lake/packages/LeanCopilot/.lake/build/CTranslate2 is entirely missing. I dont know if this is the default.

[Janos Wolosz]

I see you found a solution to the problem—thanks, it helped me out!
https://github.com/lean-dojo/LeanCopilot/issues/153

By the way, when using LeanCopilot with mathlib4, do you also experience that Copilot somehow confuses the Lean cache?

[Daniel Rehsmann]

Hey no problem. In my fork I also incorporated cuda and cudnn acceleration, which was turned off by default. So you can use hardware acceleration if you want.

How do you see this confusion?

[Janos Wolosz]

I am getting the following error message during the lake exe cache get step:
Failed to connect to lakecache.blob.core.windows.net port 443 after 34 ms: Couldn't connect to server

This never happens when my branch is independent of LeanCopilot.

My setup method can be summarized as follows (assuming I am on a local branch that was branched off from mathlib4's master):

1. Merge my dojo branch.
2. Run lake update LeanCopilot.
3. Run lake exe cache get.
4. Run lake build.

If I forget to get the cache on the original branch before the merge, step 4 will take a very long time.

[Kevin Buzzard]

You could try disabling your antivirus if you're on windows (antivirus is responsible for some network issues sometimes) but I'm not optimistic that this will solve your problem

[Daniel Rehsmann]

I see - but it seems to me that Lean Copilot is only supported on Windows WSL. In which step does this error occur? Building libraries? Downloading models?

You can try to manually download the llms.
Also make sure you have git-lfs installed.

[Janos Wolosz]

Thanks for your helpful attitude! Let me emphasize that after applying @Daniel Rehsmann 's fix, LeanCopilot is working on my Ubuntu system—it’s just not very convenient to apply it to a new branch after branching off from the mathlib4 master.

I’m attaching the log of my lake exe cache get step. To be honest, I already find it quite suspicious that some C++ compilation is taking place during a cache retrieval step.

That said, my experience with LeanCopilot has been quite positive. While it can’t handle mathematically challenging steps for me, search_proof is quite useful for dealing with coercions, simp, and similar issues. In my experience, it’s definitely smarter than apply?, so as a beginner Lean user, I find it to be a really helpful tool.
lean_copilot_cache_get_log.txt

[Daniel Rehsmann]

It seems that you have troubles downloading mathlib4. ‘lake update’, does not incur errors?

[Janos Wolosz]

Exactly. I have trouble downloading the mathlib4 cache, but only when LeanCopilot is added to lakefile.lean. Without LeanCopilot, everything works fine, and I can get the repository running in a minute.

Even with LeanCopilot, lake update completes without errors. I'm just curious if anyone else has encountered this. But since I have a workaround, I don't think this needs deep investigation.