Re: [isabelle] provers used by sledgehammer



Am 20/07/2012 16:43, schrieb Makarius:
> 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.

By default the person who introduced the tool in the first place or the one who
is responsible for the change that stops it functioning. That is you, I should
think.

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

For teaching it is still withing the critical range. We have first-hand
experience with students who are really frustrated because Isabelle/jedit
complains that there is something wrong with their text, but there isn't, the
incremental parsing has gone wrong.

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

Of course it would be great if somebody did volunteer, but Larry pointed out
some of the obstacles.

Tobias





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