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
# 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
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev