[isabelle-dev] AFP dependencies: CAVA_LTL_Modelchecker

[Makarius]

On 12/10/17 21:49, Makarius wrote:

> In Isabelle/c75769065548 I have refined the tool further to print
> "actual session dependencies", based on the imported theories and
> minimized according to the session imports relation.

The new "isabelle imports -I" also helps to determine logically vacuous
sessions, which are merely there to produce intermediate heap images.
(Often they look like development artifacts that are no longer used.)

Included is an experiment to do eliminate that "buildchain" for
CAVA_LTL_Modelchecker. It actually reduces both source complexity and
runtime (threads=4).

Before:
Finished CAVA_buildchain1 (0:03:01 elapsed time, 0:06:09 cpu time,
factor 2.03)
Finished CAVA_buildchain3 (0:05:57 elapsed time, 0:08:47 cpu time,
factor 1.48)
Finished CAVA_LTL_Modelchecker (0:05:44 elapsed time, 0:06:49 cpu time,
factor 1.19)

After:
Finished CAVA_LTL_Modelchecker (0:06:55 elapsed time, 0:13:57 cpu time,
factor 2.02)


Also note that various "All_Of_Foo" theories become obsolete: such
purely administrative theory merges can also cost measurable runtime.


	Makarius
-------------- next part --------------
# HG changeset patch
# User wenzelm
# Date 1507841930 -7200
#      Thu Oct 12 22:58:50 2017 +0200
# Node ID 388b10b402abc12b1792011146cb82dacae757f2
# Parent  ddf5e04d1e6dec093eb9c8883abd916b49463c94
simplified session structure: reduces both source complexity and runtime;

diff -r ddf5e04d1e6d -r 388b10b402ab thys/CAVA_LTL_Modelchecker/ROOT
--- a/thys/CAVA_LTL_Modelchecker/ROOT	Thu Oct 12 22:45:03 2017 +0200
+++ b/thys/CAVA_LTL_Modelchecker/ROOT	Thu Oct 12 22:58:50 2017 +0200
@@ -1,25 +1,10 @@
 chapter AFP
 
-session CAVA_buildchain1 (AFP) = "LTL_to_GBA" +
-  options [document = false, timeout = 600]
+session CAVA_LTL_Modelchecker (AFP) = LTL_to_GBA +
+  options [timeout = 2400]
   sessions
     Gabow_SCC
-  theories
-    Gabow_SCC.All_Of_Gabow_SCC
-
-(*session CAVA_buildchain2 (AFP) = CAVA_buildchain1 +
-  options [document = false]
-  theories "../Nested_DFS/All_Of_Nested_DFS"*)
-
-session CAVA_buildchain3 (AFP) = CAVA_buildchain1 +
-  options [document = false, timeout = 1200]
-  sessions
     Promela
-  theories
-    Promela.All_Of_Promela
-
-session CAVA_LTL_Modelchecker (AFP) = CAVA_buildchain3 +
-  options [timeout = 1200]
   theories [document = false]
     "Nested_DFS/NDFS_SI_Statistics"
   theories