On Sun, 31 Jul 2011, Alexander Krauss wrote:
On 07/28/2011 04:58 PM, Brian Huffman wrote:
On Thu, Jul 28, 2011 at 1:01 AM, Peter Gammie<[email protected]>
wrote:
More generally, is there (or should there be) a bug/feature/wishlist
tracker for Isabelle for these sorts of things? It might help reduce
parallel developments, or least clarify what their relative strengths
are.
See also this thread on isabelle-dev from 2009:
http://thread.gmane.org/gmane.science.mathematics.logic.isabelle.devel/793
We do indeed have a number of long-standing issues, which may be worth
documenting more formally, to make it easier for people to learn about
the deeper reasons behind them. But this won't make them go away sooner,
as most of them are due to conceptual problems in the interactions of
different parts of the system. As a consequence, the "report -> analyze
-> fix" cycle often takes many years.
For certain things the cycle has indeed become so long that many people
are not even aware of ongoing things that are "well-known" to the ones
being responsible for a certain part of the system. In extreme cases this
can go as far that documented behaviour (according to the isar-ref and
implementation manual) is considered a "bug". This is one reason why it is
important to investigate the history with "hg annotate" and "hg churn" to
see who is responsible, before trying to "fix" something.
Concerning formal tracking in general, I am keen to see a really good
solution that is not a big issue in itself (as are trac or SourceForge).
It would probably take some weeks or months to investigate the market
situation, like I have done for Mercurial some years ago. (E.g. Jira by
Atlassian looks interesting, but did not spent more than 5 min. with it.)
Why don't you just start one yourself? I don't think it matters too
much who hosts it, as long as we can get enough people use it. I would
definitely use it.
I cannot follow this idea of "outsourcing" important infrastructure.
Wrt. "enough people using it" you need to account people according to
their volume of changes produced, not their heads.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
