[isabelle-dev] Towards Isabelle2011 release

Clemens Ballarin ballarin at in.tum.de
Tue Jan 25 18:56:13 CET 2011


Quoting Lucas Dixon <ldixon at inf.ed.ac.uk>:

> 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

These messages also appear on the terminal when Isabelle is launched  
via "isabelle emacs ...".  The "notification" message is printed  
whenever the emacs window loses the focus.

Clemens


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





More information about the isabelle-dev mailing list