lean-dojo/leancopilot

LLMs as Copilots for Theorem Proving in Lean

leancopilot's Issues

Windows Support

I'm not sure how important it is to support Windows (how many Lean users actually use Windows?)

Detect Model Updates

When the models on Hugging Face are updated, we want to re-download them.

Proof Suggestion Format Issue

It looks like there are some spurious newlines, probably due to updates to Lean's functions for displaying tactic suggestions.

https://github.com/yangky11/lean4-example/tree/ml4tp-tutorial

Hardcoded Version of CTranslate2

Hard-coding this may cause problems when CTranslate2 is upgraded.

LeanCopilot/lakefile.lean

Line 256 in f00ec56

-- TODO: Don't hardcode the version "4".

Errors caused by breaking changes in `lean4:v4.3.0-rc2`

Hi Mac @tydeu,

I just noticed the changes in lean4:v4.3.0-rc2 to the directory structures. They caused a few errors in LeanDojo and LeanInfer, which I'm trying to fix. This line was
https://github.com/lean-dojo/LeanInfer/blob/dc8e2b7f4deb648733cd20f913bca812ea0ed3f0/lakefile.lean#L54
, but I changed it to
https://github.com/lean-dojo/LeanInfer/blob/b2925d5f99b35fb7b1c3ef8ad506916c4fa3fa52/lakefile.lean#L54

However, I got the following error when running lake build in a downstream package depending on lean4:v4.3.0-rc2 + LeanInfer:

error: > LEAN_PATH=./.lake/packages/std/.lake/build/lib:./.lake/packages/Qq/.lake/build/lib:./.lake/packages/aesop/.lake/build/lib:./.lake/packages/Cli/.lake/build/lib:./.lake/packages/proofwidgets/build/lib:./.lake/packages/mathlib/.lake/build/lib:./.lake/packages/LeanInfer/.lake/build/lib:./.lake/build/lib LD_LIBRARY_PATH=/home/kaiyu/local/usr/lib:/home/kaiyu/clang+llvm-13.0.1-x86_64-linux-gnu-ubuntu-18.04/lib/x86_64-unknown-linux-gnu:/home/kaiyu/clang+llvm-13.0.1-x86_64-linux-gnu-ubuntu-18.04/lib:/usr/local/cuda/lib64::./.lake/packages/LeanInfer/.lake/build/lib:./.lake/packages/LeanInfer/.lake/build/lib /home/kaiyu/.elan/toolchains/leanprover--lean4---v4.3.0-rc2/bin/lean --load-dynlib=./.lake/packages/LeanInfer/build/lib/libonnxruntime.so --load-dynlib=./.lake/packages/LeanInfer/build/lib/libctranslate2.so ./.lake/packages/LeanInfer/././LeanInfer/Frontend.lean -R ./.lake/packages/LeanInfer/./. -o ./.lake/packages/LeanInfer/.lake/build/lib/LeanInfer/Frontend.olean -i ./.lake/packages/LeanInfer/.lake/build/lib/LeanInfer/Frontend.ilean -c ./.lake/packages/LeanInfer/.lake/build/ir/LeanInfer/Frontend.c --load-dynlib=./.lake/packages/LeanInfer/.lake/build/lib/libleanffi.so
error: stderr:
libc++abi: terminating due to uncaught exception of type lean::exception: error loading library, ./.lake/packages/LeanInfer/build/lib/libonnxruntime.so: cannot open shared object file: No such file or directory
error: external command `/home/kaiyu/.elan/toolchains/leanprover--lean4---v4.3.0-rc2/bin/lean` exited with code 134

Presumably, the error is because s!"-L{__dir__}/build/lib" doesn't exist for lean4:v4.3.0-rc2. Depending on the Lean version, either s!"-L{__dir__}/build/lib" or s!"-L{__dir__}/.lake/build/lib" exists, but not both. Is there a way to make the project work for both lean4:v4.3.0-rc2 and older versions of Lean?

Thanks!

CI

Trying to use Lean Copilot to develop the std library but hitting a build dependency cycle

@yangky11 @semorrison @tydeu I'd like to use Lean Copilot to develop std library proofs but the normal install instructions fail. Copilot depends on std, so std can't depend on copilot.

Should it be possible to use Lean Copilot to develop std? If so, what do you recommend?

Thanks.

---

I tried to hack this by renaming my local instance of std to be std4 but I couldn't get it working. That said, I don't know Lean's build system. If it's useful, here's what I tried:

-- lakefile.lean
-package std where
+package std4 where

-- I also added the moreLinkArgs and require LeanCopilot lines

# alias Std/ as Std4/ and create Std4.lean
ln -s Std Std4
cp Std.lean Std4.lean

# rename Std references to Std4 in both Std4.lean and all *.lean files within Std/
sed -i '' -e 's/Std/Std4/g' Std4.lean
pushd Std
for f in `find . -iname '*.lean'`; do
  sed -i '' -e 's/Std/Std4/g' $f
  sed -i '' -e 's/Std4in/Stdin/g' $f
done
popd

Running lake clean; lake build makes progress for awhile but eventually hits this:

...

[126/307] Building Std4.Lean.Meta.Simp
[127/307] Building Std4.Lean.Format
error: > LEAN_PATH=./.lake/packages/std/.lake/build/lib:./.lake/packages/aesop/.lake/build/lib:./.lake/packages/LeanCopilot/.lake/build/lib:./.lake/build/lib DYLD_LIBRARY_PATH=./.lake/build/lib /Users/atlas/.elan/toolchains/leanprover--lean4---v4.5.0-rc1/bin/lean -Dlinter.missingDocs=true ./././Std4/Tactic/CoeExt.lean -R ././. -o ./.lake/build/lib/Std4/Tactic/CoeExt.olean -i ./.lake/build/lib/Std4/Tactic/CoeExt.ilean -c ./.lake/build/ir/Std4/Tactic/CoeExt.c
error: stdout:
./././Std4/Tactic/CoeExt.lean:8:25: error: unknown namespace 'Std4'
./././Std4/Tactic/CoeExt.lean:31:10: error: unknown identifier 'elabTerm'
./././Std4/Tactic/CoeExt.lean:32:19: error: unknown identifier 'coerceToFunction?'
./././Std4/Tactic/CoeExt.lean:35:42: error: unknown identifier 'indentExpr'
./././Std4/Tactic/CoeExt.lean:39:10: error: unknown identifier 'elabTerm'
./././Std4/Tactic/CoeExt.lean:40:19: error: unknown identifier 'coerceToSort?'
./././Std4/Tactic/CoeExt.lean:43:38: error: unknown identifier 'indentExpr'
./././Std4/Tactic/CoeExt.lean:55:11: error: function expected at
  ToExpr
term has type
  ?m.2380
./././Std4/Tactic/CoeExt.lean:72:11: error: function expected at
  ToExpr
term has type
  ?m.4293
./././Std4/Tactic/CoeExt.lean:77:20: error: function expected at
  SimpleScopedEnvExtension
term has type
  ?m.4326
./././Std4/Tactic/CoeExt.lean:78:2: error: unknown identifier 'registerSimpleScopedEnvExtension'
./././Std4/Tactic/CoeExt.lean:77:20: error: function expected at
  SimpleScopedEnvExtension
term has type
  ?m.4370
./././Std4/Tactic/CoeExt.lean:76:0: error: initialization function '[email protected]._hyg.762' must have type of the form `IO <type>`
./././Std4/Tactic/CoeExt.lean:84:32: error: function expected at
  CoreM
term has type
  ?m.4428
./././Std4/Tactic/CoeExt.lean:87:5: error: unknown namespace 'PrettyPrinter.Delaborator'
./././Std4/Tactic/CoeExt.lean:94:49: error: unknown identifier 'whenPPOption'
./././Std4/Tactic/CoeExt.lean:107:57: error: function expected at
  MetaM
term has type
  ?m.4492
./././Std4/Tactic/CoeExt.lean:121:71: error: function expected at
  MetaM
term has type
  ?m.4549
./././Std4/Tactic/CoeExt.lean:137:11: error: unknown identifier 'registerBuiltinAttribute'
error: external command `/Users/atlas/.elan/toolchains/leanprover--lean4---v4.5.0-rc1/bin/lean` exited with code 1
[127/307] Building Std4.Tactic.NoMatch
[128/307] Compiling Std.Linter.UnreachableTactic
error: > LEAN_PATH=./.lake/packages/std/.lake/build/lib:./.lake/packages/aesop/.lake/build/lib:./.lake/packages/LeanCopilot/.lake/build/lib:./.lake/build/lib DYLD_LIBRARY_PATH=./.lake/build/lib /Users/atlas/.elan/toolchains/leanprover--lean4---v4.5.0-rc1/bin/lean -Dlinter.missingDocs=true ./././Std4/Lean/Format.lean -R ././. -o ./.lake/build/lib/Std4/Lean/Format.olean -i ./.lake/build/lib/Std4/Lean/Format.ilean -c ./.lake/build/ir/Std4/Lean/Format.c
error: stdout:
./././Std4/Lean/Format.lean:18:33: error: unknown identifier 'prettyM'
error: external command `/Users/atlas/.elan/toolchains/leanprover--lean4---v4.5.0-rc1/bin/lean` exited with code 1

Premise Selection on GPUs

We only select premises on CPUs but want to make it work also for GPUs.

LeanCopilot/cpp/ct2.cpp

Line 246 in 8c7b338

// TODO: We should remove this line when everything can work well on CUDA.

@Peiyang-Song . A recent discussion on Zulip may be relevant: https://leanprover.zulipchat.com/#narrow/stream/219941-Machine-Learning-for-Theorem-Proving/topic/LeanCopilot/near/418208166

Lean 4.5.0 , not working

I added the lines

require LeanCopilot from git "https://github.com/lean-dojo/LeanCopilot.git" @ v1.1.0

moreLinkArgs := #["-L./.lake/packages/LeanCopilot/.lake/build/lib", "-lctranslate2"]

In the end of a fresh lakefile.lean file, a new project!

ar@tranco puzzles % lean -v
Lean (version 4.5.0, commit 1a3021f98e55, Release)
ar@tranco puzzles % elan show
installed toolchains
--------------------

leanprover/lean4:nightly-2023-12-31
leanprover/lean4:stable (default)

active toolchain
----------------

leanprover/lean4:stable (overridden by '/Users/ar/r/puzzles/lean-toolchain')
Lean (version 4.5.0, commit 1a3021f98e55, Release)

ar@tranco puzzles % lake update LeanCopilot   
error: ./lakefile.lean:14:78: error: unknown identifier 'v1'
error: ./lakefile.lean:14:82: error: invalid field notation, identifier or numeral expected
error: ./lakefile.lean:14:83: error: unexpected token; expected command
error: ./lakefile.lean: package configuration has errors

any idea?

CI Failed

https://github.com/lean-dojo/LeanCopilot/actions/runs/8420847569/job/23057242430

LeanInfer could not build when tested on Github Codespace

The issues were posted on Zulip, please check there for more context.

TL;DR

1. Github Codespace can only compile after -stdlib=libc++ is removed
2. lake build hangs indefinitely in linking, and it's not using much CPU

Issue Details

I've tried out lean4-example in Github Codespace, I got the following issues:

1. lake build fails to compile C++ with Clang++, resolved by removing all -stdlib=libc++from the lakefile of LeanInfer

lean4-example (improve-installation) $ lake build
[23/197] Compiling ffi.cpp
error: > clang++ -c -o ./lake-packages/LeanInfer/build/ffi.o ./lake-packages/LeanInfer/ffi.cpp -fPIC -std=c++11 -stdlib=libc++ -O3 -I /home/codespace/.elan/toolchains/leanprover--lean4---v4.0.0/include
error: stderr:
In file included from ./lake-packages/LeanInfer/ffi.cpp:1:
/home/codespace/.elan/toolchains/leanprover--lean4---v4.0.0/include/lean/lean.h:14:10: fatal error: 'atomic' file not found
#include <atomic>
         ^~~~~~~~
1 error generated.
error: external command `clang++` exited with code 1

I ran bash -c "$(wget -O - https://apt.llvm.org/llvm.sh)" from https://apt.llvm.org/ to fix it, no change.
Then I test the clang++ command with extra options -E -x c++ -v at the end, it showed the following search path:

ignoring nonexistent directory "/include"
#include "..." search starts here:
#include <...> search starts here:
 /home/codespace/.elan/toolchains/leanprover--lean4---v4.0.0/include
 /usr/local/include
 /usr/lib/llvm-10/lib/clang/10.0.0/include
 /usr/include/x86_64-linux-gnu
 /usr/include
End of search list.

which is shorter than a raw clang++ -E -x c++ - -v < /dev/null 2>&1 which shows

ignoring nonexistent directory "/include"
ignoring duplicate directory "/usr/bin/../lib/gcc/x86_64-linux-gnu/9/../../../../include/x86_64-linux-gnu/c++/9"
#include "..." search starts here:
#include <...> search starts here:
 /usr/bin/../lib/gcc/x86_64-linux-gnu/9/../../../../include/c++/9
 /usr/bin/../lib/gcc/x86_64-linux-gnu/9/../../../../include/x86_64-linux-gnu/c++/9
 /usr/bin/../lib/gcc/x86_64-linux-gnu/9/../../../../include/c++/9/backward
 /usr/local/include
 /usr/lib/llvm-10/lib/clang/10.0.0/include
 /usr/include/x86_64-linux-gnu
 /usr/include
End of search list.

Clearly Clang++ stop looking for the GNU C++ headers if -stdlib=libc++ is present. If Github Codespace misses it I guess it would be missed in the environments of many end-users.

2. After resolved issue 1, I end up having the same issue fatal error: 'onnxruntime_cxx_api.h' file not found, resolved by

( cd /workspace/ && wget https://github.com/microsoft/onnxruntime/releases/download/v1.15.1/onnxruntime-linux-x64-1.15.1.tgz && tar xzvf  onnxruntime-linux-x64-1.15.1.tgz)

Then add "-I", "/workspaces/onnxruntime-linux-x64-1.15.1/include" to flags in LeanInfer lakefile or just add CPATH environment variable as instructed.

3. Run lake build after step 2, I have the same linker error libc++abi: terminating due to uncaught exception of type lean::exception: error loading library, libonnxruntime.so.1.15.1: cannot open shared object file: No such file or directory, I tried to fix it by adding "-L", "/workspace/onnxruntime-linux-x64-1.15.1/lib/" to moreLinkArgs then

LD_LIBRARY_PATH=/workspaces/onnxruntime-linux-x64-1.15.1/lib/ lake build

But the build hangs indefinitely, and it's not using much CPU (<3%). So far, I'm stuck here.

buildArchive?

Hi @tydeu,

I recently upgraded to the latest Lean v4.6.0-rc1 and found that now I have to manually add the OS and tar.gz to buildArchive?. Just wanted to double-check if that's expected.

LeanCopilot/lakefile.lean

Line 65 in 4bc4e6c

def buildArchiveName : String :=

Please see these two commits:
965d4ba
4bc4e6c

difficulty installing on MacOS, CTranslate2 related

my lakefile:

import Lake
open Lake DSL
require scilean from git "https://github.com/lecopivo/SciLean" @ "master"
require LeanCopilot from git "https://github.com/lean-dojo/LeanCopilot.git" @ "v1.1.2"

package ScileanExtra where
  moreLinkArgs := #[
    "-L./.lake/packages/LeanCopilot/.lake/build/lib",
    "-lctranslate2"
  ]


lean_lib «ScileanExtra» where

@[default_target]
lean_exe «scilean-extra» where
  root := `Main

try to import leancopilot gives:

Failed responding to request 14423: error loading library, dlopen(./.lake/packages/LeanCopilot/.lake/build/lib/libleanffi.dylib, 0x0009): Library not loaded: @rpath/libctranslate2.3.dylib
  Referenced from: <4C4C44DC-5555-3144-A126-85C66AEB5F51> /Users/alokbeniwal/scilean-extra/.lake/packages/LeanCopilot/.lake/build/lib/libleanffi.dylib (built for macOS 99.0 which is newer than running OS)
  Reason: tried: './.lake/packages/std/.lake/build/lib/libctranslate2.3.dylib' (no such file), 
-- (etc)

the strange thing is that the files do seem to exist

.lake/packages/LeanCopilot/.lake/build/include/ctranslate2/
.lake/packages/LeanCopilot/.lake/build/lib/libctranslate2.3.dylib
.lake/packages/LeanCopilot/.lake/build/lib/libctranslate2.4.dylib
.lake/packages/LeanCopilot/.lake/build/lib/libctranslate2.dylib
.lake/packages/LeanCopilot/.lake/build/lib/libctranslate2.dylib.hash
.lake/packages/LeanCopilot/.lake/build/lib/libctranslate2.dylib.trace

Usability Improvements

• Installation (cloud release, testing)
• Interface for user-provided models
• Documentation