Email Gateway (May 06 2025 at 14:37): Email Gateway (May 06 2025 at 14:37):From: Makarius <makarius@sketis.net>
Recently we have seen massive attacks by dumb AI bots again. After tinkering
with the webserver configuration for 1-2h, I did not manage to achieve
significant improvements.
As a consequence, I have now disabled the public access to
isabelle-dev.sketis.net --- it is for members only, who also need to be logged-in.
People who are directly involved in the isabelle-dev process and don't have an
account yet can email me privately.
Makarius
Email Gateway (May 07 2025 at 08:42):From: Makarius <makarius@sketis.net>
On 06/05/2025 16:36, Makarius wrote:
As a consequence, I have now disabled the public access to isabelle-
dev.sketis.net --- it is for members only, who also need to be logged-in.People who are directly involved in the isabelle-dev process and don't have an
account yet can email me privately.
A few more side-remarks:
* For public use, the main purpose of isabelle-dev.sketis.net are the
blogs, notably for release candidates. We are presently losing that.
* For development use, the main purpose of isabelle-dev.sketis.net is to
browse the history. I've also seen IntelliJ IDEA being used for that, or a
different high-end Mercurial client. One happy day that functionality will
become part of the regular Prover IDE.
* To access particular Isabelle versions (e.g. for automated clones) it is
better to use a regular hgweb service. The traditional one is
https://isabelle.in.tum.de/repos/isabelle but that has seen various technical
problems recently. I am now more often using the clone
https://isabelle.sketis.net/repos/isabelle
Hgweb does not suffer much from bad AI bots: the performance for Python + Rust
(hg) is better than PHP + MySQL (Phorge). It is still a waste of energy, and
the planet would be in better shape without all this AI non-sense.
Makarius
Last updated: May 31 2025 at 01:44 UTC