Error importing mathlib

Stream: general

[Jared green]

When trying to create a project with mathlib I get an error.
image.jpeg
The first time I tried it, the avast antivirus stopped it, now I can’t do anything about it. It’s not even my laptop.

[Mauricio Collares]

Try following the instructions at https://support.avast.com/en-us/article/use-antivirus-https-scan/ to disable HTTPS scanning

[Jared green]

And if avast isn’t responsible? I’m not even sure if it is.

[Jared green]

Update: that did it.

[Marc Huisinga]

Is there other antivirus software that is known to cause issues with Lean? We should add a hint about disabling them to the VS Code setup guide.

[Jared green]

Not to my knowledge.

[Kevin Buzzard]

FWIW someone at Xena had a problem installing two weeks ago and it turned out to be Avast. Maybe someone from the lean community can approach Avast and flag this as an issue?

[Julian Berman]

The place to do so appears to be here: https://www.avast.com/en-us/false-positive-file-form.php

[Julian Berman]

(I'm not familiar with 2024-in-antivirii but if we really want to be spicy, casual browsing seems to suggest Windows users discouraging using Avast entirely, so the tutorial could recommend you switch to some other one entirely if that's actually the case.)

[Mauricio Collares]

Marc Huisinga said:

Is there other antivirus software that is known to cause issues with Lean? We should add a hint about disabling them to the VS Code setup guide.

There have been reports of Kaspersky and AVG also causing problems at Lean for the Curious Mathematician 2023: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/lake.20exe.20cache.20get.20errors/near/388979416

[Mauricio Collares]

Antiviruses seem to like to MitM every HTTPS connection by default, and curl really doesn't like it

[Mauricio Collares]

Unfortunately this is by design. To scan HTTPS traffic, the antivirus must necessarily weaken security by doing a man-in-the-middle "attack". It's not a false positive because the antivirus is not detecting anything, curl is the one (rightfully) complaining about bad certificates.

[Marc Huisinga]

Thanks!