option parallel_proofs_reuse_timing controls reuse of log information -- since it is not always beneficial for performance;
authorwenzelm
Wed Feb 20 19:57:17 2013 +0100 (2013-02-20)
changeset 5123019192615911e
parent 51229 6e40d0bb89e3
child 51231 67882f99274e
child 51233 7b0c723562af
option parallel_proofs_reuse_timing controls reuse of log information -- since it is not always beneficial for performance;
etc/options
src/Pure/Tools/build.scala
     1.1 --- a/etc/options	Wed Feb 20 18:04:44 2013 +0100
     1.2 +++ b/etc/options	Wed Feb 20 19:57:17 2013 +0100
     1.3 @@ -53,6 +53,8 @@
     1.4    -- "level of parallel proof checking: 0, 1, 2"
     1.5  option parallel_proofs_threshold : int = 100
     1.6    -- "threshold for sub-proof parallelization"
     1.7 +option parallel_proofs_reuse_timing : bool = true
     1.8 +  -- "reuse timing information from old log file for parallel proof scheduling"
     1.9  
    1.10  
    1.11  section "Detail of Proof Recording"
     2.1 --- a/src/Pure/Tools/build.scala	Wed Feb 20 18:04:44 2013 +0100
     2.2 +++ b/src/Pure/Tools/build.scala	Wed Feb 20 19:57:17 2013 +0100
     2.3 @@ -288,12 +288,14 @@
     2.4  
     2.5    object Queue
     2.6    {
     2.7 -    def apply(tree: Session_Tree, get_timings: String => (List[Properties.T], Double)): Queue =
     2.8 +    def apply(tree: Session_Tree, load_timings: String => (List[Properties.T], Double)): Queue =
     2.9      {
    2.10        val graph = tree.graph
    2.11        val sessions = graph.keys.toList
    2.12  
    2.13 -      val timings = sessions.map(name => (name, get_timings(name)))
    2.14 +      val timings = sessions.map((name: String) =>
    2.15 +        if (tree(name).options.bool("parallel_proofs_reuse_timing")) (name, load_timings(name))
    2.16 +        else (name, (Nil, 0.0)))
    2.17        val command_timings =
    2.18          Map(timings.map({ case (name, (ts, _)) => (name, ts) }): _*).withDefaultValue(Nil)
    2.19        val session_timing =
    2.20 @@ -680,7 +682,7 @@
    2.21  
    2.22      /* queue with scheduling information */
    2.23  
    2.24 -    def get_timing(name: String): (List[Properties.T], Double) =
    2.25 +    def load_timings(name: String): (List[Properties.T], Double) =
    2.26      {
    2.27        val (path, text) =
    2.28          find_log(name + ".gz") match {
    2.29 @@ -703,7 +705,7 @@
    2.30        }
    2.31      }
    2.32  
    2.33 -    val queue = Queue(selected_tree, get_timing)
    2.34 +    val queue = Queue(selected_tree, load_timings)
    2.35  
    2.36  
    2.37      /* main build process */