Installing Lean Copilot but have "git" problem

Stream: Machine Learning for Theorem Proving

[Albert.J]

I was trying to install Lean Copilot and encountered problem when running "lake exe LeanCopilot/download", it says "process 'git' exited with code 128". I'm using Mac 15 Air, M3 chip, and my lean-toolchain version is v4.10.0-rc2 so I set the LeanCopilot version to be v1.4.1.
Pictures of my terminal :down:
1.png
2.png
3.png

And I ran lake build despite the "process 'git' exited with code 128", here follows the picture of my VScode after that.
4.png

How can I fix it?

[Kaiyu Yang]

It looks like an issue when Git attempts to download or update the model checkpoint. Maybe try deleting ~/.cache/lean_copilot and re-run everything? If it doesn't work, please open an issue on GitHub.

[Richard Copley]

Hard to say. Git prints a message on stderr and exits with error code 128 when something called its die function (ref), but the Lean function IO.Process.run used here to run git throws away the stderr. So there's some debugging (or guessing) to do.

Do you have enough disk space for the objects being downloaded?
Can you deduce the relevant git commands and run them directly in the terminal for yourself?

[Albert.J]

Kaiyu Yang said:

It looks like an issue when Git attempts to download or update the model checkpoint. Maybe try deleting ~/.cache/lean_copilot and re-run everything? If it doesn't work, please open an issue on GitHub.

I tried your method but it still has "git 128" error. I opened an issue under your project in github, you can see more details there. https://github.com/lean-dojo/LeanCopilot/issues/103#issue-2428819916

[Albert.J]

Richard Copley said:

Hard to say. Git prints a message on stderr and exits with error code 128 when something called its die function (ref), but the Lean function IO.Process.run used here to run git throws away the stderr. So there's some debugging (or guessing) to do.

Do you have enough disk space for the objects being downloaded?
Can you deduce the relevant git commands and run them directly in the terminal for yourself?

It's a new Mac, to install the Lean Copilot is one of the first things so there is enough space. I also attempted to run the relevant git commands directly in the terminal, e.g. git remote set-url origin git@github.com:lean-dojo/LeanCopilot.git, ssh -T git@github.com, git clone , looks good. However, the 128 issue persists. Could you provide further guidance ?

[Jasper Ganten]

I also got a problem during the installation of LeanCopilot. Id be grateful if you could help me troubleshoot it.

>>>lake exe LeanCopilot/download
ℹ [3/18] Replayed LeanCopilot/libopenblas
info: Cloning OpenBLAS from https://github.com/OpenMathLib/OpenBLAS
info: Building OpenBLAS with `make NO_LAPACK=1 NO_FORTRAN=1 -j32`
✖ [4/18] Building LeanCopilot/libctranslate2
info: Cloning CTranslate2 from https://github.com/OpenNMT/CTranslate2
error: no such file or directory (error code: 2)
  file: ././.lake/packages/LeanCopilot/.lake/build/lib/libctranslate2.so
Some builds logged failures:
- LeanCopilot/libctranslate2
error: build failed

I'm quite irritated by this since it works on my Laptop. The server I'm running it on has cmake version 3.30.2 and gcc > 8.3.0 installed. I basically adapted the example from the Leancopilot Repo for testing.
I already tried deleting the .lake folder and the cache. Thanks!

[Bulhwi Cha]

I have the same problem installing LeanCopilot:

chabulhwi@desktop ~/l/lean-playground> lake exe LeanCopilot/download
ℹ [3/18] Replayed LeanCopilot/libopenblas
info: Cloning OpenBLAS from https://github.com/OpenMathLib/OpenBLAS
info: Building OpenBLAS with `make NO_LAPACK=1 NO_FORTRAN=1 -j32`
✖ [4/18] Building LeanCopilot/libctranslate2
info: Cloning CTranslate2 from https://github.com/OpenNMT/CTranslate2
error: no such file or directory (error code: 2)
  file: ././.lake/packages/LeanCopilot/.lake/build/lib/libctranslate2.so
Some builds logged failures:
- LeanCopilot/libctranslate2
error: build failed

I use Slackware Linux and have installed GCC 13.2.0 and 14.2.0. Here's my lakefile.lean:

lakefile.lean

import Lake
open Lake DSL

package «playground» where
 -- Settings applied to both builds and interactive editing
 leanOptions := #[
   ⟨`pp.unicode.fun, true⟩, -- pretty-prints `fun a ↦ b`
   ⟨`pp.proofs.withType, false⟩
 ]
 -- add any additional package configuration options here
 moreLinkArgs := #[
   "-L./.lake/packages/LeanCopilot/.lake/build/lib",
   "-lctranslate2"
 ]

require mathlib from git
 "https://github.com/leanprover-community/mathlib4.git" @ "v4.10.0-rc1"

meta if get_config? env = some "dev" then -- dev is so not everyone has to build it
require «doc-gen4» from git
 "https://github.com/leanprover/doc-gen4" @ "main"
require LeanCopilot from git "https://github.com/lean-dojo/LeanCopilot.git" @ "v1.4.1"

@[default_target]
lean_lib «Playground» where
 -- add any library configuration options here

[恭良夜]

(deleted)

[恭良夜]

Albert.J said:

I was trying to install Lean Copilot and encountered problem when running "lake exe LeanCopilot/download", it says "process 'git' exited with code 128". I'm using Mac 15 Air, M3 chip, and my lean-toolchain version is v4.10.0-rc2 so I set the LeanCopilot version to be v1.4.1.
Pictures of my terminal :down:
1.png
2.png
3.png

And I ran lake build despite the "process 'git' exited with code 128", here follows the picture of my VScode after that.
4.png

How can I fix it?

I encountered the same problem as you, did you solve it? Could you please let me know if it has been resolved?