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.)
This archive was generated by a fusion of
Pipermail (Mailman edition) and