Re: [isabelle-dev] Status of afp-devel

2017-09-28 Thread Gerwin.Klein
Imminent. I was waiting for the statistics part to be updated to the new qualified imports, but I think we’ll just handle that one separately. Cheers, Gerwin > On 28.09.2017, at 23:52, Makarius wrote: > > What is the status of the afp-devel repository? > >

[isabelle-dev] Status of afp-devel

2017-09-28 Thread Makarius
What is the status of the afp-devel repository? Isabelle2017-RC3 is fairly stable and deserves a proper afp-2017 repository fork. Having a clear correspondence of isabelle-dev vs. afp-devel and Isabelle2017 vs. afp-2017 also means that changes to the devel branches can be again more ambitious.

Re: [isabelle-dev] AFP statistics

2017-09-28 Thread 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

Re: [isabelle-dev] AFP statistics

2017-09-28 Thread Lawrence Paulson
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. Larry > On 28 Sep 2017, at 13:20, Tobias Nipkow

Re: [isabelle-dev] AFP statistics

2017-09-28 Thread Tobias Nipkow
The whole project started with this AFP paper: 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

Re: [isabelle-dev] AFP statistics

2017-09-28 Thread Lars Hupel
> The AFP statistics https://www.isa-afp.org/statistics.html is very nice > -- I often show the last diagram in presentations, as a proof of success > of Isabelle as application platform over the years. > > Who is actually responsible for this tool? Me and our student Max Haslbeck. It is part of

[isabelle-dev] AFP statistics

2017-09-28 Thread Makarius
The AFP statistics https://www.isa-afp.org/statistics.html is very nice -- I often show the last diagram in presentations, as a proof of success of Isabelle as application platform over the years. Who is actually responsible for this tool? Is there a chance to take into account how AFP entries