Re: [isabelle] AFP and Library

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

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

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.


PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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