0
$\begingroup$

I have just started learning Lean 4 using Mathematics in Lean in Visual Studio Code, and I ran into a problem right away. I get the following error message:

    `c:\Users\User\.elan\toolchains\leanprover--lean4---v4.5.0-rc1\bin\lake.exe setup-file C:/Users/User/Documents/Coding/mathematics_in_lean/my_files/C01_Introduction/S02_Overview.lean Init Mathlib.Data.Nat.Basic Mathlib.Data.Nat.Parity MIL.Common` failed:

stderr:
info: [186/255] Downloading proofwidgets cloud release
error: > curl -s -f -o .\.lake/packages\proofwidgets\.lake\windows-64.tar.gz -L https://github.com/leanprover-community/ProofWidgets4/releases/download/v0.0.24/windows-64.tar.gz
error: external command `curl` exited with code 35
info: [341/661] Building ProofWidgets.Component.Basic
error: > LEAN_PATH=.\.lake/packages\std\.lake\build\lib;.\.lake/packages\Qq\.lake\build\lib;.\.lake/packages\aesop\.lake\build\lib;.\.lake/packages\proofwidgets\.lake\build\lib;.\.lake/packages\Cli\.lake\build\lib;.\.lake/packages\mathlib\.lake\build\lib;.\.lake\build\lib PATH c:\Users\User\.elan\toolchains\leanprover--lean4---v4.5.0-rc1\bin\lean.exe .\.lake/packages\proofwidgets\.\.\ProofWidgets\Component\Basic.lean -R .\.lake/packages\proofwidgets\.\. -o .\.lake/packages\proofwidgets\.lake\build\lib\ProofWidgets\Component\Basic.olean -i .\.lake/packages\proofwidgets\.lake\build\lib\ProofWidgets\Component\Basic.ilean -c .\.lake/packages\proofwidgets\.lake\build\ir\ProofWidgets\Component\Basic.c
error: stdout:
.\.lake/packages\proofwidgets\.\.\ProofWidgets\Component\Basic.lean:75:16: error: no such file or directory (error code: 2)
  file: .\.lake/packages\proofwidgets\.\.\ProofWidgets\Component\..\..\.lake\build\js\interactiveExpr.js
.\.lake/packages\proofwidgets\.\.\ProofWidgets\Component\Basic.lean:73:2: error: cannot evaluate code because 'ProofWidgets.InteractiveExpr' uses 'sorry' and/or contains errors
error: external command `c:\Users\User\.elan\toolchains\leanprover--lean4---v4.5.0-rc1\bin\lean.exe` exited with code 1

The program stops processing after the very first line, it seems as if there is something wrong with all the "import"s. I followed all the instructions during installation, does anyone know what the problem could be?

enter image description here

$\endgroup$

1 Answer 1

0
$\begingroup$

It is not the imports, the computer told you:

error: external command `curl` exited with code 35

If you look up exit code 35 for curl it says "A TLS/SSL connect error". So this does not look like it's related to Lean directly. Unfortunately there are many reasons why it might be failing, ranging from "temporarily something's wrong with the remote server" to "an (incompetent) foreign agency is spying on you".

The command works for me at the moment, so I'd lean towards "temporarily something was wrong". Are you behind an overzealous firewall by any chance?

$\endgroup$

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.