[isabelle-dev] AFP statistics

[Makarius]

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