isabelle-dev.sketis.net and isabelle.sketis.net down for maintenance

Tobias Nipkow nipkow at in.tum.de
Thu Mar 27 14:39:50 CET 2025


Thank you for bringing all this up. This must also be the reason why some of our 
servers (AFP, ...)  are sometimes unreachable. I knew that it has to do with 
crawlers, but I was unaware of the global nature of the problem and that AI bots 
are causing it.

Tobias

On 27/03/2025 14:34, Makarius wrote:
> There have been a couple of private notes, hints, and recommendations. This is 
> my current understanding of possible approaches:
> 
>    (1) Block particular User-agent names from the other side, e.g. this list
> https://github.com/ai-robots-txt/ai.robots.txt/blob/main/robots.txt --- not via 
> robots.txt (which is often ignored), but hardwired into the Webserver.
> 
>    Weakness: AI bots often don't identify themselves properly.
> 
>    (2) Block particular address ranges, e.g. according to this list https:// 
> github.com/JasonLovesDoggo/caddy-defender/blob/main/ranges/data/generated.go
> 
>    Weakness: this is neither correct nor complete, i.e. legitimate users could 
> use a cloud address, bad addresses could be missing. Maybe it is better not to 
> block completely, but to reduce the bandwidth for such addresses.
> 
>    (3) Aggressive counterstrikes, e.g. via proof-of-work imposed on the other 
> side, e.g. see https://anubis.techaro.lol
> 
>    Weakness: answering war by more war is not a winning strategy.
> 
> 
>      Makarius
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5187 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20250327/5e2e699a/attachment.bin>


More information about the isabelle-dev mailing list