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
