How to install LeanCopilot?

Stream: new members

[Justus Willbad]

I read https://github.com/lean-dojo/LeanCopilot?tab=readme-ov-file#using-lean-copilot-in-your-project. But I have 3 files lakefile.lean in my project directory and dozens in the .elan directory.

In which file and at which place I have to add the package configuration option "moreLinkArgs..."?

[Kevin Buzzard]

You can't have three files with exactly the same name in one directory, that is not a thing. Or do you mean "in various subdirectories of my project directory", which doesn't sound right either.

[Justus Willbad]

I have a lakefile.lean in the directories Oq, proofwidgets and mathlib.
(I don't know what lakefile is. I'm only a possible user, not a software progammer.)

[Ruben Van de Velde]

These are under .lake, right?

[Bulhwi Cha]

Here's my lakefile.lean for my Lean project playground:

My 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.11.0"
require LeanCopilot from git "https://github.com/lean-dojo/LeanCopilot.git" @ "v1.6.0"

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

1. Run lake new playground math to create a new project called playground.
2. Go to the playground directory and make sure the content of the lean-toolchain file is leanprover/lean4:v4.11.0.
3. Replace the content of the lakefile.lean with the one I provided above.

[Kevin Buzzard]

Oh if you're poking around in .lake then this sounds right. What are you doing in there? That's a system directory, there's nothing of interest to a user in there (that's why its name begins with a dot).

[Justus Willbad]

I cannot find a file lakefile.lean. I'm working with VSCode and Windows.

[Ruben Van de Velde]

Do you have a lakefile.toml?

[Justus Willbad]

Yes, I have.

[Kevin Buzzard]

That's the file you should be changing, although I don't know the syntax. You might want the authors of LeanCopilot to update their readme. However you might find it easier just to use github copilot or the tool assistance offered by IDEs such as Cursor, I suspect that they outperform leancopilot and are much easier to install.

[Justus Willbad]

The code is written here: https://github.com/lean-dojo/LeanCopilot?tab=readme-ov-file#using-lean-copilot-in-your-project

[Kevin Buzzard]

I know, and it gives you instructions about how to install leancopilot in a project which has been set up with a lakefile.lean, which is now an old-fashioned way to set up a simple project. The instructions have not been updated. My point is that if you just use github copilot or cursor then it just works and you don't need to fiddle with any system files.

[Bulhwi Cha]

Kevin Buzzard said:

That's the file you should be changing, although I don't know the syntax. You might want the authors of LeanCopilot to update their readme.

Here it is:

My lakefile.toml

name = "playground"
version = "0.1.0"
keywords = ["math"]
defaultTargets = ["Playground"]
moreLinkArgs = ["-L./.lake/packages/LeanCopilot/.lake/build/lib", "-lctranslate2"]

[leanOptions]
pp.unicode.fun = true # pretty-prints `fun a ↦ b`
autoImplicit = false

[[require]]
name = "mathlib"
scope = "leanprover-community"
rev = "v4.11.0"

[[require]]
name = "LeanCopilot"
scope = "lean-dojo"
rev = "v1.6.0"

[[lean_lib]]
name = "Playground"

@Justus Willbad Replace the default lakefile.toml with mine.

[Justus Willbad]

The same problem is at installing Proofmaker.

The next problem is: I don't know how to get he old version v4.11.0 of Lean in VSCode.

[Bulhwi Cha]

Justus Willbad said:

The same problem is at installing Proofmaker.

Sorry, but I don't know about it.

The next problem is: I don't know how to get he old version v4.11.0 of Lean in VSCode.

1. Run lake new playground math to create a new project called playground.
2. Go to the playground directory and make sure the content of the lean-toolchain file is leanprover/lean4:v4.11.0.
3. Replace the content of the lakefile.toml with the one I provided above.
4. Follow instructions No. 3–5 in the section Adding Lean Copilot as a Dependency.

[Justus Willbad]

After many many hours: I give up here too: too many riddles. There isn't described where I have to enter the commands, and VSCode prints error messages in each second step.

That means I'm also unable to use Lean.

[Dominic Steinitz]

Justus Willbad said:

After many many hours: I give up here too: too many riddles. There isn't described where I have to enter the commands, and VSCode prints error messages in each second step.

That means I'm also unable to use Lean.

I too tried to install lean copilot and gave up. I am still able to use lean though and am happily proving things.

[Jason Rute]

Cc @Kaiyu Yang

[Justus Willbad]

Now I found the following.
"TOML require
To require a package in a TOML configuration, the parallel syntax for the above examples is:
A Git dependency:
[[require]]
name = "<pkg-name>"
git = "<url>"
rev = "<rev>"
subDir = "<subDir>"

How I have to type in the following information into my lakefile.toml?

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

require Paperproof from git "https://github.com/Paper-Proof/paperproof.git"@"main"/"lean"

lake update LeanCopilot and lake update Paperproof give an error.

https://github.com/Paper-Proof/paperproof
https://github.com/lean-dojo/LeanCopilot

[Bulhwi Cha]

Justus Willbad said:

After many many hours: I give up here too: too many riddles.

I used Konsole to run the commands. It works fine for me.

[Bulhwi Cha]

There isn't described where I have to enter the commands, and VSCode prints error messages in each second step.

That means I'm also unable to use Lean.

You have to run these commands on terminal emulators. Do you know how to use terminal emulators? What operating system are you using?

[Bulhwi Cha]

Justus Willbad said:

How I have to type in the following information into my lakefile.toml?

lakefile.toml

name = "playground"
version = "0.1.0"
keywords = ["math"]
defaultTargets = ["Playground"]
moreLinkArgs = ["-L./.lake/packages/LeanCopilot/.lake/build/lib", "-lctranslate2"]

[leanOptions]
pp.unicode.fun = true # pretty-prints `fun a ↦ b`
autoImplicit = false

[[require]]
name = "mathlib"
scope = "leanprover-community"
rev = "v4.11.0"

[[require]]
name = "paperproof"
scope = "Paper-Proof"
rev = "21e4ec999c23fc6181d6528cbaecb600a2db6851"

[[require]]
name = "LeanCopilot"
scope = "lean-dojo"
rev = "v1.6.0"

[[lean_lib]]
name = "Playground"

[Bulhwi Cha]

From https://github.com/leanprover/lean4/blob/master/RELEASES.md#lake-6:

Running lake translate-config toml will produce a lakefile.toml version of a package's lakefile.lean. Any configuration options unsupported by the TOML format will be discarded during translation, but the original lakefile.lean will remain so that you can verify the translation looks good before deleting it.

[Justus Willbad]

I'm working with the current versions of Lean and VSCode under Windows.
I changed lakefile.toml and lean-toolchain in the project directory playground as you said.
There is no lakefile.lean in this directory for translating.

How can I proceed?
lake update LeanCopilot gives the error lakefile.lean: error: no such file or directory
lake exe LeanCopilot/download gives the error: dependency 'LeanCopilot' not in manifest; use lake update LeanCopilot to add it

I used C:\Windows\System32\cmd.exe from the playground directory with and without adminstrator rights and I use the command line under Strg Shift P in VSCode.

At https://lean-lang.org/functional_programming_in_lean/hello-world/starting-a-project.html, there is nothing written about files lakefile.toml.

[Bulhwi Cha]

Justus Willbad said:

lake update LeanCopilot gives the error lakefile.lean: error: no such file or directory

I don't know why you got this error. Your project has lakefile.toml.

I used C:\Windows\System32\cmd.exe from the playground directory with and without adminstrator rights and I use the command line under Strg Shift P in VSCode.

Have you installed Git for Windows? This includes Git Bash, a Bash emulation used to run Git from the command line. I recommend using Git Bash directly.

[Bulhwi Cha]

I'm beginning to think that a Unix shell tutorial for a complete beginner might be helpful for everyone, including those trying to configure a Lean project.

[Justus Willbad]

I used Git Bash, went to my directory "playground" and typed in: lake update LeanCopilot.

Git Bash wrote:
$ lake update LeanCopilot
PANIC at getOS! lakefile:16:4: Windows is not supported
trace: .\.\.lake\packages\LeanCopilot> git fetch --tags --force origin
error: .\.\.lake\packages\proofwidgets\lakefile.lean:20:20: error: invalid argument name 'text' for function 'Lake.buildFileAfterDep'
error: .\.\.lake\packages\proofwidgets\lakefile.lean:46:2: error: invalid field 'afterBuildCacheAsync', the environment does not contain 'Lake.Package.afterBuildCacheAsync'
pkg
has type
Package
error: .\.\.lake\packages\proofwidgets\lakefile.lean: package configuration has errors

I think the problem is that the outdated instructions need lakefile.lean, but with the current Lean versions, my project directory has only a lakefile.toml.
The problem isn't the Windows command shell.
How can I proceed with the lakefile.toml without lakefile.lean?
or
How can I get a right lakefile.lean in my project directory?

[Bulhwi Cha]

Oh, I forgot that LeanCopilot doesn't support native Windows.

[Bulhwi Cha]

From https://github.com/lean-dojo/LeanCopilot?tab=readme-ov-file#requirements:

Supported platforms: Linux, macOS, and Windows WSL; :warning: Native Windows currently not supported.

[Bulhwi Cha]

I think learning to use a native Linux distribution is beneficial, although it requires effort and time.

[Kaiyu Yang]

The next problem is: I don't know how to get he old version v4.11.0 of Lean in VSCode.

You don't need to (anymore). I just updated LeanCopilot to work with the current stable Lean version v4.14.0.

[Jason Rute]

@Kaiyu Yang I’m not finding a release for v4.14.0/x86_64macOS . Do you still support x86 Macs?

[Kaiyu Yang]

@Jason Rute I cannot provide a prebuilt x86 Mac binary since I don't have a X86 Mac anymore. You could try to build it locally without cloud release?

[Jason Rute]

I can try. (But I thought ARM Macs let you build universal binaries for both x86 and ARM.)

[Jason Rute]

Also, here are some other issues with the current LeanCopilot:

• lake new myprojectname math now defaults to making a lakefile.toml file instead of a lakefile.lean. It isn't clear how the instructions for Lean Copilot adapt. You can use lake new myprojectname math.lean to make the lakefile.lean, but I don't know how to change it after. Does LeanProject work with .toml files. If so, what are the parts that need to be added?
• I've found that I need to explicitly set the version of mathlib to prevent lake from trying to bump lean to v4.15.0-rc (since Copilot doesn't work with that version). This looks like require "leanprover-community" / "mathlib" @ "git#v4.14.0" does the trick (or at least it is a way I figured out to do this).

[Kaiyu Yang]

@Jason Rute

(But I thought ARM Macs let you build universal binaries for both x86 and ARM.)

That may be possible. However, since LeanCopilot builds its dependencies OpenBLAS and CTranslate2, it may require modifying the building scripts of these dependencies, which I currently don't have the bandwidth to look into.

Does LeanProject work with .toml files.

Yes, I updated LeanCopilot's README to add instructions for lake.toml.

I've found that I need to explicitly set the version of mathlib to prevent lake from trying to bump lean to v4.15.0-rc (since Copilot doesn't work with that version).

I just updated LeanCopilot to support v4.15.0-rc. Now it uses the same convention with other Lean packages: The main branch tries to keep up to date with the most recent Lean version, and it will have a stable branch for the most recent stable version, as well as one release (e.g., tagged v4.14.0) for each stable version of Lean. Hopefully this will mitigate the headache with versions.

[Justus Willbad]

I have problems to find/start VSCode or Lean that I installed in Ubuntu.
LeanCopilot is designed for Linux and WSL. Is it enough to start VSCode under Windows, load the WSL extension therein and go to WSL therein?

[Kaiyu Yang]

I have problems to find/start VSCode or Lean that I installed in Ubuntu.

I believe you can enter WSL, open a terminal in WSL, and type the command for VS Code (maybe code or something).

[Justus Willbad]

I didn't want to believe it: I had to disable my firewall, Lean installed now. That's horrible!
Many many thanks to all of you.

[Notification Bot]

Justus Willbad has marked this topic as resolved.

[Notification Bot]

Justus Willbad has marked this topic as unresolved.

[Justus Willbad]

Lean 4 under WSL in VSCode under Windows works with Lean 4 version 4.15.0-rc1. But LeanCopilot needs version 4.11.0.

If I type another version into my file lean-toolchain, e.g. v.4.14.0, and use "import Mathlib" in my lean-file, I get the error "Lean exited with code 1".

What can I do?

[Kevin Buzzard]

If you change your lean-toolchain then you'll also need to change your lakefile so that it's compatible

[Jason Rute]

@Kaiyu Yang above said it no longer requires 4.11 (or even 4.14).

[Jason Rute]

@Kevin Buzzard how do you change the lakefile? I gave a way above to set mathlib, but I don’t know if that was right?

[Kevin Buzzard]

I don't know the details, I was just pretty confident that you never just change lean-toolchain and nothing else. I always follow instructions mindlessly rather than making things up as I go along or understanding what's actually happening.

I just made a new project with lake new testproj math, edited lean-toolchain by changing it from 4.15.0-rc1 to v.14.0, then typed lake exe cache get and lean-toolchain is back on 4.15.0-rc1.

[Jason Rute]

Here is how I found to set the version, but not sure if canonical:

Jason Rute said:

I've found that I need to explicitly set the version of mathlib to prevent lake from trying to bump lean to v4.15.0-rc (since Copilot doesn't work with that version). This looks like require "leanprover-community" / "mathlib" @ "git#v4.14.0" does the trick (or at least it is a way I figured out to do this).

[Jason Rute]

But it is fine now to use v4.15.0-rc for Lean Copilot (or v14.4.0). For the rc version I think you use “main” instead of “v4.15.0-rc”.

Kaiyu Yang said:

I've found that I need to explicitly set the version of mathlib to prevent lake from trying to bump lean to v4.15.0-rc (since Copilot doesn't work with that version).

I just updated LeanCopilot to support v4.15.0-rc. Now it uses the same convention with other Lean packages: The main branch tries to keep up to date with the most recent Lean version, and it will have a stable branch for the most recent stable version, as well as one release (e.g., tagged v4.14.0) for each stable version of Lean. Hopefully this will mitigate the headache with versions.

[Justus Willbad]

Unfortunately, in the current Lean we have the file lakefile.toml instead of lakefile.lean. But Lean needs lakefile.lean for correcting some errors.

Therefore I used the lakefile.lean presented by Bulhwi Cha at 11:09 AM, as presented above and with version v4.14.0 of both mathlib and LeanCopilot and got the following errors.

Cannot build project. Command output: warning: manifest out of date: git url of dependency 'mathlib' changed; use lake update mathlib to update it warning: manifest out of date: git revision of dependency 'mathlib' changed; use lake update mathlib to update it error: dependency 'LeanCopilot' not in manifest; use lake update LeanCopilot to add it

After typing lake update mathlib:
info: mathlib: URL has changed; you might need to delete '.\.\.lake\packages\mathlib' manually
trace: .\.\.lake\packages\mathlib> git fetch --tags --force origin
info: LeanCopilot: URL has changed; you might need to delete '.\.\.lake\packages\LeanCopilot' manually
trace: .\.\.lake\packages\LeanCopilot> git fetch --tags --force origin
error: .\.\.lake\packages\LeanCopilot\lakefile.lean:66:17: error: no such file or directory (error code: 2)
error: .\.\.lake\packages\LeanCopilot\lakefile.lean:68:5: error: no such file or directory (error code: 2)
error: .\.\.lake\packages\LeanCopilot\lakefile.lean: package configuration has errors

After typing lake update LeanCopilot:
info: LeanCopilot: URL has changed; you might need to delete '.\.\.lake\packages\LeanCopilot' manually
trace: .\.\.lake\packages\LeanCopilot> git fetch --tags --force origin
error: .\.\.lake\packages\LeanCopilot\lakefile.lean:66:17: error: no such file or directory (error code: 2)
error: .\.\.lake\packages\LeanCopilot\lakefile.lean:68:5: error: no such file or directory (error code: 2)
error: .\.\.lake\packages\LeanCopilot\lakefile.lean: package configuration has errors

What can I do?

[Eric Wieser]

Justus Willbad said:

But Lean needs lakefile.lean for correcting some errors.

What do you mean by this?

[Kaiyu Yang]

Sounds like deleting .lake before running lake update might help?

[Justus Willbad]

Eric Wieser schrieb:

Justus Willbad said:

But Lean needs lakefile.lean for correcting some errors.

What do you mean by this?

with lakefile.toml:
stderr: error: dependency 'LeanCopilot' not in manifest; use lake update LeanCopilot to add it Invalid Lake configuration. Please restart the server after fixing the Lake configuration file.

[Kevin Buzzard]

And what happens if you follow the instructions given in this error?

[Justus Willbad]

See the errors in the post above from 12:13 AM.

[Kaiyu Yang]

I'm happy to take a look (on my Mac) if @Justus Willbad can provide a GitHub repo of your code and a list of commands I can run to re-produce the error.

[Justus Willbad]

The newest version of LeanCopilot is given at github as 4.14.0, of paperproof 1.6.4.

Using lakefile.lean and using lakefile.toml given below gave the same errors as presented above.
https://github.com/lean-dojo/LeanCopilot
https://github.com/Paper-Proof/paperproof

[Jason Rute]

(deleted)

[Jason Rute]

(Sorry for my deleted message. I misread the version numbers you gave.)

[Eric Wieser]

Justus Willbad said:

See the errors in the post above from 12:13 AM.

Aren't the errors from this post the ones from creating a lakefile.lean?

[Justus Willbad]

Yes, they are.

Lean with lakefile.toml says: "Cannot build project. Command output: warning: manifest out of date: "
lake update LeanCopilot and lake update Paperproof give the other errors.

I think the lakefile.lean comes from Git.

[Bulhwi Cha]

Kaiyu Yang said:

Sounds like deleting .lake before running lake update might help?

@Justus Willbad Have you deleted the .lake directory? You might also have to delete the lake-manifest.json file.

[Kaiyu Yang]

The newest version of LeanCopilot is given at github as 4.14.0

The latest release is v4.14.0, but the current main branch uses v4.15.0-rc1.

[Jason Rute]

@Justus Willbad I think if you want to get this resolved, you may need to be a bit more systematic in your investigation:

1. Create a new Lean project and install Lean Copilot in it.
2. If you get errors, then share your exact steps or do what @Kaiyu Yang suggested and put your code in a GitHub repo.
3. If it works, then slowly start to make that test project look more like your actual project, and try it again. Go back to step 2.

Alternately, you could copy your repo (only the code, not any files or directories starting with ., like .lake), and try to run lake on that project, but that might be a bit more confusing. Also, it is hard for others to reproduce your errors unless you make your repo public for others to investigate. So I would recommend starting over from scratch first.

[Justus Willbad]

Now I got the following error:
.../example.lean Init LeanCopilot` failed:
stderr:
✖ [3/555] Building LeanCopilot/libopenblas
info: Cloning OpenBLAS from https://github.com/OpenMathLib/OpenBLAS
error: no such file or directory (error code: 2)
file: ././.lake/packages/LeanCopilot/.lake/build/lib/libopenblas.so
Some required builds logged failures:

• LeanCopilot/libopenblas
  error: build failed

My file example.lean contains the example from https://github.com/lean-dojo/LeanCopilot - Getting Started with Lean Copilot:

import LeanCopilot
example (a b c : Nat) : a + b + c = a + c + b := by
suggest_tactics

suggest_tactics is written white, not blue.

I tried mathlib versions v4.14.0 and v4.15-rc1 (in accordance with my file lean-toolchain) together with LeanCopilot v4.14.0 and v1.6.0.

I installed WSL (Ubuntu), installed VSCode in this WSL-Ubuntu and load Lean 4 extension and WSL extension in this VSCode and opened my file example.lean in this VSCode WSL extension.
I had to create my project through lakefile.lean because creating through lakefile.toml gaver errors.
I have all administrator rights and no firewall.

[Jason Rute]

@Justus Willbad While someone more experienced might instantly recognize this error, it would probably help to give more context:

• what did you do differently to get this error instead of the previous error?
• what specific command did you run to get this error?
• what setup did you do before that command? (Is this the same project as before or a fresh one like I suggested above?)
• what does your lakefile look like?

[Justus Willbad]

Here is the content of the lakefile.lean I used:

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.14.0"
require Paperproof from git "https://github.com/Paper-Proof/paperproof.git" @ "main"/"lean"
require LeanCopilot from git "https://github.com/lean-dojo/LeanCopilot.git" @ "v4.14.0"

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

[Kevin Buzzard]

Triple backticks ``` to make your posts of code readable. See #mwe for more information on posting code.

[Justus Willbad]

I wasn't able to use LeanCopilot under Windows WSL with VSCode with WSL extension with user rights or administrator rights. Therefore I now tried to use LeanCopilot in VSCode under Ubuntu.

But I got the following error messages. What can I do?

/home/kubuntu/.elan/toolchains/leanprover--lean4---v4.17.0-rc1/bin/lake setup-file /home/kubuntu/Theorem10.lean Init Mathlib LeanCopilot failed:
stderr:
✖ [6027/6417] Building LeanCopilot/libopenblas
info: Cloning OpenBLAS from https://github.com/OpenMathLib/OpenBLAS
error: no such file or directory (error code: 2)
file: ././.lake/packages/LeanCopilot/.lake/build/lib/libopenblas.so
Some required builds logged failures:

• LeanCopilot/libopenblas
  error: build failed

my lean-toolchain file:

leanprover/lean4:v4.17.0-rc1

my lakefile.lean:

import Lake
open Lake DSL
package «playground» where
leanOptions := #[
⟨pp.unicode.fun, true⟩, -- pretty-prints fun a ↦ b ⟨pp.proofs.withType, false⟩
]
moreLinkArgs := #[
"-L./.lake/packages/LeanCopilot/.lake/build/lib",
"-lctranslate2"
]

require mathlib from git "https://github.com/leanprover-community/mathlib4.git" @ "v4.17.0-rc1"
require LeanCopilot from git "https://github.com/lean-dojo/LeanCopilot.git" @ "main"

I installed libopenblas in and outside VSCode and typed in "lake update LeanCopilot", but the error message remains.

[Bulhwi Cha]

Follow instructions No. 2 in the section Adding Lean Copilot as a Dependency. Hmm, you've already set the correct version of LeanCopilot.

[Bulhwi Cha]

@Justus Willbad I've moved the Lean toolchain to v4.17.0-rc1, and now I have no problem using LeanCopilot. I use Slackware Linux.