[isabelle-dev] AFP

[Andrei Popescu]

>> Here we are back to the (wrong) assumption that Proof General could 
>> continue forever, without doing anything.

I do not assume this, and in time I will switch to Isabelle/jEdit -- my experience 

with working with Jasmin is already close to the "corridor full of smart people" 

experience anyway.  :-)  


I also appreciate your efforts to keep the old army hero alive with Isabelle.  


Andrei 



On Friday, May 16, 2014 10:57 AM, Makarius <makarius at sketis.net> wrote:
 
On Thu, 15 May 2014, Andrei Popescu wrote:

> Proof General is a silent proof partner who gives me a lot of space. By 
> contrast, Isabelle/jEdit seems like a corridor full of smart people who 
> keep offering to help me. I prefer to do proofs with my office door 
> closed.

Here we are back to the (wrong) assumption that Proof General could 
continue forever, without doing anything.

In the past 3 years of Proof General being "legacy" I have invested 
substantial work just to keep the status quo more or less.  Over more than 
5 years there were calls to arms, to hold the territory of the general, 
but no volunteers ever showed up at proofgeneral-devel at inf.ed.ac.uk.

Without anybody doing anything, the only option to remaining users of 
Proof General is to stick to the last Isabelle version that supported 
it, i.e. when the list of remaining uses of it has become empty.



    Makarius
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20140516/9225a2b2/attachment-0002.html>