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 like.
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). Cheers, Florian 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.
Description: S/MIME Cryptographic Signature