Zulip Chat Archive

Stream: lean4

Topic: Adding a dependency without a prebuilt release


Adarsh Kumarappan (May 09 2024 at 19:48):

Hi everyone! I am using Lean4 for a new project that requires adding a GitHub repo as a dependency. I have used a require statement for this in my lakefile.lean, but when I run lake build --verbose, I get one of the following exceptions:

error: LeanCopilot: wanted prebuilt release, but could not find an associated tag for the package's revision
or

[1/4] Downloading LeanCopilot cloud release
Downloading LeanCopilot/v1.2.0/arm64-macOS.tar.gz
error: > curl -f -o ./.lake/packages/LeanCopilot/.lake/arm64-macOS.tar.gz -L https://github.com/Adarsh321123/AdarshLeanCopilot/releases/download/v1.2.0/arm64-macOS.tar.gz
error: stderr:
  % Total    % Received % Xferd  Average Speed   Time    Time     Time  Current
                                 Dload  Upload   Total   Spent    Left  Speed
  0     0    0     0    0     0      0      0 --:--:-- --:--:-- --:--:--     0
curl: (22) The requested URL returned error: 404
error: external command `curl` exited with code 22
warning: fetching cloud release failed; falling back to local build

This issue occurs even with preferReleaseBuild := false under the package block in lakefile.lean. I want lake to build the package locally instead of retrieving a nonexistent prebuilt release, but I couldn't figure how to do this using online materials. Can someone please guide me in the right direction?


Last updated: May 02 2025 at 03:31 UTC