Difficulty installing leancopilot(Mac)

Stream: lean4

[Jared green]

I tried to install leancopilot, this is what I get
image.jpg

[Jason Rute]

Please copy and paste the error or at least take a screenshot.

[Jason Rute]

Cc @Kaiyu Yang

[Jason Rute]

And explain the steps you did and where you got stuck. That would make it easiest to assist you.

[Jared green]

I followed the steps in the leancopilot readme immediately after installing lean and dependencies. I have not updated curl.

$ lake update LeanCopilot
warning; Qq: ignoring missing dependency manifest ‘./.lake/packages/Qq/lake-manifest.json’
warning: Cli: ignoring missing dependency manifest ‘./.lake/packages/Cli/lake-manifest.json’
mathlib: running post-update hooks
Warning: recommended ‘curl’ version >=7.70. Found 7.64.1. Can’t use ‘--parallel.’
No files to download
Decompressing 4291 file(s)
unpacked in 72690 ms
$ lean exe LeanCopilot/download
error unknown package ‘LeanCopilot’
$

[Jared green]

apparently I couldn’t send from my Mac so I had to type that out.

[Kaiyu Yang]

@Jared green Please open an issue in the LeanCopilot GitHub repo. Thx

[Jared green]

Done

[Jared green]

@Peiyang Song I had mistyped here and then copied from here. However apparently I cannot reopen the issue.

[Peiyang Song]

I reopened it.

[Jared green]

i got another problem. pardon any remaining errors in this, i had to get creative about getting it here.

$ lake exe LeanCopilot/download
info: [1/91] Linking libleanffi.dylib

info: [11/91] Building ModelCheckpointManager.Url

error: > LEAN PATH:-Lake/packages/Std/-Lake/build/Lib::/.Lake/packages/Qq/-lake/build/Lib:./-lake/packages/aesop/.1ake/build/Lib: ./.Lake/packages/proofwidgets/-Lake/build/Lib:=/-lake/packages/C11/.lake/build/lib:./.lake/packages/importGraph/- Lake/build/1b::. Lake/packages/mathlib/-Lake/butld/Lib::/-Lake/packages/auto/.lake/build/lib:./.lake/packages/Duper/-Lake/build/103-Lake packages/Leancopilot/- Lake/but ld/Lib: ./-lake/build/Lib DYLD_LIBRARY_ PATH-./. lake/packages/LeanCop Lot/-lake/build/tb::/-lake/packages/LeanCopilot/.lake/build/Lib /users/programr/.elan/toolchains/lean
-v4.7.0-c1/bin/lean -load-dynlib=./. lake/packages/LeanCopilot/.lake/build/lib/libctranslate.dylib ./. lake/packages/LeanCopilot/././ModelCheckpointManager/Url. lean -R ./. lake/packages/LeanCopilot/./.=9 ./-lake/packages/LeanCopiot/.lake/build/Ltb/ModeLCheckpointManager/UrL.olean =1 /lake/packages/LeanCop1Lot/.lake/build/Lib/ModelCheckpointManager/Url-ilean -c =./. lake/packages/LeanCopilot/.lake/build/lib/libleanffi.dylib

-c ./.lake/packages/LeanCopilot/.lake/bulld/ir/ModelCheckpointManager/Url.C —Load-dynlib=./.lake/packages/LeanCopilot/.lake/build.lib/libleanffi.dylib
error: stderr:

libc++abi.dylib: terminating with uncaught exception of type lean: exception: error loading library, dlopen./. lake/packages/LeanCopilot/.lake/build/lib/libleanffi-dylib, 9): Symbol not found: __ZTTNSt3__114basic_ifstreamIcNS_11char_traitsIcEEEE

Referenced from: ./. lake/packages/LeanCopilot/. lake/build/lib/libleanffi-dyLib

Expected in: flat namespace

in ./. Lake/packages/LeanCopilot/.lake/build/lib/Libleanffi-dylib
error: external command ' /Users/program/-elan/toolchains/Leanprover-lean4--V4.7.0-rcl/bin/lean' exited with code 134

[Jared green]

after having updated everything, i tried again, and im getting a 404.

[Mauricio Collares]

Please always post full error messages if possible! The message might include the bad URL, for example, which helps the LeanCopilot developers diagnose the problem.

[Mauricio Collares]

You can use #backticks to make them prettier

[Jared green]

sorry but actually i can't. on mac the zulip send button is missing.

[Jared green]

but the url is https://github.com/lean-dojo/LeanCopilot/releases/download/v1.3.3/x86_64-macOS.tar.gz

[Mauricio Collares]

Thanks for the info! Looks like they had macos x86_64 binaries back in v1.1.1, so having Apple Silicon-only releases might not be intentional.

[Jared green]

yes mine is all intel. by the way here is the error message.
$ lake exe LeanCopilot/download

✖ [1/17] Fetching LeanCopilot:optRelease

trace: downloading https://github.com/lean-dojo/LeanCopilot/releases/download/v1.3.3/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.3.3/x86_64-macOS.tar.gz

trace: stderr:

curl: (22) The requested URL returned error: 404

error: external command 'curl' exited with code 22

✖ [2/17] Fetching LeanCopilot:release

trace: downloading https://github.com/lean-dojo/LeanCopilot/releases/download/v1.3.3/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.3.3/x86_64-macOS.tar.gz

trace: stderr:

curl: (22) The requested URL returned error: 404

error: external command 'curl' exited with code 22

Some builds logged failures:

• LeanCopilot:optRelease
• LeanCopilot:release

error: build failed

[Jared green]

of course, v1.1.1 is the last one with a download for intel mac. unfortunately i cant just roll back now.

[Kim Morrison]

Jared green said:

sorry but actually i can't. on mac the zulip send button is missing.

Maybe you should start by dealing with that, then?