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 _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
