Problem with lake/proofwidgets

Stream: lean4

[Bastiaan Cnossen]

I've installed Lean4 earlier today and was trying to do the tutorial "Introduction to Lean". However, already at the very first file S02_Overview.lean things are not working properly for me. Instead of seeing the expected Lean proof state, I get a notification that I need to "restart the file", and after doing so I'm getting the following list of errors:

`c:\Users\LocalAdmin\.elan\toolchains\leanprover--lean4---v4.21.0\bin\lake.exe setup-file C:/Users/LocalAdmin/Documents/Lean/Introduction to Lean/MIL/C01_Introduction/S02_Overview.lean Init MIL.Common` failed:
stderr:
⚠ [571/724] Ran proofwidgets:extraDep
warning: building from source; failed to fetch GitHub release (run with '-v' for details)
✖ [572/724] Building proofwidgets/widgetJsAll
error: ProofWidgets not up-to-date. Please run `lake exe cache get` to fetch the latest ProofWidgets. If this does not work, report your issue on the Lean Zulip.
Some required builds logged failures:
- proofwidgets/widgetJsAll
error: build failed

I tried to run lake exe cache get, as suggested, but this did not work:

PS C:\Users\LocalAdmin\Documents\Lean\Mathlib> lake exe cache get
installing leantar 0.1.15
uncaught exception: failure in curl #[https://github.com/digama0/leangz/releases/download/v0.1.15/leantar-v0.1.15-x86_64-pc-windows-msvc.zip, -L, -o, C:\Users\LocalAdmin\.cache\mathlib\leantar-0.1.15.exe.zip]:
  % Total    % Received % Xferd  Average Speed   Time    Time     Time  Current
                                 Dload  Upload   Total   Spent    Left  Speed
  0     0    0     0    0     0      0      0 --:--:-- --:--:-- --:--:--     0
curl: (35) schannel: next InitializeSecurityContext failed: CRYPT_E_NO_REVOCATION_CHECK (0x80092012) - The revocation function was unable to check revocation for the certificate.

Unfortunately I'm not very good with computers, so I have no clue what I am supposed to do. I looked around online, to no avail. I asked ChatGPT, tried fixing this for about 1.5 hours, to no avail. I asked Cursor to solve it for me, which was somewhat helpful since it confirmed that Lean was working properly (it created a test-file for me in which I did get to see Lean's proof state), but in the end it still wasn't able to let me do this tutorial.

Does anyone know what I need to do to fix this? Thanks a lot in advance!

[Dagur Asgeirsson]

I have no idea if this will work, but you could try to remove .lake by running rm -rf .lake and then running lake exe cache get again

[Bastiaan Cnossen]

Where precisely am I supposed to run this? (Remember: I'm a noob.) If I try to run this in the directory where lakefile.lean is stored, I get:

Remove-Item : A parameter cannot be found that matches parameter name 'rf'.
At line:1 char:4
+ rm -rf .lake
+    ~~~
    + CategoryInfo          : InvalidArgument: (:) [Remove-Item], ParameterBindingException
    + FullyQualifiedErrorId : NamedParameterNotFound,Microsoft.PowerShell.Commands.RemoveItemCommand

[Dagur Asgeirsson]

Oh, I'm not sure how to do this on Windows, but what your trying to do is delete the folder .lake and all its contents, which lives inside your lean project

[Sebastian Ullrich]

Try disabling your antivirus for running cache get: https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/curl.20error.20CRYPT_E_NO_REVOCATION_CHECK.20.280x80092012.29/with/542503759