[isabelle-dev] Towards Isabelle2011 release

Lucas Dixon ldixon at inf.ed.ac.uk
Tue Jan 25 12:48:51 CET 2011


I get a (minor) error when running this version (MacOS 10.6, 
double-clicking on "isa2011-test2.app" icon):

if I have theory file being processed, and I quit Isabelle/Aquamacs, I 
get a dialogue box telling me that I have active processes, and do I 
want to kill them. If I say "yes", then I get a error window saying 
something like:

2011-01-25 11:42:54.894 Emacs[7555:623] ns_raise_fr
2011-01-25 11:42:58.407 Emacs[7555:623] notification
2011-01-25 11:43:01.187 Emacs[7555:623] ns_raise_fr
2011-01-25 11:43:02.788 Emacs[7555:623] notification
2011-01-25 11:43:31.366 Emacs[7555:623] notification

Seems to be coming from the Isabelle application wrapper:
Scenario 2: I start-up by Aquamacs directly - not via the Isabelle icon, 
using my emacs settings which starts PG using the load-file command, 
then when I quit (by command-Q). In this case, I don't get a 
dialogue-box telling me about the active processes; instead, I get the 
typical emacs mini-buffer message. When I say "yes" there, it quits 
without any strange error messages.

best,
lucas

On 24/01/2011 15:12, Makarius wrote:
> Here is another test release:
>
> http://www4.in.tum.de/~wenzelm/test/isa2011-test2/
>
> while the main Isabelle code base seems to be in good shape, there are
> various issues with the overall integration of external tools on the
> different platforms that we support officially. Some of them have been
> resolved.
>
> Some notable changes:
>
> * contrib/spass-3.7: make it actually work on x86-darwin (Leopard)
> (avoiding really weird crashes and strange error messages with
> Sledgehammer)
>
> * contrib/cvc3-2.2: make it actually work on darwin without Mac Ports
>
> * contrib/z3: make it actually work on x86_64-linux; still not working
> on Windows/Cygwin (?) unavailable on Mac OS X (!)
>
> * Cygwin: Back to old ProofGeneral-3.7.1.1 with ancient XEmacs, because
> PG 4.x with GNU Emacs 23 is very slow here.
>
> * ProofGeneral-4.1pre110112: deleted .elc files on Linux to improve
> compatibility with GNU Emacs 23.1.x instead of 23.2.1
>
> In the Mac OS X app/dmg I have also exchanged GNU Emacs 23.2.x ("no
> nonsense version") with Aquamacs 2.1, although it looks again like this
> is the choice between Scylla and Charybdis.
>
> It is also unclear when exactly PG 4.1-final will be released this week.
>
>
> Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>


-- 
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.




More information about the isabelle-dev mailing list