i still cannot download on intel mac

[jaredgreen2]

i still get a 404
$ lake exe LeanCopilot/download
✖ [3/20] (Optional) Fetching LeanCopilot:optRelease
trace: downloading https://github.com/lean-dojo/LeanCopilot/releases/download/v1.5.1/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.5.1/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

[Peiyang-Song]

I see, thanks for the report. Seems like it is somehow still trying to get the download from a prebuilt release. Did all the steps before lake exe LeanCopilot/download succeed? Specifically did the lake build complete without errors? If it's just the downloading step that triggers a 404, you may download the models manually.

[jaredgreen2]

yes everything before succeeded. could you put up instructions on how to do the download manually? and what to do afterwards?

[Peiyang-Song]

Thanks, that's great to know. Sure -- let me put this guide of manually downloading models into README and also post it here after I'm done.

[Peiyang-Song]

In PR #118 instructions are added for manually downloading models from Hugging Face, into the README. The Hugging Face URLs for the four models are at

"https://huggingface.co/kaiyuy/ct2-leandojo-lean4-tacgen-byt5-small"
"https://huggingface.co/kaiyuy/ct2-leandojo-lean4-retriever-byt5-small"
"https://huggingface.co/kaiyuy/premise-embeddings-leandojo-lean4-retriever-byt5-small"
"https://huggingface.co/kaiyuy/ct2-byt5-small"

You can download them directly and put them into ~/.cache/lean_copilot/. All other steps before and after stay the same.

[jaredgreen2]

do i just download model.bin, or the entirety of each repository?

[Peiyang-Song]

The entire repo, you can directly git clone.

[jaredgreen2]

also, what is the full path to that folder, starting at <project_name>

[Peiyang-Song]

Which folder? The repos are directly at the URLs.

[jaredgreen2]

~/.cache/lean_copilot/

[Peiyang-Song]

This is already the path to the folder. I cannot tell what the exact full path is on your machine, because that depends on what your home directory is. Is this what you are asking?

[jaredgreen2]

it doesnt appear to exist.

[jaredgreen2]

~/.cache/mathlib is the only folder present in .cache

[Peiyang-Song]

Right, if you have not ever downloaded these models before, that folder should not have existed by now. You can create it.

[jaredgreen2]

and the command for that is

[Peiyang-Song]

You mean how to create a folder on your desktop?

[Peiyang-Song]

You can get into the parent directory and create a new folder, or if you prefer the command line you can mkdir.

[jaredgreen2]

and then for the cloning

[jaredgreen2]

is the cloning supposed to finish in seconds?

[jaredgreen2]

i get an error message:
$ lake build
✖ [9/491] (Optional) Fetching auto:optRelease
error: no release tag found for revision 'bfb20f93b4e67029b977f218c67d8ca87ca09c9a'
⚠ [10/491] Ran auto:extraDep
warning: building from source; failed to fetch cloud release (see 'auto:optRelease' for details)
✖ [12/491] (Optional) Fetching LeanCopilot:optRelease
trace: downloading https://github.com/lean-dojo/LeanCopilot/releases/download/v1.5.1/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.5.1/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

[Peiyang-Song]

You can just git clone, and it will likely not finish in several seconds, but definitely no more than a few minutes.

[jaredgreen2]

i got this for the first cloning:
$ git clone https://huggingface.co/kaiyuy/ct2-leandojo-lean4-tacgen-byt5-small
Cloning into 'ct2-leandojo-lean4-tacgen-byt5-small'...
remote: Enumerating objects: 19, done.
remote: Counting objects: 100% (19/19), done.
remote: Compressing objects: 100% (17/17), done.
remote: Total 19 (delta 4), reused 10 (delta 1), pack-reused 0 (from 0)
Unpacking objects: 100% (19/19), done.
git-lfs filter-process: git-lfs: command not found
fatal: the remote end hung up unexpectedly
warning: Clone succeeded, but checkout failed.
You can inspect what was checked out with 'git status'
and retry with 'git restore --source=HEAD :/'

[Peiyang-Song]

Did you run the lake build first or did you clone first? Just to be clear: are you working on Lean Copilot itself or are you trying to use it in an external project?

[jaredgreen2]

im trying to use it in a project. i cloned first.

[Peiyang-Song]

Okay. For the error you are seeing when you clone, it seems to me that you don't have git-lfs available. Have you satisfied the requirements in the readme before you start the setup steps?

[jaredgreen2]

i have now installed git-lfs. and cloned successfully. i still get
$ lake build
✖ [9/491] (Optional) Fetching auto:optRelease
error: no release tag found for revision 'bfb20f93b4e67029b977f218c67d8ca87ca09c9a'
⚠ [10/491] Ran auto:extraDep
warning: building from source; failed to fetch cloud release (see 'auto:optRelease' for details)
✖ [12/491] (Optional) Fetching LeanCopilot:optRelease
trace: downloading https://github.com/lean-dojo/LeanCopilot/releases/download/v1.5.1/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.5.1/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

[Peiyang-Song]

Thanks, I thought we said it's just the downloading step that did not work. Anyways, did the lake build succeed before or did it never?

[Peiyang-Song]

If the lake build actually never succeeded, it looks like the error message is still related to cloud release. Although I don't have a x86_64 Mac personally, we had a contributor successfully testing out Lean Copilot on one recently. I will reach out to him and try to reproduce.

[idontgetoutmuch]

I too have this problem. I will try the manual instructions you have given.

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)

[idontgetoutmuch]

The entire repo, you can directly git clone.

Which repo? I am looking here: https://huggingface.co/kaiyuy but

git clone https://huggingface.co/kaiyuy
Cloning into 'kaiyuy'...
Username for 'https://huggingface.co': 

I don't have a username for huggingface. But maybe you meant something different?

[idontgetoutmuch]

The problem is lean detects the wrong OS

def getArch? : IO (Option SupportedArch) := do
  let out ← IO.Process.output {cmd := "uname", args := #["-m"], stdin := .null}
  let arch := out.stdout.trim
  IO.println s!"Detected architecture: {arch}"
  if arch ∈ ["arm64", "aarch64"] then
    return some .arm64
  else if arch == "x86_64" then
    return some .x86_64
  else
    return none

dom@Wandle mathematics_in_lean % lake build
warning: LeanCopilot: repository '././.lake/packages/LeanCopilot' has local changes
info: Detected architecture: x86_64

dom@Wandle mathematics_in_lean % uname -m
arm64

lol

[idontgetoutmuch]

The answer is to install the correct version of elan (arm64): https://github.com/leanprover/elan/releases/download/v3.1.1/elan-aarch64-apple-darwin.tar.gz. @jaredgreen2 I think all the other things are red herrings.

[jaredgreen2]

and what do i do after downloading?

[idontgetoutmuch]

and what do i do after downloading?

I think you unzip it and run the installer. I assume you did uname -m to check your architecture.

[jaredgreen2]

$ uname -m
x86_64

[lakesare]

Stumbling upon the same issue when trying to use v1.6.0:

❯ lake update LeanCopilot                                                                               carleson/git/lakesare/scales_impacting_interval !
No files to download
Decompressing 5149 file(s)
Unpacked in 425 ms
Completed successfully!
info: LeanCopilot: cloning https://github.com/lean-dojo/LeanCopilot.git to '././.lake/packages/LeanCopilot'
info: mathlib: running post-update hooks
❯ lake exe LeanCopilot/download                                                                         carleson/git/lakesare/scales_impacting_interval !
✖ [3/20] (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
❯ uname -m                                                                                                                                            carleson/git/lakesare/scales_impacting_interval !
x86_64