binary package was not provided for 'windows'

Stream: new members

[Andre Hernandez-Espiet (Rutgers)]

I tried to get a fresh branch of mathlib using leanproject get -b mathlib:blah and got the following error: binary package was not provided for 'windows'. What should I do?

[Mauricio Collares]

Run elan self update, it was recently fixed

[Andre Hernandez-Espiet (Rutgers)]

I tried that, and then I get the error could not remove 'elan-bin' file: 'C:\Users\André\.elan\bin\elan.exe' info: caused by: Access is denied. (os error 5)

[Martin Dvořák]

After I pulled master from mathlib, typing leanproject build gave me:

Building project mathlib
info: downloading component 'lean'
error: binary package was not provided for 'windows'
Command '['leanpkg', 'build']' returned non-zero exit status 1.

The same error happens when I try to open the infoview in VSC. The same thing happens after I do leanproject get -b matlib:my_branch instead of pulling master.

[Alex J. Best]

Did you try elan self update

[Martin Dvořák]

$ elan self update
info: checking for self-updates
info: downloading self-update
Error(Download(HttpStatus(404)), State { next_error: None, backtrace: InternalBacktrace { backtrace: None } })
error: could not download file from 'https://github.com/leanprover/elan/releases/download/v1.4.2/elan-.zip' to 'C:\Users\dvora\AppData\Local\Temp\elan-update.mEJT7DsgmYiX\elan-.zip'
info: caused by: http request returned an unsuccessful status code: 404

[Alex J. Best]

Try reinstalling elan with elan self uninstall then install following https://github.com/leanprover/elan

[Martin Dvořák]

Uninstall done. Then:

$ curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
curl: (60) SSL certificate problem: unable to get local issuer certificate
More details here: https://curl.haxx.se/docs/sslcerts.html

curl failed to verify the legitimacy of the server and therefore could not
establish a secure connection to it. To learn more about this situation and
how to fix it, please visit the web page mentioned above.

Is it a problem in my computer?

[Alex J. Best]

yeah if curl isn't working that seems to be a deeper issue

[Alex J. Best]

You can simply download https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh and run the script by hand though

[Martin Dvořák]

It doesn't seem to help.

$ ./elan-init.sh
info: downloading installer
curl: (60) SSL certificate problem: unable to get local issuer certificate
More details here: https://curl.haxx.se/docs/sslcerts.html

curl failed to verify the legitimacy of the server and therefore could not
establish a secure connection to it. To learn more about this situation and
how to fix it, please visit the web page mentioned above.
elan: command failed: curl -sSfL https://github.com/leanprover/elan/releases/download/v1.4.2/elan-x86_64-pc-windows-msvc.zip -o /tmp/tmp.dSsqltC2XR/elan-init.zip

Is the problem on my side?

[Alex J. Best]

Yes the install script works fine for me

[Martin Dvořák]

I uninstalled Git for Windows (all parts) and installed it again. However, when I run elan-init.sh in Git Bash, curl keeps giving me the same error as before.

I suppose this is not a question for Leanprover Zulipchat. Where do you think I should ask for help instead?

[Martin Dvořák]

When I install Lean without Elan, VSC gives me:

Unable to start the Lean server process: Error: spawn lean ENOENT --- The lean.executablePath "lean" may be incorrect, make sure it is a valid Lean executable

[Martin Dvořák]

I guess that having leanproject without having lean is good for nothing.

$ which leanproject
/c/Users/dvora/AppData/Local/Programs/Python/Python36/Scripts/leanproject

$ which lean
which: no lean in (...)

$ which elan
which: no elan in (...)

Is there a way to install Lean 3 on Windows manually without SSL and curl? Possibly avoiding elan?

[Alex J. Best]

I would say that you are best off trying to fix elan or whatever is wrong with your curl / ssl setup. Maybe there is some stack exchange site for this. Did you read the url the errors link to?

[Martin Dvořák]

In the end, I disabled SSL certificate validating by:
echo insecure >> $HOME/.curlrc

[Martin Dvořák]

Elan now installed successfully. Should I be worried about security of my computer now?

[Alex J. Best]

Probably its best to remove that line from curlrc and just add it back whenever elan complains again yes

[Martin Dvořák]

Line removed. The file $HOME/.curlrc is now completely empty (except for LF). Is it safe?