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
On Tue, 11 Jan 2011, David Aspinall wrote: (error defpacustom: missing :type keyword or wrong :type value) Thanks -- just patched pg-pamacs.el which should fix. Can you re-try? Now the error is: (error Invalid menu item in easymenu) I've already tried myself to look through all the occurrences of 'integer and add a analogous 'float versions. This turned out to affect approx. 5 files, when I gave up. Included is a tiny changeset to activate the pgipfloat protocol message on the Isabelle side, so you can see yourself. You need to build HOL-Plain at the least, which is a bit faster than full HOL. Makarius# HG changeset patch # User wenzelm # Date 1294763673 -3600 # Node ID 6f7efa7dc4e0e5141fbd3ab80c941dd771c2f54e # Parent f1e7e244dcf5bdeb25b5340845c5dc6f7edf1a15 actually emit pgipfloat message; diff -r f1e7e244dcf5 -r 6f7efa7dc4e0 src/Pure/ProofGeneral/pgip_types.ML --- a/src/Pure/ProofGeneral/pgip_types.ML Tue Jan 11 17:00:21 2011 +0100 +++ b/src/Pure/ProofGeneral/pgip_types.ML Tue Jan 11 17:34:33 2011 +0100 @@ -272,7 +272,7 @@ | Pgipbool = pgipbool | Pgipint _ = pgipint | Pgipnat = pgipint -| Pgipreal = pgipint (* FIXME sic? *) +| Pgipreal = pgipfloat | Pgipstring = pgipstring | Pgipconst _ = pgipconst | Pgipchoice _ = pgipchoice ___ 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
