Re: [isabelle-dev] Towards Isabelle2011 release
On Thu, 27 Jan 2011, Makarius wrote: Yet another test release: http://www4.in.tum.de/~wenzelm/test/isa2011-test3/ There is now an update of the same isa2011-test3 with a patched version of ProofGeneral-4.1pre110112 as follows: * Mac OS X fonts: instead of IsabelleText refer to STIXGeneral as fall back, which is somehow hardwired into Proof General 4.1 * (proof-full-annotation nil) for improved stability and performance. * (proof-strict-read-only t) for improved stability. There is a remaining issue with preferences http://proofgeneral.inf.ed.ac.uk/trac/ticket/387 which is a show-stopper for the Isabelle2011 release. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Towards Isabelle2011 release
On Fri, 28 Jan 2011, Makarius wrote: On Thu, 27 Jan 2011, Makarius wrote: Yet another test release: http://www4.in.tum.de/~wenzelm/test/isa2011-test3/ There is now an update of the same isa2011-test3 with a patched version of ProofGeneral-4.1pre110112 as follows: * Mac OS X fonts: instead of IsabelleText refer to STIXGeneral as fall back, which is somehow hardwired into Proof General 4.1 * (proof-full-annotation nil) for improved stability and performance. * (proof-strict-read-only t) for improved stability. There is a remaining issue with preferences http://proofgeneral.inf.ed.ac.uk/trac/ticket/387 which is a show-stopper for the Isabelle2011 release. This is one more update of http://www4.in.tum.de/~wenzelm/test/isa2011-test3/ The only difference to above is ProofGeneral-4.1pre101216 instead of ProofGeneral-4.1pre110112 as basis for our patches, so the problem of ticket/387 is absent. After one more round of looking closely at the distribution, we have a chance for the final Isabelle2011 snapshot on Sunday or Monday. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Towards Isabelle2011 release
Yet another test release: http://www4.in.tum.de/~wenzelm/test/isa2011-test3/ Some odd problems have shown up and addressed as follows: * contrib/z3: make native Windows executables actually work on x86-cygwin * quickcheck/codegen: eliminated serious race condition * slightly more robust Isabelle/Scala document processing, especially on systems with few cores, and on x86_64 * last-minute fixes for HOL-SPARK * ProofGeneral-4.1pre110112: option -f FONT can be used e.g. with IsabelleText to get proper Unicode symbols * Mac OS X app bundle is back to GNU Emacs 23.2.x (no-nonsense), default font configuration for IsabelleText font This is another chance to see if everything works. I hope that we manage the final release before the end of the months, which is now very close. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Towards Isabelle2011 release
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-...@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-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Towards Isabelle2011 release
On Tue, 25 Jan 2011, Lucas Dixon wrote: 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. The dialogue-box is part of the Isabelle.app bundle, it merely shows all results from stdout/stderr after the process has terminated. I reckon that the Aquamacs.app merely absorbs such traces, whereever they might come from. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Towards Isabelle2011 release
On Mon, 24 Jan 2011, Makarius wrote: * ProofGeneral-4.1pre110112: deleted .elc files on Linux to improve compatibility with GNU Emacs 23.1.x instead of 23.2.1 It is also unclear when exactly PG 4.1-final will be released this week. We stick with ProofGeneral-4.1pre110112 for the Isabelle2011 release until the dust on the PG 4.1-final development has settled. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Towards Isabelle2011 release
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-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Towards Isabelle2011 release
On Sat, 15 Jan 2011, Makarius wrote: The actual test branch for Isabelle2011 will probably start within the next few days -- on a separate repository clone where submission of changesets works via email or pull only. It looks like the point zero will be today, either in the afternoon or evening (GMT). So this is the very last chance for small amendments on the main Isabelle repository. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Towards Isabelle2011 release
On Mon, 17 Jan 2011, Makarius wrote: It looks like the point zero will be today, either in the afternoon or evening (GMT). As of version 54a4512e29a6 the release branch continues at http://isabelle.in.tum.de/repos/isabelle-release * Any urgent changes that need to go onto that need to be sent to me via email, as clean changesets without any merges inside. * Changes for isabelle-release should *not* be pushed to the main Isabelle repository, but they will come there after the release is shipped and the isabelle-release clone merged back. * isatest refers to isabelle-release * AFP morally refers to isabelle-release as well. (There are still some broken theories on AFP, probably due to some last minute changes in main HOL.) Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Towards Isabelle2011 release
On Mon, 17 Jan 2011, Makarius wrote: On Mon, 17 Jan 2011, Makarius wrote: It looks like the point zero will be today, either in the afternoon or evening (GMT). As of version 54a4512e29a6 the release branch continues at http://isabelle.in.tum.de/repos/isabelle-release This also means that http://isabelle.in.tum.de/repos/isabelle is again open for submissions for the post-release development cycle (cf. c78b786fe060). The only limitation is that big HOL library changes on the Isabelle development branch should be postponed, until AFP for Isabelle2011 is officially released. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
