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