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