[isabelle-dev] Sunsetting Mercurial support in Bitbucket

[Makarius]

On 23/08/2019 13:29, Lawrence Paulson wrote:
> You are confident but I am not so sure. The longer we cling on, the more painful the eventual transition will be for all of us. This is not to criticise your original choice all those years ago.

When you say "cling", you implicitly agree with the Git worldview, but
that is not necessary. The non-Git world pretty much alive, and
populated by smart people who know how to resist social pressure.
(Occasionally such people also come to me and tell me personally.)


> What are the objective reasons for us to stick with Mercurial? What are its real benefits over Git?

Mercurial emphasizes purity, simplicity and monotonicity. Moreover, it
is more "serving" than "ruling", i.e. a tool that stays in the
background and does not cause much attention.
All of this fits nicely with the overall Isabelle philosophy.

At the bottom, the technology of Mercurial and Git is not fundamentally
different. It is just a matter how that is used in practice, and Git
culture is particularly bad in that respect: huge centralized services,
coolness, noise, people who don't know how to produce clean history etc.


We are implicitly talking about two repositories here:

  (1) Isabelle
  (2) AFP

Isabelle is the underlying technology for AFP, see also my recent paper
https://arxiv.org/abs/1905.07244

Isabelle/Scala already contains a few administrative operations both for
Isabelle and AFP -- both being Mercurial simplifies things. More of that
should be coming eventually, also more integration of it into the Prover
IDE.

Isabelle is a complex software product with some theory libraries --
this means good version control with clean history is vital. Mercurial
does a pretty good job at that -- I am not worried about the next 5 years.

In contrast, AFP is mostly a formal mathematical library, i.e. the
target audience are not software developers but mathematicians (at least
that is our claim and eventual target). Authors of formal mathematics
are not software developers, and should not be burdened with platforms
for "social coding" (former slogan of Github).

Instead we as prover communities need eventually come up with something
more fitting for authoring mathematics in a collaborative environment --
this is a matter of future research and development. Standard services
for SCM ("Source Code Management") will not do that in the long run,
although such a technology might be at the bottom of such infrastructure.


In the short term, the task is more simple: to find a new canonical
hosting platform for Mercurial, and maybe use the opportunity to purify
and simplify the overall setup.

It would be great if this is not a reason for divorcing Isabelle from
AFP at the bottom of SCM technology. Such a split would mean that I had
to spend more resources to work around it -- resources that are better
invested elsewhere.


	Makarius