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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
