Zulip Chat Archive

Stream: new members

Topic: error: binary package was not provided

Vasily Ilin (Dec 01 2022 at 01:45):

I am having trouble with leanproject. Does anyone know how to fix this?

C:\Users\Math User\Github
λ leanproject new LLL
> cd LLL
> git init -q
> git checkout -b lean-3.42.1
Switched to a new branch 'lean-3.42.1'
configuring LLL 0.1
Adding mathlib
info: downloading component 'lean'
error: binary package was not provided for 'windows'
Command '['leanpkg', 'add', 'leanprover-community/mathlib']' returned non-zero exit status 1.

Alex J. Best (Dec 01 2022 at 01:49):

Try elan self update

Bjørn Kjos-Hanssen (Dec 01 2022 at 04:05):

I have the same problem... elan self update gave this response:

info: checking for self-updates
error: failed to parse latest release tag

Kevin Buzzard (Dec 01 2022 at 04:06):

If that doesn't work then uninstall and reinstall elan following the installation instructions on the community website

Vasily Ilin (Dec 01 2022 at 06:07):

Thank you all! elan self update did the trick for me. Some other people are getting errors. I'll ask for more help if needed!

Last updated: Dec 20 2023 at 11:08 UTC