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.

Improve this question
$\endgroup$

1 Answer 1

Reset to default
6
$\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).

Improve this answer
$\endgroup$
1
  • $\begingroup$ 'elan self update' worked. Thanks! $\endgroup$
    – Strichcoder
    Jan 8 at 0:03

Your Answer

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

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