[isabelle-dev] NEWS: proper session directories and faster PIDE startup

[Makarius]

On 12/09/2019 20:32, Makarius wrote:
> 
> Whenever I pass by this JNF-AFP-Lib session, I wonder if there is any
> remaining use of it. It quotes a lot of theories without a check if they
> are actually needed. Loading the material takes only 30s in my 8core
> machine.

Here are some concrete measurements on my 8 core machine with very fast
memory + SSD:

  ML_PLATFORM="x86_64_32-linux"
  ML_HOME="/home/makarius/.isabelle/contrib/polyml-5.8/x86_64_32-linux"
  ML_SYSTEM="polyml-5.8"
  ML_OPTIONS="--minheap 1500"

$ isabelle build -d '$AFP' Jordan_Normal_Form Polynomial_Factorization
Jordan_Normal_Form Polynomial_Factorization
Building JNF-AFP-Lib ...
Finished JNF-AFP-Lib (0:00:57 elapsed time, 0:03:46 cpu time, factor 3.92)
Running Polynomial_Factorization ...
Finished Polynomial_Factorization (0:00:26 elapsed time, 0:01:30 cpu
time, factor 3.44)
Running Jordan_Normal_Form ...
Finished Jordan_Normal_Form (0:02:43 elapsed time, 0:09:19 cpu time,
factor 3.42)
0:04:15 elapsed time, 0:14:36 cpu time, factor 3.42

$ isabelle build -d '$AFP' Jordan_Normal_Form Polynomial_Factorization
Running Jordan_Normal_Form ...
Finished Jordan_Normal_Form (0:02:58 elapsed time, 0:11:54 cpu time,
factor 4.01)
Running Polynomial_Factorization ...
Finished Polynomial_Factorization (0:00:39 elapsed time, 0:02:32 cpu
time, factor 3.86)
0:03:45 elapsed time, 0:14:26 cpu time, factor 3.85


The canonical changeset to "build faster without intermediate sessions"
is included (not pushed yet).


	Makarius
-------------- next part --------------
# HG changeset patch
# User wenzelm
# Date 1568314131 -7200
#      Thu Sep 12 20:48:51 2019 +0200
# Node ID 229812cc587410c279aece30432a26bd52fec64a
# Parent  98320942654aaf57ea6e91c1863b1ce192bc59cd
build faster without intermediate sessions;

diff -r 98320942654a -r 229812cc5874 thys/Jordan_Normal_Form/ROOT
--- a/thys/Jordan_Normal_Form/ROOT	Wed Sep 11 21:50:31 2019 +0200
+++ b/thys/Jordan_Normal_Form/ROOT	Thu Sep 12 20:48:51 2019 +0200
@@ -1,9 +1,16 @@
 chapter AFP
 
-session "Jordan_Normal_Form" (AFP) = "JNF-AFP-Lib" +
+session "Jordan_Normal_Form" (AFP) = "HOL-Algebra" +
   options [timeout = 1200]
   sessions
+    "Abstract-Rewriting"
+    "HOL-Cardinals"
+    Containers
+    Gauss_Jordan Matrix
     Polynomial_Factorization
+    Polynomial_Interpolation
+    Show
+    VectorSpace
   theories
     Missing_Ring
     Missing_Permutations
diff -r 98320942654a -r 229812cc5874 thys/Polynomial_Factorization/ROOT
--- a/thys/Polynomial_Factorization/ROOT	Wed Sep 11 21:50:31 2019 +0200
+++ b/thys/Polynomial_Factorization/ROOT	Thu Sep 12 20:48:51 2019 +0200
@@ -1,63 +1,18 @@
 chapter AFP
 
-session "JNF-AFP-Lib" (AFP) in "Lib" = "HOL-Algebra" +
-  description "Theories from HOL-Library and the Archive of Formal Proofs that are used by this entry"
-  options [timeout = 600]
-  sessions
-    Containers
-    "Abstract-Rewriting"
-    Gauss_Jordan Matrix
-    Polynomial_Interpolation
-    Show
-    VectorSpace
-    "HOL-Cardinals"
-  theories
-    Containers.Set_Impl
-    Matrix.Utility
-    Matrix.Ordered_Semiring
-    "Abstract-Rewriting.SN_Order_Carrier"
-    "Abstract-Rewriting.Relative_Rewriting"
-    Show.Show_Instances
-    VectorSpace.VectorSpace
-    Polynomial_Interpolation.Missing_Polynomial
-    Polynomial_Interpolation.Ring_Hom_Poly
-    "HOL-Library.AList"
-    "HOL-Library.Cardinality"
-    "HOL-Library.Char_ord"
-    "HOL-Library.Code_Binary_Nat"
-    "HOL-Library.Code_Target_Numeral"
-    "HOL-Library.DAList"
-    "HOL-Library.DAList_Multiset"
-    "HOL-Library.Infinite_Set"
-    "HOL-Library.Lattice_Syntax"
-    "HOL-Library.Mapping"
-    "HOL-Library.Monad_Syntax"
-    "HOL-Library.More_List"
-    "HOL-Library.Multiset"
-    "HOL-Library.Permutation"
-    "HOL-Library.Permutations"
-    "HOL-Library.IArray"
-    "HOL-Library.Phantom_Type"
-    "HOL-Library.Ramsey"
-    "HOL-Library.RBT_Impl"
-    "HOL-Library.Simps_Case_Conv"
-    "HOL-Library.While_Combinator"
-    "HOL-Computational_Algebra.Fundamental_Theorem_Algebra"
-    "HOL-Computational_Algebra.Fraction_Field"
-    "HOL-Computational_Algebra.Polynomial"
-    "HOL-Computational_Algebra.Primes"
-    "HOL-Cardinals.Order_Union"
-    "HOL-Cardinals.Wellorder_Extension"
-
-
-session Polynomial_Factorization (AFP) = "JNF-AFP-Lib" + 
+session Polynomial_Factorization (AFP) = "HOL-Algebra" + 
   description "Algebraic Numbers"
   options [timeout = 600]
   sessions
+    "Abstract-Rewriting"
+    "HOL-Cardinals"
+    Containers
+    Gauss_Jordan Matrix
     Partial_Function_MR
     Polynomial_Interpolation
     Show
     Sqrt_Babylonian
+    VectorSpace
   theories
     Missing_Multiset
     Missing_List