lean-dojo / LeanCopilot

LLMs as Copilots for Theorem Proving in Lean
https://leandojo.org
MIT License
1k stars 92 forks source link

Building LeanCopilot package to use GPU #104

Closed vanessalama09 closed 3 months ago

vanessalama09 commented 3 months ago

@yangky11 I'm also trying to build Lean Copilot on NVIDIA cuda-compatible GPU. I was able to build locally, but on the GPU, it's throwing an error at the same stage as above. A little about the machine:

The build error:

ℹ [3/1126] 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/1126] 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

A little help would be much appreciated!

Originally posted by @vanessalama09 in https://github.com/lean-dojo/LeanCopilot/discussions/76#discussioncomment-10151380