After more AI bot attacks: isabelle-dev.sketis.net is now for members only

[Makarius]

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