brew elan missing nightly

Stream: lean4

[Mac]

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]

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

[Mac]

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]

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

[Mauricio Collares]

Huh, we're getting rate limited

[Mauricio Collares]

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]

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]

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