[isabelle-dev] Towards the next release

Makarius makarius at sketis.net
Wed Nov 21 11:35:01 CET 2012


On Tue, 20 Nov 2012, Lawrence Paulson wrote:

> I am using version 4.1. I was having problems compiling 4.2, and it 
> doesn't seem to run in interpreted mode. I'm not sure what is changed 
> between 4.1 and 4.2 anyway.

I am unsure myself, but there was quite a lot of activity on the Coq side 
on the PG devel mailing list.

I've used 4.2 recently with Isabelle, and found it a bit awkward in some 
details.  Somehow the windows don't pop-up and disappear the way they did 
before, making it hard to work in the two-window mode of the ancient past 
that I am still using.  (If I were still involved, I would have spent a 
few days investigating this, produce tracker items, polish the elisp code 
myself.)

Maybe I should make an effort to get the hard-wrap for text paragraphs 
work smoothly in Isabelle/jEdit, so that I don't have to go back to Emacs 
just for that (the last thing where I still use the dinosaur).


> For the Emacs client, definitely Aquamacs. The other Emacs port is 
> terrible, in particular because it doesn't behave at all like a native 
> OS X application.

What I need for the release (on-time before the start of the RC phase) is 
this:

   * A version of Proof General as Isabelle component, like
     http://isabelle.in.tum.de/components/ProofGeneral-4.1.tar.gz
     (it must be platform/emacs independent, without .elc files).

   * A specification which Emacs.app needs to be included in the
     Isabelle.app -- I will do the final montage myself.

It is then up to remaining PG/Emacs users to test that in the RC phase of 
the release (2-3 weeks before lift-off).  I am not going myself again 
through the agony and desparation to make all this work in all reasonable 
combinations that users might have (as I used to do until October 2011).


> And this for me is still a problem with jEdit as well.

So what are the remaining problems?  It is time to list them and sort them 
out if possible.

At the Orleans Isabelle Tutorial someone had a very new Mac and was unable 
to copy-paste from the Output window, but that was Isabelle2012 with the 
Lobo browser, not the Rich_Text_Area of Isabelle/jEdit now.  (I will ask 
him to test again before the coming release).

Anything else that hinders Isabelle/jEdit use, especially on the Mac?


 	Makarius



More information about the isabelle-dev mailing list