installing lean copilot

Stream: lean4

[秋天]

Is there anyone using leancopilot? I am trying to install it on my windows wsl ubuntu env. but after downloading everything needed, the config file rasies an error,which leads to the server breaking down
image.png
image.png
first image show the config in the leancopilot .the second shows the config in the whole project. My whole installing totally followed the leandojo's documents. plz help me :smiling_face_with_tear:

[Notification Bot]

A message was moved here from #lean4 > Accessing inductive hypothesis after using <;> by Mario Carneiro.

[Jason Rute]

@Kaiyu Yang :up:

[Kaiyu Yang]

I just tried with Windows WSL but was unable to reproduce the problem. I have WSL with git, VS Code, elan, and the Lean 4 VS Code extension installed. I ran the following commands to get the LeanCopilot-demo branch of lean4-examle and download the models.

git clone https://github.com/yangky11/lean4-example
cd lean4-example
git checkout LeanCopilot-demo
lake exe LeanCopilot/download

Then, I ran code . to launch VS Code and opened the Lean4Example.lean file, which worked.

Could you please try and let me know if it works?

[yefim]

Hi, I meat a problem when I use leancopilot+win11 wsl2 too.
I install elan in wsl and update lean to v4.7.0, then I clone the lean4-example/LeanCopilot-demo and open it in VS Code:

git clone -b LeanCopilot-demo http://github.com/yangky11/lean4-example
cd lean4-example

I run these command in sequence:

1. lake update LeanCopilot
2. lake exe LeanCopilot/download
3. lake build
   It goes wrong in the last step, the terminal shows:

[484/485] Building Lean4Example
error: > LEAN_PATH=./.lake/packages/std/ xxxxxxxxxx(a lot of paths)
error: stdout:
./././Lean4Example.lean:10:2: error: process 'git' exited with code 1
./././Lean4Example.lean:13:2: error: tactic 'aesop' failed, made no progress
a b c d : Nat
⊢ a + b + c + d = a + (c + b) + d
error: external command `/home/yefim/.elan/toolchains/leanprover--lean4---v4.7.0/bin/lean` exited with code 1

The LeanCopilot statement also shows:
image.png
image.png

And the Output in VS Code(Ctrl+Shift+U) print that:

[Error - 3:20:29 PM] Request textDocument/foldingRange failed.
  Message: Server process for file:///mnt/d/Workspace/Lean/lean4-example/Lean4Example.lean crashed, likely due to a stack overflow or a bug.
  Code: -32902

Does anyone else have the same problem?

[Richard Copley]

Maybe ... . My error from lake build in that recipe is

error: stderr:
terminate called after throwing an instance of 'thrust::system::system_error'
terminate called recursively
error: external command `/home/buster/.elan/toolchains/leanprover--lean4---v4.7.0/bin/lean` exited with code 134

Note that the LEAN_PATH=<lean_path> LD_LIBRARY_PATH=<ld_library_path> <command> <args> is not just a list of paths; it's the command that was run. (VAR=xxx yyy is sh syntax for adding VAR=xxx to the environment of the new process for the command yyy.) This gives you the possibility to run the same command in the debugger:

LEAN_PATH=<lean_path> LD_LIBRARY_PATH=<ld_library_path> lldb <command> -- <args>

or

LEAN_PATH=<lean_path> LD_LIBRARY_PATH=<ld_library_path> gdb --args <command> <args>

So maybe that will give you a clue for further debugging. (For me, at this point I give up. Sorry!)

[Joseph Tooby-Smith]

I'm getting the following error when running the lake update LeanCopilot command in the setup instructions :

error: ././.lake/packages/LeanCopilot/lakefile.lean:180:8: error: unknown identifier 'logStep'
error: ././.lake/packages/LeanCopilot/lakefile.lean:185:8: error: unknown identifier 'logStep'
error: ././.lake/packages/LeanCopilot/lakefile.lean:236:8: error: unknown identifier 'logStep'
error: ././.lake/packages/LeanCopilot/lakefile.lean:241:8: error: unknown identifier 'logStep'
error: ././.lake/packages/LeanCopilot/lakefile.lean:244:8: error: unknown identifier 'logStep'
warning: ././.lake/packages/LeanCopilot/lakefile.lean:283:75: warning: `Lake.SchedulerM` has been deprecated, use `Lake.SpawnM` instead
error: ././.lake/packages/LeanCopilot/lakefile.lean:290:33: error: application type mismatch
  @compileO { toString := path.toString } oFile deps[0]!
argument
  deps[0]!
has type
  FilePath : outParam Type
but is expected to have type
  optParam (Array String) #[] : Type
error: ././.lake/packages/LeanCopilot/lakefile.lean: package configuration has errors

Maybe this is a Lean version issue? I'm using v4.8.0-rc1. Is anyone running lean copilot with v4.8.0-rc1?

[Matthew Ballard]

It looks like LeanCopilot is on v4.7.0

[Adam Topaz]

@Kaiyu Yang

[Kaiyu Yang]

We're currently working on supporting v4.8.0 and it should be ready in a few days.