Email Gateway (May 19 2025 at 13:51): Email Gateway (May 19 2025 at 13:51):From: Paolo Crisafulli <cl-isabelle-users@lists.cam.ac.uk>
Hi,
I used to watch the Isabelle ongoing development blog, for announcements
such as:
https://isabelle-dev.sketis.net/home/menu/view/20/
I see that now access is restricted.
Should I ask for an account, or are there other means to get this kind
of information?
Thank you in advance.
Best,
Paolo Crisafulli
Email Gateway (May 22 2025 at 12:35):From: Makarius <makarius@sketis.net>
On 19/05/2025 15:50, Paolo Crisafulli (via cl-isabelle-users Mailing List) wrote:
I used to watch the Isabelle ongoing development blog, for announcements such as:
https://isabelle-dev.sketis.net/home/menu/view/20/
I see that now access is restricted.
That is a sad consequence of evil AI bots attacking public servers. The
ancient agreement on "robots.txt" has little value today. That is the end of
fundamental conventions of the public Internet.
In the past 12 months or so, I have managed a few times to make the underlying
Caddy web server more robust in various respects. It has worked occasionally,
but recent AI attacks have become more fierce. So the current measure is to
run https://isabelle-dev.sketis.net private member-only website --- suddenly
everything becomes light-weight and efficient.
Note that public Isabelle repository access still works, with the canonical
clones at:
https://isabelle.in.tum.de/repos/isabelle
https://isabelle.sketis.net/repos/isabelle
Both are based on plain hgweb, which is a combination of Apache/Python + Rust,
instead of Apache/PHP + MySQL for Phabricator/Phorge. Thus it performs better
under heavy attack of AI bots, but it still wastes a lot of energy, like most
other AI activity we see today.
It is high time to stop this global AI insanity ...
Makarius
Email Gateway (May 22 2025 at 13:17):From: Jan van Brügge <jan@vanbruegge.de>
Apparently Anubis helps against these crawlers: https://anubis.techaro.lol/
22.05.2025 14:35:34 Makarius <makarius@sketis.net>:
On 19/05/2025 15:50, Paolo Crisafulli (via cl-isabelle-users Mailing List) wrote:
I used to watch the Isabelle ongoing development blog, for announcements such as:
https://isabelle-dev.sketis.net/home/menu/view/20/
I see that now access is restricted.That is a sad consequence of evil AI bots attacking public servers. The ancient agreement on "robots.txt" has little value today. That is the end of fundamental conventions of the public Internet.
In the past 12 months or so, I have managed a few times to make the underlying Caddy web server more robust in various respects. It has worked occasionally, but recent AI attacks have become more fierce. So the current measure is to run https://isabelle-dev.sketis.net private member-only website --- suddenly everything becomes light-weight and efficient.
Note that public Isabelle repository access still works, with the canonical clones at:
https://isabelle.in.tum.de/repos/isabelle
https://isabelle.sketis.net/repos/isabelleBoth are based on plain hgweb, which is a combination of Apache/Python + Rust, instead of Apache/PHP + MySQL for Phabricator/Phorge. Thus it performs better under heavy attack of AI bots, but it still wastes a lot of energy, like most other AI activity we see today.
It is high time to stop this global AI insanity ...
Makarius
Email Gateway (May 22 2025 at 13:23):From: Makarius <makarius@sketis.net>
On 22/05/2025 15:11, Jan van Brügge wrote:
Apparently Anubis helps against these crawlers: https://anubis.techaro.lol
I've seen this already, but was reluctant to apply this "nuclear counter
strike", as someone has called it in a blog.
I need to revisit the situation soon, and figure out a way to solve problems
without escalating aggression.
Makarius
Email Gateway (May 22 2025 at 13:52):From: "\"Lammich, Peter (UT-EEMCS)\"" <cl-isabelle-users@lists.cam.ac.uk>
I've also seen an increase in "are you a human" checks recently. Stack overflow, Ubuntu, etc seems to use them now.
Peter
On 22 May 2025 15:23, Makarius <makarius@sketis.net> wrote:
On 22/05/2025 15:11, Jan van Brügge wrote:
Apparently Anubis helps against these crawlers: https://anubis.techaro.lol
I've seen this already, but was reluctant to apply this "nuclear counter
strike", as someone has called it in a blog.
I need to revisit the situation soon, and figure out a way to solve problems
without escalating aggression.
Makarius
Email Gateway (May 22 2025 at 14:03):From: Makarius <makarius@sketis.net>
On 22/05/2025 15:52, Lammich, Peter (UT-EEMCS) wrote:
I've also seen an increase in "are you a human" checks recently. Stack
overflow, Ubuntu, etc seems to use them now.
That was the start of the end of the free Internet, already some years ago.
Note that I do have my own tools to "harvest websites" under program control,
and I don't want to dilute this plain and basic idea with strange add-ons.
Makarius
Last updated: May 30 2025 at 04:27 UTC