more explicit session dependency, for improved parallel performance of HOL-UNITY test session -- NB: separate 'theories' sections are sequential;
authorwenzelm
Thu, 21 Feb 2013 18:21:40 +0100
changeset 51236 f301ad90c48b
parent 51235 8333c10d1a6d
child 51237 22ba938ab10f
more explicit session dependency, for improved parallel performance of HOL-UNITY test session -- NB: separate 'theories' sections are sequential;
src/HOL/ROOT
--- a/src/HOL/ROOT	Thu Feb 21 16:00:48 2013 +0100
+++ b/src/HOL/ROOT	Thu Feb 21 18:21:40 2013 +0100
@@ -224,7 +224,7 @@
     "Guard/Auth_Guard_Public"
   files "document/root.tex"
 
-session "HOL-UNITY" in UNITY = HOL +
+session "HOL-UNITY" in UNITY = "HOL-Auth" +
   description {*
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1998  University of Cambridge
@@ -232,7 +232,6 @@
     Verifying security protocols using UNITY.
   *}
   options [document_graph]
-  theories [document = false] "../Auth/Public"
   theories
     (*Basic meta-theory*)
     "UNITY_Main"
@@ -276,12 +275,10 @@
   files "document/root.bib" "document/root.tex"
 
 session "HOL-ZF" in ZF = HOL +
-  description {* *}
   theories MainZF Games
   files "document/root.tex"
 
 session "HOL-Imperative_HOL" in Imperative_HOL = HOL +
-  description {* *}
   options [document_graph, print_mode = "iff,no_brackets"]
   theories [document = false]
     "~~/src/HOL/Library/Countable"