Lean 3.49 on Mac OS

Stream: general

[Oliver Nash]

Is anyone else having trouble upgrading to Lean 3.49 on Mac OS?

elan complains that:

error: binary package was not provided for 'darwin'

[Kevin Buzzard]

Is this the old error fixed by elan self update? What does elan -V give? Are you on >= 1.4.2 or below?

[Oliver Nash]

elan -V reports something quite embarrassing:

elan 1.0.8 (b41b00c6a 2021-09-10)

[Oliver Nash]

I'll try updating.

[Eric Rodriguez]

yeah this came up for me too, updating fixed the issue pretty fast

[Kevin Buzzard]

If elan self update doesn't work then uninstall and reinstall elan; this will hopefully fix it.

[Oliver Nash]

Now elan self update fails with an apparently known issue: https://github.com/leanprover/elan/issues/78

I'm losing the will.

[Oliver Nash]

OK maybe if I blow everything away. Thanks.

[Oliver Nash]

Oliver Nash said:

OK maybe if I blow everything away. Thanks.

This worked, specifically, all that was required was:

rm -rf ~/.elan
brew install elan-init

[Mauricio Collares]

@Sebastian Ullrich Is it worth using gnu tar for creating the Mac elan tarballs too?