Re: [isabelle-dev] White space in theory names
On Thu, 12 Jun 2014, Florian Haftmann wrote: This is an offspring from http://fa.isabelle.narkive.com/QI1dxXvo/isabelle-quotient-type-command-fails I do not recommend white space in theory names: over the years proper naming conventions have been increasingly enforced for logical entities like variable names etc. The issue with theory names maybe just escaped attention due to its almost extralogical nature. Allowing white space would be definitely a move in the wrong direction. Theory names were indeed quite informal some decades ago, but have slowly gained a more formal and disciplined status, like any other logical entity with a canonical name space. The transition towards properly qualified and authentic theory names is not yet complete, but this spring I got *almost* there. (The attempt was defeated by various technical side-conditions imposed by the still existing Isar TTY loop, as well as some unexpected problems with the HOL-Light importer.) the fact that the quotient package would cut a name at white space borders nevertheless seems strange to me and would deserve an inspection. This is due to slightly odd bundle trickery as I called it in my change 745f568837f1, which also removes a deadly handle _ =. Note that I was cleaning up and robustifying other system interfaces in the usual way and passed-by accidentally (see also 8bedca4bd5a3). The fragility exposed on this thread is caused by taking an internal long name, and scanning that again as outer token. This works under the assumption that names are (qualified) identifiers, which is almost always the case these days. The qualification prevents overlap with Isar keywords, unless people define very odd keywords themselves that look like long identifiers. An alternative is to produce quotes around the name, before parsing it again. It is up to Ondřej if he wants to make this yet more robust -- there are more than 2 weeks left before the Isabelle2014-RC1 repository fork. Makarius___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Theory_Data.extend still needed?
On Sat, 28 Jun 2014, Florian Haftmann wrote: grep -rIPn 'val\s+extend\s*=\s*[^I ]' src ./Pure/context.ML:554:val extend = Data.extend; (which is not relevant since this is the definition of Theory_Data istelf) There are a few occurences of fun extend, e.g. in src/Pure/theory.ML. (Note that the val for extend or merge is a canonical source of SML/NJ unhappiness.) Conceptually, the extend operation is a single-armed merge; the implementation manual also covers it to some extent. It allows data slots to participate in the graph structure (although there might be other ways to achieve that today, e.g. via theory begin/end hooks). Actual use of extend is rare and usually somewhat exotic, but also happens to be in important kernel modules. Since there is no true counterindication against it, we should keep things as is. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Towards the Isabelle2014 release
On Tue, 1 Jul 2014, Makarius wrote: I am about to update the website, such that Isabelle2014-RC0 can be published with an approximation of the one for the coming release. I will tag Isabelle2014-RC0 today or tomorrow, shooting blindly at the repository. This is not a regular release candidate yet, but a preliminary version used at VSL 2014, e.g. for the Isabelle tutorial. It will be also announced on isabelle-users, such that people can start some testing. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] sledgehammer problem malformed message
Hi Leo, Am 04.07.2014 um 07:48 schrieb Leo Freitas leo.frei...@newcastle.ac.uk: I was playing with HOL-Word to see if I could bring some discharged VCs from another tool into Isabelle. When I tried sledgehammer on it I got the error message for Z3 Thanks for the report! We will look into this. It may take some time because of a deadline, though. And do let us know should you run into more issues with Z3 (which we upgraded to 4.3 from 3.2 in this version, requiring a major overhaul of our infrastructure). Cheers, Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
