Re: [isabelle] provers used by sledgehammer



On Fri, 20 Jul 2012, Tobias Nipkow wrote:

It is customary to continue maintaining a tool until the replacement is ready for prime time. Currently jedit is not at the point (and PG still works). I expect that PG will be kept in a working state until key jedit problems like "Workaround: Cut/paste larger parts or reload buffer" and the absence of menus (which force people to remember and type commands) have been eliminated.

So who is continuing the maintenance of Proof General? It won't continue to work magically without doing anything.

One of the reasons why Isabelle/jEdit is still not as complete as I would like to have is the extra time that I have spent to keep Isabelle Proof General working in the last 4 years.

This is why I have now stopped its maintenance after the Isabelle2011-1 release; the Isabelle2012 version of Isabelle/jEdit is sufficient to be outside the critical range.

And again: I have now reason to see Isabelle Proof General broken too early after so many years taking care of it. So I would welcome someone standing forward to continue its maintenance. (It needs to be someone who understands what maintenance of sofware systems means in general.)


	Makarius





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