Re: [isabelle-dev] Towards release
We have had this problem before with Isabelle2011. PG 4.x has a certain idea about using glyphs from existing Unicode fonts, with a preference for STIXGeneral as fall-back option As you'd expect, this is all highly configurable at PG level (see lib/unicode-tokens.el and isar/isar-unicode-tokens.el), I just set picked some reasonable default fonts and Unicode points which worked well when I wrote the code 3 years ago. I welcome improvements from anyone. By default all symbols are taken from a single Unicode font, which seems simplest and most sensible with the advent of STIX. There are mechanisms to try to choose fallback symbol renderings automatically, which can be taken glyphs or sequences of glyphs from other fonts (see isar-symbols-tokens-fallbacks). But the automation is tricky because the functions to determine whether a glyph is blank or not are not reliable. Mac users should be aware that there are issues with the underlying font support on the native Mac port of Emacs, although a couple of these have been fixed recently they haven't made it into a released version yet. http://proofgeneral.inf.ed.ac.uk/trac/ticket/338 http://proofgeneral.inf.ed.ac.uk/trac/ticket/409 I think the worst problem is broken super/sub scripts. I've checked that this *is* fixed now in the current nightly builds at http://emacsformacosx.com/builds, but it's probably not a good idea to bundle one of those with the release, 8-(. - David -- 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] Option type for auto tools timeout
(error defpacustom: missing :type keyword or wrong :type value) Thanks -- just patched pg-pamacs.el which should fix. Can you re-try? A quick grep through the elisp sources reveals that the 'float tag is not always handled in correspondance to 'integer, for example. What is the release schedule for PG 4.1 anyway? Should be good to go to fit with Isabelle-X release. Had hoped Coq multiple-file patch would be ready but probably won't. - D. -- 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] Option type for auto tools timeout
The dealine for the next Isabelle release is shortly after the start of the year 2011. If PG 4.1 is available by then, and works on Linux, Mac OS, Cygwin with the usual Emacsen, I see no problem emit pgreal for real-valued preferences. There is a patch now committed in PG CVS for a type pgipfloat. Officially syntax should match spec here: http://www.w3.org/TR/xmlschema-2/#float Emacs is not going to check but other stricter tools might. But this would also mean to abandon PG 3.7.1.1 and PG 4.0, so the 4.1 version needs to be beyond any doubt. I am myself hooked on the PG CVS for several weeks already. It looks fine, but I am not using it a lot. I did not hear anything from elsewhere, which means it works perfectly well, or nobody has tried it. For 4.0, there are over 300 direct downloads since 10th Oct, about a dozen registrations, but I don't know how many correspond to real users or real Isabelle users. (How many downloads does Isabelle get per month out of interest?) Feedback from bona fide committed Isabelle hackers welcome! http://proofgeneral.inf.ed.ac.uk/trac/ - D. -- 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] Aquamacs emacs
I have tried Aquamacs-2.0 with the CVS version of Proof General (from 12-Apr-2010) for 20min, and ran into two problems within the first 5min. One was due to Aquamacs failing to configure fonts for the buffer. The other was PG trac item #314 (Duplication of some special messages). These mysterious message problems might be also related to the general danger of loosing synchronisation, which have never been isolated to far. If you hit this problem within the first 5 mins perhaps you have a recipe to reproduce it? The last (non-spam) comment on the ticket suggests it is due to a change in Isabelle since Isabelle2009. http://proofgeneral.inf.ed.ac.uk/trac/ticket/314 Doesn't Mercurial have a tool to do a binary chop across through commits to help isolate this? - D. -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. ___ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] PG preferences (auto solve in particular)
I am also struggling again to find a combination of PG + Emacs that works on Mac OS. GNU Emacs 23 somehow fails -- tickets will come when I've managed to pin down the problems. OK, thanks. Would be good to bless one version. I am keen to cut down the number of supported Emacs versions for PG 4, which should make things easier for everyone. - D. -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
[isabelle-dev] PG preferences (auto solve in particular)
My general impression is that PG-4 prefers Emacs 23, but this usually requires to upgrade to newer Linux installations, which is apt to cause other problems, as we have seen. Emacs 23 doesn't require newer Linuxes, it can be compiled on recent-ish earlier OSes easily enough. Probably more easily than building obsolete versions of XEmacs! I have been using CVS builds of Emacs 23 for several years without many problems. But anyway, I hope Emacs 22 can be supported. - D. -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
[isabelle-dev] x-symbols
Lawrence Paulson wrote: Does anybody know what would cause the symbols that look like this? It is the latest version of proof general running under GNU Emacs 22.2.1 Nobody else came running so I'll answer... First of all: everyone will have a *much* better experience with Emacs 23.x if you can find/build a version. It's what persuaded me Emacs was worth sticking with. I wish they would release it properly. Some Linux distributions (e.g. Ubuntu) are distributing it as a package now (emacs-snapshot). Supposing you have to stick with Emacs 22.2: This effect is caused by using a font which does not have glyphs in the Unicode positions for the tokens. You can select a better font to improve matters, try: Tokens - Make fontsets and then Options - Set font/fontset and try the possibilities on the Fontset submenu. On the Linux I'm using right now, I get a better result with the fontset standard:16-dot-medium than I do with the custom pgXXX fontsets created by the first menu command. Not sure why, it wasn't the case when I wrote all the fontset support mess a year ago. I thought I had documented this somewhere but can't find it now, must admit. - David -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
[isabelle-dev] Isabelle2009 fails to handle interrupts
I don't believe this is PG's fault. I can reproduce problems in tty mode. With the previous version, you sent C-c C-c and it reliably interrupted and printed *** Interrupted. With Isabelle2009 interrupts may get ignored or go unreported and output and the following prompt may or may not appear. http://proofgeneral.inf.ed.ac.uk/trac/ticket/179 I've added some workaround but it's not easy to tell between a busy prover and one that's been interrupted and stopped sending output but is too secretive to tell you about it! - David -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
[isabelle-dev] HOL-Bali
PS bear in mind the top of http://proofgeneral.inf.ed.ac.uk/releases/ProofGeneral-3.7.1/CHANGES which warns exactly about this! -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
[isabelle-dev] Relation_Power.thy
You can achieve the above name space effect of symbols already via something like \caret_funpow, Aha -- we can easily do this in PG then instead of \caret1. which is presently unused because LaTeX output is a bit strange (as for \caret1). The idea is to make the output the same as \caret, of course (with the disadvantage that you can't wave your mouse over a piece of paper). - D. -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
[isabelle-dev] Proof General 3.7 for Isabelle 2007 -- final issues on Trac
Dear All, Makarius asked me to post a note here. If you have any issues you would like to see fixed in Proof General for the 3.7 release timed to coincide with Isabelle 2007, please report them to me via the Trac interface here: http://proofgeneral.inf.ed.ac.uk/trac You can create your own account or login with a shared account I just made, user name: isabelledev password: isabelledev When logged in, New Ticket appears in the tabs. To see a list of outstanding tickets to fix for this milestone, try this query: http://tinyurl.com/32woo4 If you're reported something to me in the past (or even recently) by email it would help to upload the report, I find it hard to keep track of emails and what has been fixed or not otherwise. I expect to get (a little bit) of time next week to work through these. Thanks, - David
