[Merged by Bors] - chore: download recent curl if necessary on x64 Linux #3097
Conversation
Kha
commented
Mar 25, 2023
Kha
commented
Cache/IO.lean
Outdated
| -- NOTE: we host only one version of curl, which we assume to be at least as recent | ||
| -- as the version encoded in `CURLBIN` | ||
| let _ ← runCmd "curl" #[ | ||
| "https://pp.ipd.kit.edu/~ullrich/tmp/curl-x86_64-linux-static", "-o", CURLBIN.toString] |
There was a problem hiding this comment.
Obviously this should be hosted somewhere else, could someone move it to the Azure cache?
There was a problem hiding this comment.
Should we go with the time-honored tradition of abusing github releases for this? I can make a leanprover-community/static-curl repo and give you access if you want.
There was a problem hiding this comment.
Sounds fine too, whatever is simpler I would say
There was a problem hiding this comment.
Done, and added aarch64 for good measure
Kha
force-pushed
the
curl-static
branch
2 times, most recently
from
4e86178
to
4d3eefe
Compare
| def CURLVERSION := | ||
| "7.88.1" |
There was a problem hiding this comment.
Why are we screaming again?
|
By the way, I'm surprised we haven't hit leanprover/elan@342a0ca yet |
|
No, they only remove |
|
Right, bad memory 🤦🏼 |
|
bors r+ |
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
