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
