It looks like the setup for blast changed, in the following entries is a non-terminating blast call. They do not seam to be related to the change at all:
Graph_Theory ShortestPath Rank_Nullity_Theorem Echelon_Form Gauss_Jordan Interestingly in Jordan_Normal_Form QR_Decomposition a real :: 'a => real is required! Both introduce a type class with group/vector-space homomorphism. I did _not_ look yet into: JinjaThreads Ordinary_Differential_Equations Affine_Arithmetic Akra_Bazzi - Johannes Am Mittwoch, den 11.11.2015, 18:29 +0100 schrieb Johannes Hölzl: > 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
