[isabelle-dev] the state of the lattice theories

[Makarius]

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>
>> 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