leancopilot installation

Stream: new members

[Dominic Steinitz]

I am following the instructions here: https://github.com/lean-dojo/LeanCopilot and have updated my lakefile.lean to be

import Lake
open Lake DSL

package mil where
  moreLinkArgs := #[
      "-L./.lake/packages/LeanCopilot/.lake/build/lib",
      "-lctranslate2"
      ]
  leanOptions := #[
    ⟨`pp.unicode.fun, true⟩, -- pretty-prints `fun a ↦ b`
    ⟨`autoImplicit, false⟩,
    ⟨`relaxedAutoImplicit, false⟩]

@[default_target]
lean_lib MIL where

require mathlib from git "https://github.com/leanprover-community/mathlib4"@"master"
require LeanCopilot from git "https://github.com/lean-dojo/LeanCopilot.git" @ "v1.6.0"

but running lake build gives the error

dom@Wandle mathematics_in_lean % lake build
✖ [10/2385] (Optional) Fetching LeanCopilot:optRelease
trace: downloading https://github.com/lean-dojo/LeanCopilot/releases/download/v1.6.0/x86_64-macOS.tar.gz
trace: .> curl -s -S -f -o ././.lake/packages/LeanCopilot/.lake/x86_64-macOS.tar.gz -L https://github.com/lean-dojo/LeanCopilot/releases/download/v1.6.0/x86_64-macOS.tar.gz
trace: stderr:
curl: (22) The requested URL returned error: 404
error: external command 'curl' exited with code 22
error: build failed

And indeed when I look here https://github.com/lean-dojo/LeanCopilot/releases there is no such file and presumably I should use https://github.com/lean-dojo/LeanCopilot/releases/download/v1.6.0/arm64-macOS.tar.gz.

But how do I convince lake / lean to use this?

Lean 4.12.0
Lake version 5.0.0-src (Lean version 4.12.0-rc1)

[Dominic Steinitz]

So it looks like the lean installation instructions give you an x86_64 version of lean and not arm64.

Lean (version 4.12.0-rc1, x86_64-apple-darwin22.6.0, commit e9e858a44849, Release)

[Jason Rute]

Cc @Kaiyu Yang

[Kaiyu Yang]

Hi, please open an issue in LeanCopilot's GitHub repo. @Peiyang Song is the maintainer and may be able to assist you.

[Dominic Steinitz]

There was already an issue for this and I have solved it: https://github.com/lean-dojo/LeanCopilot/issues/117#issuecomment-2382913583.

Now I have another problem lol: https://github.com/lean-dojo/LeanCopilot/issues/125. I think this might be a version issue as LeanCopilot seems to be set up for Lean 4.11 and I am running 4.12 (not sure about the OP). I will wait for @Peiyang Song to respond.

[Dominic Steinitz]

Actually forget that. After I reinstalled lean to use arm64 rather than x86_64, I now have

Lean (version 4.11.0, arm64-apple-darwin23.6.0, commit ec3042d94bd1, Release)