Lean server crashes after LeanCopilot is used in more advanced topics

[scherblu]

When running Lean Copilot v1.4.1 with Lean 4's language v4.10.0-rc1 (including mathlib which I imported completely) in more advanced topics, the Lean server crashes. My operating system is Debian GNU/Linux 12 (bookworm). Thank you in advance for looking into this issue!

I attempted to use Lean Copilot with Kevin Buzzard's Lean 4 course. It worked successfully on the initial logic chapter but failed in more advanced topics like measure theory (e.g. Section13Sheet1). Specifically, the Lean server crashed after I typed commands such as suggest_tactics and search_proof.

Is this a known issue? When LeanCopilot does not find a tactic or a proof, does LeanCopilot print such a note that or is the Lean server supposed to crash?

[scherblu]

Note, this is the error message:

error: Lean exited with code 132 Some builds logged failures:

• TestCopilot2.measure_theory error: build failed

[Peiyang-Song]

Hi @scherblu , thank you for the report! This is not a known issue and is quite interesting. Generally when LeanCopilot fails at a very hard goal it is indeed not expected to cause a server crash. The error message seems not very meaningful though, as it just indicates a build failure of a file outside Lean Copilot's core. It would be very helpful if you could provide a mwe for a simple case where, when applying Lean Copilot's suggest_tactics to an advanced theorem, a server crash is resulted. I would be very interested to reproduce and look into it. Thanks!

[jganten]

Hello, I tested it on wsl with this code (basically the referenced sheet) and got the same error:

import Mathlib
import LeanCopilot

-- let X be a set
variable (X : Type)

example (A : Set X) :
    (MeasurableSpace.generateFrom {A}).MeasurableSet' =
    ({∅, A, Aᶜ, ⊤} : Set (Set X)) := by
  --suggest_tactics
  search_proof
end

Both tactics result in a server crash. The Server crashes do not contain a lot of information therefore I compiled the file manually.

Compilation output for search_proof case is attached: search_proof_error_on_wsl.txt The other case is similar.

[scherblu]

Hey, thank you @Peiyang-Song. I tried to use Lean v4.9.0 and not v4.10.0-rc1 (and downloading mathlib4 locally like @harrytherealhero proposed in a different issue for the copilot) with Copilot v1.4.0 but I got now the following error after lake build (before that, everything worked successfully). I just like to mention that, maybe it is helpful for you.

`/home/peiyangsong/LeanCopilot/.lake/build/CTranslate2/src/models/model.cc: At global scope: /home/peiyangsong/LeanCopilot/.lake/build/CTranslate2/src/models/model.cc:454:17: warning: ‘bool ctranslate2::models::replace(std::string&, const string&, const string&)’ defined but not used [-Wunused-function] 454 | static bool replace(std::string& str, const std::string& from, const std::string& to) { | ^~~ /home/peiyangsong/LeanCopilot/.lake/build/CTranslate2/src/models/model.cc: In static member function ‘static std::shared_ptr ctranslate2::models::Model::load(ctranslate2::models::ModelReader&, ctranslate2::Device, int, ctranslate2::ComputeType, bool, bool)’: /home/peiyangsong/LeanCopilot/.lake/build/CTranslate2/src/models/model.cc:739:34: warning: ‘current_index’ may be used uninitialized in this function [-Wmaybe-uninitialized] 739 | if (outputs.size() > current_index && !outputs[current_index].empty()) | ^~~~~ /home/peiyangsong/LeanCopilot/.lake/build/CTranslate2/src/models/model.cc:718:92: warning: ‘world_size’ may be used uninitialized in this function [-Wmaybe-uninitialized] 718 | dim_t dim_per_kqv_per_partition = SAFE_DIVIDE(variable.dim(outer_dim) / 2, world_size); | ^~~~~~ ✖ [13/15] Building Main trace: .> LEAN_PATH=././.lake/packages/batteries/.lake/build/lib:././.lake/packages/Qq/.lake/build/lib:././.lake/packages/aesop/.lake/build/lib:././.lake/packages/proofwidgets/.lake/build/lib:././.lake/packages/Cli/.lake/build/lib:././.lake/packages/importGraph/.lake/build/lib:/home/scherberger/code_bin/test_copilot_local_mathlib/test_copilot_LEANLOC/mathlib4/.lake/build/lib:././.lake/packages/LeanCopilot/.lake/build/lib:././.lake/build/lib LD_LIBRARY_PATH=././.lake/build/lib /home/scherberger/.elan/toolchains/leanprover--lean4---v4.9.0/bin/lean ././././Main.lean -R ./././. -o ././.lake/build/lib/Main.olean -i ././.lake/build/lib/Main.ilean -c ././.lake/build/ir/Main.c --json error: ././././Main.lean:4:24: unknown identifier 'hello' error: Lean exited with code 1 Some builds logged failures:

• Main error: build failed`

[Peiyang-Song]

@jganten Thanks very much for the example. I just tried Lean Copilot on this theorem, and both suggest_tactics and search_proof did work without errors. Here are two screenshots of using both tools from Lean Copilot on this goal, and getting responses as expected.

suggest_tactics:

search_proof:

In general, it is possible that Lean Copilot may find some theorems harder than others, and its capability dealing with different theorems can vary. Nonetheless I have not observed (nor would I expect that to happen) any instances where Lean Copilot produces a server crash when facing a hard theorem.

[Peiyang-Song]

@scherblu Thank you for the report! From looking at the log of building failure, it looks like the failure is caused directly by an error in your Main.lean file. The error seems to be due to an unknown identifier "hello". I do not recall we ever introduced such an identifier in the source of Lean Copilot, and given that the error comes from Main.lean, it is likely that the error is caused by part of your main file.

[Peiyang-Song]

I am closing this issue now. Thank you both for your detailed discussions! Feel free to report anything new that you find interesting.