Re: [isabelle-dev] Datatypes Isatest failures
Hi again, Am 17.09.2014 um 11:40 schrieb Jasmin Christian Blanchette jasmin.blanche...@gmail.com: 1. HOL-Proofs times out since September 14 on at-poly-e. On September 13, we had Timing HOL-Proofs (2 threads, 3161.882s elapsed time, 2889.329s cpu time, 840.167s GC time, factor 0.91) Finished HOL-Proofs (0:54:37 elapsed time, 0:48:53 cpu time, factor 0.89) which is close to the timeout (1 hour, I believe) but not *that* close. Still, the failures on September 14, 15, 16, and 17 have been consistent enough to suggest that change be0f5d8d511b (the only relevant one between Sept. 13 and 14) is the cause, in which case I have a strong suspicion about subst_tac. It doesn't seem like subst_tac had anything to do with it. I still have no idea about what made HOL-Proofs slower on at-poly-e beween September 13 and 14. The log reveals nothing special, except a truncation at the end. (while processing Predicate.thy). My personal inclination would be to disable this test for this platform -- HOL-Proofs isn't exactly used by many people, and I'm not sure there's much value in running CPUs for 1 hour each night to test it on some slow hardware and old version of Poly/ML (5.3). I see the following options as relatively painless ways of solving this: 1. Increase the timeout from 3600 s to, e.g. 4800. 2. Make HOL-Proofs and dependencies ISABELLE_FULL_TEST. 3. Introduce another condition to control whether HOL-Proofs should be built. Does anybody have an opinion? Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Proposal for localized interpretations
Dear developers, Jasmin mentioned to me that his new implementation allows to select which plugins should be applied. Currently, the code generator has its own manager of plugins (Code.datatype_interpretation) and I would be very happy if certain plugins could be disabled selectively upon code_datatype commands. For example, in AFP/Coinductive, I would like code_datatype to not change the code equations for the partial_term_of instantiations, because it does not (and cannot in general) adapt the equations for narrowing, but the two should be in sync. At present (AFP/222773085523), I have to undo the effect of the partial_term_of plugin in Lazy_LList.thy and Lazy_TLList.thy by writing ugly code equations. It would be much easier to disable the plugin locally for this declaration. I would expect that if Jasmin's plugin manager is also used in the code generator, it would be easy to implement plugin selection for code_datatype, too. Best, Andreas On 05/09/14 10:36, Jasmin Christian Blanchette wrote: Hi all, The interpretation mechanism, as defined in Pure/interpretation.ML, is used in a few places in Isabelle, including the new (co)datatype package, for allowing other tools and users to register their hooks. Unfortunately, it works at the theory level, which interacts poorly with local definitions. For example, if you try locale A = fixes a :: 'a assumes a = a begin datatype_new 'b x = X 'b end with Isabelle2014, you will get Undeclared hyps: A a The error(s) above occurred for the goal statement⌂: left_total R ⟹ left_total (A.rel_x R) This error arises in the Transfer hook. I can think of no way to solve this at the theory level. To solve this issue, I introduced my own interpretation mechanism, in HOL/Tools/Ctr_Sugar/local_interpretation.ML, that works both on theories and local theories. If you look at it, you will see that it is mostly a copy-paste job. The key insight is that there are three scenarios (taking datatypes as our example): 1. The datatype is defined after the hook is registered. 2a. The datatype is defined before the hook is registered. 2b. The dataype and the hooks are registered in two parallel theories, which are later merged. In case 1, one can imagine having the datatype directly giving its local theory to the hook. This is what local_interpretation.ML does, and this is enough to solve the problem in the example above. In case 2a and 2b, things have to be done at the theory level, like before, but this is a rarer case (e.g. we have no local datatypes in Main). Also, the odd signature management that was necessary before to make 2a and 2b work (cf. my April 2 email to this mailing list) is now centralized (cf. e6e3b20340be). I would like to propose either replacing the old mechanism by the new one or having both live in parallel in Pure. It is certainly not perfect, but it is IMO an improvement over the statu quo. What do you think? Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Products over lists – naming convention for big sums and products.
On 18/09/2014 15:47, Florian Haftmann wrote: Changeset #fe083c681ed8 introduces products over lists. There has been some private discussion whether there could be a serious attempt to establish a new consistent naming scheme for summation and products over collections. a) for lists: sum_list (← listsum), prod_list (← listprod) b) for multisets: Sum_mset (← msetsum), Prod_mset (← msetprod) c) for finite sets: Sum (← setsum), Prod (← setprod) Looking again at the result of our discussion I still like it. Tobias As far as can be forseen, 58 theories would be affected by a switch as suggested by a). b) is no big issue. c) is maybe beyond what should be reasonably attempted (218 affected theories). Suggestions welcome. Cheers, Florian ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Products over lists – naming convention for big sums and products.
A gain in legibility for sure. Larry On 18 Sep 2014, at 15:11, Tobias Nipkow nip...@in.tum.de wrote: On 18/09/2014 15:47, Florian Haftmann wrote: Changeset #fe083c681ed8 introduces products over lists. There has been some private discussion whether there could be a serious attempt to establish a new consistent naming scheme for summation and products over collections. a) for lists: sum_list (← listsum), prod_list (← listprod) b) for multisets: Sum_mset (← msetsum), Prod_mset (← msetprod) c) for finite sets: Sum (← setsum), Prod (← setprod) Looking again at the result of our discussion I still like it. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Printing integers in Isabelle/ML
When printing integers, there is a funny historic artefact: Library.string_of_int :: int - string examples 1705, ~42 -- ie. ML syntax Library.signed_string_of_int :: int - string examples 1705, -42 -- ie. conventional syntax ML_Syntax.print_int is an alias for Library.string_of_int What is particularly confusing about string_of_int vs. signed_string_of_int that actually both return »signed« strings. The naive expectation would be something like: Library.string_of_int :: int - string examples 1705, -42 -- ie. conventional syntax ML_Syntax.print_int :: int - string examples 1705, ~42 -- ie. ML syntax But there would be a considerable amount of code to be checked and sorted out then -- without support from the type system. Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
