On 28/09/17 14:20, Tobias Nipkow wrote: > The whole project started with this AFP paper: > > Concerning growth of articles. I am not sure we want to provide more > finegrained statistics for every entry, but attached you find a summary > slide. I cannot remember precisely what is measured, but at a first > approximation it tells us that over time every second line of an AFP > entry is modified.
These changes are probably of very mixed nature. Often this is just trivial maintenance like turning old 'def' into new 'define': I did not get very far with it recently, because AFP has become somewhat unwieldy. The session-qualified theory names reform should actually help to make this easier, since it allows to edit many different AFP sessions in the same PIDE process, without worrying about underlying session images. There are other factors that have made AFP maintenance increasingly difficult. I've taken your summary slide at BigProof (Cambridge, July 2017) as an indication that it is high time to improve the technology again. For example, the diagram shows a significant jump from 2011 to 2012: that was the point where I replaced the old "isabelle make" by "isabelle build", and David Matthews made the online heap compaction in Poly/ML. Thus full AFP builds shrank from 4h to 45min. Subsequently, routine changes became very easy and happened frequently. E.g. people were quite liberal in reworking basic HOL or library concepts and pushed that through all applications in AFP. We should see better times pretty soon: I've started to rework the build process right now. Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev