Zulip Chat Archive

Stream: lean4

Topic: brew elan missing nightly


Mac (Sep 20 2022 at 22:58):

The elan distributed via homebrew cannot seem to find the lean binary package for nightly 09-20. From, the logs of the Lake CI (where I encountered this problem), the error message is:

info: downloading component 'lean'
error: binary package was not provided for 'darwin'

Mauricio Collares (Sep 20 2022 at 23:03):

This was fixed in elan 1.4.2, which should be available via brew according to https://formulae.brew.sh/formula/elan-init

Mac (Sep 20 2022 at 23:06):

Looking again at the logs of the Lake CI, it seems that brew is still stuck on elan 1.4.1:

==> Summary
🍺  /usr/local/Cellar/elan-init/1.4.1: 20 files, 5MB

Mauricio Collares (Sep 20 2022 at 23:11):

Maybe adding a brew update step helps? https://github.com/leanprover/lake/pull/124 needs approval to test it on CI

Mauricio Collares (Sep 20 2022 at 23:26):

Huh, we're getting rate limited

Mauricio Collares (Sep 20 2022 at 23:30):

I guess brew update won't be needed once https://github.com/actions/runner-images/pull/6268 lands, though, so I don't know what's the best solution

Mauricio Collares (Sep 20 2022 at 23:30):

You can switch from macOS-latest to macOS-12, which has a newer image already available, but I don't know if that breaks compatibility somehow

Sebastian Ullrich (Sep 21 2022 at 08:38):

Let's keep it simple: https://github.com/leanprover/lake/pull/125


Last updated: Dec 20 2023 at 11:08 UTC