leantar install issues

Stream: mathlib4

[Tiago]

I have been attempting to set up a Mathlib project, however when I run lake update, in the post-update hooks, it attempts to install leantar but fails with the error message below:

"""
info: toolchain not updated; already up-to-date
info: mathlib: running post-update hooks
PANIC at String.Slice.toNat! Init.Data.String.Slice:1272:4: Nat expected
installing leantar 0.1.16
uncaught exception: failure in curl #[https://github.com/digama0/leangz/releases/download/v0.1.16/leantar-v0.1.16-x86_64-pc-windows-msvc.zip, -L, -o, C:\Users\tibai\.cache\mathlib\leantar-0.1.16.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
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.

error: mathlib: failed to fetch cache
"""

I have attempted multiple things like installing leantar manually and putting it within the cache as well as the .elan/bin directory but those don't seem to work. I have also disabled any sort of external antivirus processes that could have been impacting it. I am not sure if this is something that has happened before but I have tried so many different ways to attempt to resolve this and nothing seems to work.

Thank you if anyone can help, this is my first time posting or using this website, so I hope I have set this message up correctly and in the right place (was recommended to post here by my lecturer)

[Anne Baanen]

It looks like your download never got started because of certificate issues, which usually means you have an antivirus or firewall blocking you from accessing GitHub. You say that antivirus is disabled, are you using a proxy/VPN/firewall?

[Tiago]

I do not use a VPN or proxy, and below are the exclusions I set for the antivirus and website threat scanning:

image.png
image.png

I use Norton360 as my antivirus and am not sure if there is an easier/better way to know whether the problem could be coming from it, as I believe I have switched everything off that could be impacting it but everything I have seen online seems to point to this being the source.

I was working with ChatGPT to help debug the source of the problem and we got to a stage where it wanted me to run the following commands in the created mathlib directory: "where lean", "where lake", "where leantar"; but after doing these, nothing is printed in the terminal, meaning it cannot locate their file locations. ChatGPT seems to think this is the issue and I tried adding the file locations to path as well as some other things it recommended but nothing worked.

I have used Lean before, without mathlib, and the lean worked perfectly fine, so not sure why the path location cant be found, and I'm not even sure if this has anything to do with the original error I was getting.

[Kevin Buzzard]

I would temporarily completely disable your antivirus and see if this solves the problem. I have seen examples where no amount of guessing the right directories works, and you just have to switch it off for a bit.

[Tiago]

I completely disabled my Nortons antivirus and web protection for 10 mins and it worked, cant believe it was that easy the whole time, and very annoying that the antivirus does that.

Will this be something I will have to disable whenever "lake update" is used from now on, or should it be okay now that leantar has been downloaded after running once?

Thank you for the help, despite it being an easy fix, I was starting to lose my mind over this!

[Snir Broshi]

Tiago said:

very annoying that the antivirus does that

OTOH it's really great that antiviruses are capable of checking every file right at the moment it lands on your disk
btw if you're on Windows there's no reason to use anything other than the built-in antivirus (Windows Defender), it's very integrated to the OS and does great things already