Re: [isabelle] the state of the lattice theories



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.

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.

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.

btw: The original claim, that a tracker would help reduce parallel developments is unclear to me.

Alex





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.