[isabelle-dev] Sunsetting Mercurial support in Bitbucket

[Makarius]

On 23/08/2019 17:48, Lars Hupel wrote:
>> The reason why I have been so explicit about it this time: I've been
>> visiting colleagues in Paris (including Coq developers), and later had
>> discussions with other people in Prague about related topics. They have
>> huge problems by being too uncritical about doing it like the majority
>> (or "industry") does.
> 
> Did those people also specify what kind of problems they encountered? Or
> is this just a gut feeling?

These are routine discussions between peers at the bottom of huge
software products like Isabelle or Coq (that are now indeed very elitist
circles, I cannot find another term for that).

Generally, I try to get an impression what the colleagues are doing,
what problems they have and why, put our own situation into a broader
perspective, and learn from the good and bad things of the other team.

Short conclusion: we are in exceedingly good shape for a project of that
age.


That was topped by a talk by Claudio Sacerdoti Coen at Prague, LML
workshop
https://www.cicm-conference.org/2019/cicm.php?event=lml&menu=general
about "Attempts at skinning an elephant". It was a long-term experience
report by himself as developer of Coq plugins (the elephant is the Coq
code base). Unfortunately he has neither paper nor slides on the web.

His rather drastic statements of the talk will be a starting point for
my next discussions with the Coq developers in the next round of the
dialogue. Ultimately, I want to help them improve the overall quality of
their software project -- we cannot carry the full weight of ITP users
alone.


	Makarius