[isabelle-dev] Proof General 4.1pre
There is now a development snapshot of Proof General 4.1pre, provided by David Aspinall: http://proofgeneral.inf.ed.ac.uk/releases/ProofGeneral-4.1pre110112.tgz It looks pretty stable to me. There are only few remaining entries at http://proofgeneral.inf.ed.ac.uk/trac/ Are there still users of PG 3.x with recent Isabelle snapshots or versions from the repository? The question is if PG 4.1 converges sufficiently fast for Isabelle2011, and if we should switch to the PGIP update for floating point settings. This would mean to discontinue 4.0 and 3.x altogether. If there is the slightest doubt we can also keep the odd treatment of pgreal values in Isabelle2011 -- PG 4.1 would work nonetheless, despite our abuse of the protocol. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Proof General 4.1pre
The question is if PG 4.1 converges sufficiently fast for Isabelle2011, and if we should switch to the PGIP update for floating point settings. This would mean to discontinue 4.0 and 3.x altogether. I've been using PG 4.1 for a while now from cvs, and it works nicely, except that I've regularly experienced sync losses in connection with the undo-on-edit feature. I couldn't track this down enough to come up with a useful bug report yet, but it seems that switching off this feature solves the problem. Thus, if 4.1 is going to be used, I would recommend having undo-on-edit switched off by default (maybe this is the case anyway, I am not sure...) Alex ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Proof General 4.1pre
Quoting Makarius makar...@sketis.net: Are there still users of PG 3.x with recent Isabelle snapshots or versions from the repository? I do. I recently tried to use PG 4.0 with Aquamacs 2.1. That didn't seem to work, so I went back to PG 3.7.1.1 and Carbon Emacs 1.6 (based on GNU Emacs 22.3.1). I'd prefer using Aquamacs for the native cut-copy-paste. One thing that didn't work was fonts (under the assumption Unicode would produce the same results for both combinations; I have not special fonts installed), and instructions how to do this with minimal intervention would be appreciated. I think also the Isabelle/PG interaction did not work properly, and that's why I gave up in the end. PG 3.7.1.1 and Carbon Emacs 1.6 have their issues as well, but I know how to live with them ... Clemens ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Proof General 4.1pre
Are there still users of PG 3.x with recent Isabelle snapshots or versions from the repository? I am using PG 3.7.1.1 with XEmacs 21.4.21 and a recent version from the Isabelle repository. My motivation for not switching is that PG 4.x did not seem to work with XEmacs when I tried, and I have not yet figured out how to set up auto-completion that XEmacs provides with any other Emacs. Does anyone know how to do this? Andreas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
