On Fri, 5 Apr 2013, Thomas Sewell wrote:
By comparison, David is providing you with what would be considered a
good bug report in most open-source communities. It comes with a clear
explanation not only of what the problem is but what causes it to occur,
and how it might be fixed. In such communities, the proposed patches are
nearly never applied as-is, but they provide a far more useful starting
point than the average bug report.
All my complaints on this (and related) mail threads can be reduced to
this assumption about "most open-source comminities". This universal
standard simply does not exist, and the average open-source project just
produces junk. Especially people from NICTA / L4.verified should care
about the platform(s) they depend on -- this also includes Poly/ML.
Here we have a very unusual project -- it still exists after > 25 years
and the system is in fairly good shape. This is not an accident, it is the
consequence of a certain development process. But the air is getting
thinner and thinner as we still move on.
Larry had quite visionary ideas in his initial 1989 sketch of Isabelle,
including "Programs like Isabelle are not products: when they have served
their purpose, they are discarded." Historically, my biggest mistake was
to disregard that when there was still a chance.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
