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

[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?
> 
> 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.
> 
> 
>   Makarius
> ___
> 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] Status of afp-devel

[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.


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [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
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] AFP statistics

[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  wrote:
> 
> 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 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

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] AFP statistics

[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 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

On 28/09/2017 14:02, Makarius wrote:

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 evolve over time?
Right now, it only shows the year of first appearance with the *current*
size. Thus incrementally added sources (or whole sessions) are
attributed to the wrong year.

A prominent example is JinjaThreads, but newer entries like
Ordinary_Differential_Equations have grown significantly, too.


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev



slides.pdf
Description: Adobe PDF document


smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] AFP statistics

[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 the site generator that
is invoked every time a new entry is added.

The devel equivalent is available at
 and is re-generated every
time someone pushes to the repository. Currently that one shows wrong
dependency numbers because it hasn't been adapted yet to
session-qualified imports. I'm still working on a proper fix.

Cheers
Lars
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] AFP statistics

[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 evolve over time?
Right now, it only shows the year of first appearance with the *current*
size. Thus incrementally added sources (or whole sessions) are
attributed to the wrong year.

A prominent example is JinjaThreads, but newer entries like
Ordinary_Differential_Equations have grown significantly, too.


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev