One example was broken and I fixed it in 06bfc5cfaeab, but the rest went through as usual.
Fabian > Am 12.11.2015 um 11:00 schrieb Fabian Immler <imm...@in.tum.de>: > > Some examples have always been very slow. But I will double-check and mark > the slow ones as (* slow *) to reduce confusion in the future. > > Fabian > >> Am 11.11.2015 um 18:29 schrieb Johannes Hölzl <hoe...@in.tum.de>: >> >> Okay, I look at the AFP entries. >> >> I assume Affine_Arithmetic is just slow, but I can ask Fabian tomorrow >> if this is unusual. >> >> - Johannes >> >> Am Mittwoch, den 11.11.2015, 17:19 +0000 schrieb Lawrence Paulson: >>> It would be great if you could help. I have just committed some >>> corrections to a number of AFP theories, including that one I think. >>> Affine_Arithmetic comes with some examples that run extremely slowly; >>> I’m not sure whether there is a problem or whether it is always like >>> that. If you want to take over with those, I can do some more tidying >>> up with the main libraries. >>> >>> Larry >>> >>>> On 11 Nov 2015, at 17:17, Johannes Hölzl <hoe...@in.tum.de> wrote: >>>> >>>> Hi Larry, >>>> >>>> this is a huge change and after I adapted Markov_Models I see that it >>>> simplifies some proofs. >>>> >>>> If you want I can adapt all AFP entries for which I'm the maintainer, or >>>> which are related to Probability theory: >>>> >>>> Density_Compiler >>>> Integration >>>> Lower_Semicontinuous >>>> Markov_Models >>>> Ordinary_Differential_Equations >>>> Possibilistic_Noninterference >>>> Probabilistic_Noninterference >>>> UpDown_Scheme >>>> Girth_Chromatic >>>> Probabilistic_System_Zoo >>>> Random_Graph_Subgraph_Threshold >>>> pGCL >>>> >>>> Just tell me which of these you are already working on, so we can merge >>>> without conflicts. >>>> >>>> - Johannes >>>> >>>> >>>> Am Mittwoch, den 11.11.2015, 12:28 +0000 schrieb Lawrence Paulson: >>>>> I’m glad to have your support. It’s just possible that I might ask your >>>>> help in getting some things working in the AFP. >>>>> >>>>> Larry >>>>> >>>>>> On 10 Nov 2015, at 17:53, Manuel Eberl <ebe...@in.tum.de> wrote: >>>>>> >>>>>> This is very nice to hear. ‘real’ has plagued me for some time now and I >>>>>> am glad to see it gone. >>>>>> >>>>>> Thanks for the good work! >>>>>> >>>>>> >>>>>> On 10/11/15 17:45, Lawrence Paulson wrote: >>>>>>> The first phase of this project is finished: the function “real” now >>>>>>> has the monomorphic type nat => real and is simply an abbreviation for >>>>>>> the generic function, of_nat. In addition, the function “real_of_int” >>>>>>> abbreviates the generic function of_int. >>>>>>> >>>>>>> It took about a week to convert all the theories in the main >>>>>>> Isabelle/HOL directory. Most of them needed little or no attention, the >>>>>>> big exceptions being Probability (which frequently used “real” with the >>>>>>> type ereal => real) and Decision_Procs, which contained many thousands >>>>>>> of instances of “real” on integers and floats. >>>>>>> >>>>>>> The main priority at the moment is to fix the decision procedure mir, >>>>>>> which isn’t working but appears to be entirely unused. Then there is >>>>>>> still a lot of cleaning up to do, especially in Real.thy and its >>>>>>> ancestors. Two or three dozen theorems existed in duplicate forms, with >>>>>>> versions for “real” separate from versions for the other coercions; >>>>>>> occasionally these variants were named systematically, but often their >>>>>>> names were unrelated from the originals, and the names of variables in >>>>>>> the theorems were almost always different. The simplification status of >>>>>>> the two variants generally differed as well. Thus the behaviour of the >>>>>>> simplifier on a formula depended on which coercion had been used, and >>>>>>> in 150 cases, the simplification itself included the mapping of one >>>>>>> coercion to another (there were two equivalent theorems for doing this). >>>>>>> >>>>>>> Innumerable type constraints have now become redundant (things such as >>>>>>> real_of_int (i::int)), but I intend to leave them as they are. I have a >>>>>>> lot of AFP entries to fix. >>>>>>> >>>>>>> Larry >>>> >>>> >>>> _______________________________________________ >>>> 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 > > _______________________________________________ > 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
