[isabelle-dev] the state of the lattice theories
makarius at sketis.net
Tue Aug 9 16:17:49 CEST 2011
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<peteg42 at gmail.com>
>>> 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
> See also this thread on isabelle-dev from 2009:
> 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.
More information about the isabelle-dev