4
$\begingroup$

after taking a break of half a year I would like to get back to proving things in Lean. I followed the instructions to install a fresh lean project. When I do

winpty leanproject new fresh_project

in git bash, it starts creating the git repository andconfiguring, but then I get the error:

Adding mathlib
info: downloading component 'lean'
error: binary package was not provided for 'windows'
Command '['leanpkg', 'add', 'leanprover-community/mathlib']' returned non-zero e
xit status 1.

Does anyone know what I can do to get it running again?

Remark: winpty is just a workaround to get python running in the windows vresion of the git bash-command line, which I have used before.

$\endgroup$

1 Answer 1

7
$\begingroup$

You need to update elan because of upstream changes at github. Try elan self update. If this doesn't work then reinstall elan. If you search for your error on the lean Zulip you'll find lots more information about this (but hopefully you won't need it).

$\endgroup$
1
  • $\begingroup$ 'elan self update' worked. Thanks! $\endgroup$ Jan 8, 2023 at 0:03

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.