Re: [isabelle] AFP and Library

On 31/08/2017 13:26, Florian Haftmann wrote:
Maybe we should look into which library theories change the most or split library into multiple sessions.

My personal experience suggests that substantial rebuilds after pull are
seldom triggered by changes to HOL-Library; most times, that is due to
changes to HOL-Main / HOL-Complex theories â however this is not based
on any accountable evidence, so it might indeed be interesting to know
which candidates in HOL-Library have considerable velocity.

From my analysis of these 123 revisions, 10% of the builds could have been reduced from 30-60 mins to a few minutes by a less bloated Library. This is clearly not dramatic but it is helpful.

In the past, we occasionally split off sessions from HOL-Library
(sometimes also HOL-ex) as separate parts, the latest of these being
HOL-Computation_Algebra.  Though scalability always played a part in the
considerations, we always managed to find a conceptual distinction to
make clear how the contents of the newly established session should look

I certainly support moving theories out of Library for conceptual reasons, and it may also have the desired side effect.

Concerning Data_Structures please note that this directory is dedicated to conceptually clean and simple models of data structures and not to efficient implementations. Hence it is not the right home for Library/RBT*.


After a casual look at

$ wc -l src/HOL/Library/*.thy | sort -n

the following rough ideas come to my mind:

a) Shift further material to Computational_Algebra, e. g. Extended* or
material on orders and lattices.

b) Shift material to Datastructures, e. g. RBT*

c) Split off technical Âutilities like Simps_Case_Conv, Pattern_Aliases
and Code_ to  a separate session HOL-Utilities (Âtools is already used
by a different tradition).


P. S. Since that is a post-release issue and the original issue not
relevant for users working on stable releases, we should move this
discussion to isabelle-dev.

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.