[isabelle-dev] AFP statistics

Lawrence Paulson lp15 at cam.ac.uk
Thu Sep 28 15:26:53 CEST 2017

We can be very proud of these figures. I have occasionally compared the source releases of Certain Other Systems over time, and noticed that proofs are still write-only: new proofs are added, but existing proofs are almost never changed.


> On 28 Sep 2017, at 13:20, Tobias Nipkow <nipkow at in.tum.de> wrote:
> The whole project started with this AFP paper:
> http://www21.in.tum.de/~nipkow/pubs/cicm15.html <http://www21.in.tum.de/~nipkow/pubs/cicm15.html>
> First Max developed this just to support the statistics in the paper but then he and Lars made it part of the AFP. There is also a hidden part that generates tex files for these and a number of further statistics that I use for talks.
> 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.
> Tobias

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20170928/98d5d2f4/attachment-0002.html>

More information about the isabelle-dev mailing list