simplified some time constants;
authorwenzelm
Tue Nov 02 20:55:12 2010 +0100 (2010-11-02)
changeset 40301bf39a257b3d3
parent 40300 d4487353b3a0
child 40302 2a33038d858b
simplified some time constants;
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
src/HOL/Mutabelle/mutabelle_extra.ML
src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy
src/HOL/Tools/Predicate_Compile/code_prolog.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/Tools/async_manager.ML
src/HOL/Tools/try.ML
src/Pure/Concurrent/future.ML
src/Pure/ML-Systems/multithreading_polyml.ML
src/Pure/System/isabelle_process.ML
     1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Nov 02 20:31:46 2010 +0100
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Nov 02 20:55:12 2010 +0100
     1.3 @@ -497,8 +497,8 @@
     1.4      |> snd
     1.5    end
     1.6  
     1.7 -val try_inner_timeout = Time.fromSeconds 5
     1.8 -val try_outer_timeout = Time.fromSeconds 30
     1.9 +val try_inner_timeout = seconds 5.0
    1.10 +val try_outer_timeout = seconds 30.0
    1.11  
    1.12  fun sledgehammer_action args id (st as {pre, name, ...}: Mirabelle.run_args) =
    1.13    let val goal = Thm.major_prem_of (#goal (Proof.goal pre)) in
     2.1 --- a/src/HOL/Mutabelle/mutabelle_extra.ML	Tue Nov 02 20:31:46 2010 +0100
     2.2 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Tue Nov 02 20:55:12 2010 +0100
     2.3 @@ -248,7 +248,7 @@
     2.4    end
     2.5  
     2.6  fun is_executable_term thy t =
     2.7 -  can (TimeLimit.timeLimit (Time.fromMilliseconds 2000)
     2.8 +  can (TimeLimit.timeLimit (seconds 2.0)
     2.9      (Quickcheck.test_term
    2.10        (Context.proof_map (Quickcheck.map_test_params (apfst (K (1, 0)))) (ProofContext.init_global thy))
    2.11        (SOME "SML"))) (preprocess thy [] t)
     3.1 --- a/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy	Tue Nov 02 20:31:46 2010 +0100
     3.2 +++ b/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy	Tue Nov 02 20:55:12 2010 +0100
     3.3 @@ -125,7 +125,7 @@
     3.4    limited_predicates = [],
     3.5    replacing = [],
     3.6    manual_reorder = [],
     3.7 -  timeout = Time.fromSeconds 10,
     3.8 +  timeout = seconds 10.0,
     3.9    prolog_system = Code_Prolog.SWI_PROLOG}) *}
    3.10  
    3.11  
     4.1 --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Tue Nov 02 20:31:46 2010 +0100
     4.2 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Tue Nov 02 20:55:12 2010 +0100
     4.3 @@ -120,7 +120,7 @@
     4.4  structure System_Config = Generic_Data
     4.5  (
     4.6    type T = system_configuration
     4.7 -  val empty = {timeout = Time.fromSeconds 10, prolog_system = SWI_PROLOG}
     4.8 +  val empty = {timeout = seconds 10.0, prolog_system = SWI_PROLOG}
     4.9    val extend = I;
    4.10    fun merge ({timeout = timeout1, prolog_system = prolog_system1},
    4.11          {timeout = timeout2, prolog_system = prolog_system2}) =
     5.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Nov 02 20:31:46 2010 +0100
     5.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Nov 02 20:55:12 2010 +0100
     5.3 @@ -1809,7 +1809,7 @@
     5.4            let
     5.5              val [nrandom, size, depth] = arguments
     5.6            in
     5.7 -            rpair NONE (TimeLimit.timeLimit (Time.fromSeconds 20) (fn () => fst (DSequence.yieldn k
     5.8 +            rpair NONE (TimeLimit.timeLimit (seconds 20.0) (fn () => fst (DSequence.yieldn k
     5.9                (Code_Runtime.dynamic_value_strict (Dseq_Random_Result.get, put_dseq_random_result, "Predicate_Compile_Core.put_dseq_random_result")
    5.10                  thy NONE (fn proc => fn g => fn nrandom => fn size => fn s => g nrandom size s |>> DSequence.map proc)
    5.11                    t' [] nrandom size
    5.12 @@ -1817,14 +1817,14 @@
    5.13                depth true)) ())
    5.14            end
    5.15        | DSeq =>
    5.16 -          rpair NONE (TimeLimit.timeLimit (Time.fromSeconds 20) (fn () => fst (DSequence.yieldn k
    5.17 +          rpair NONE (TimeLimit.timeLimit (seconds 20.0) (fn () => fst (DSequence.yieldn k
    5.18              (Code_Runtime.dynamic_value_strict (Dseq_Result.get, put_dseq_result, "Predicate_Compile_Core.put_dseq_result")
    5.19                thy NONE DSequence.map t' []) (the_single arguments) true)) ())
    5.20        | Pos_Generator_DSeq =>
    5.21            let
    5.22              val depth = (the_single arguments)
    5.23            in
    5.24 -            rpair NONE (TimeLimit.timeLimit (Time.fromSeconds 20) (fn () => fst (Lazy_Sequence.yieldn k
    5.25 +            rpair NONE (TimeLimit.timeLimit (seconds 20.0) (fn () => fst (Lazy_Sequence.yieldn k
    5.26                (Code_Runtime.dynamic_value_strict (New_Dseq_Result.get, put_new_dseq_result, "Predicate_Compile_Core.put_new_dseq_result")
    5.27                thy NONE (fn proc => fn g => fn depth => g depth |> Lazy_Sequence.mapa proc)
    5.28                t' [] depth))) ())
    5.29 @@ -1835,7 +1835,7 @@
    5.30              val seed = Random_Engine.next_seed ()
    5.31            in
    5.32              if stats then
    5.33 -              apsnd (SOME o accumulate) (split_list (TimeLimit.timeLimit (Time.fromSeconds 20)
    5.34 +              apsnd (SOME o accumulate) (split_list (TimeLimit.timeLimit (seconds 20.0)
    5.35                (fn () => fst (Lazy_Sequence.yieldn k
    5.36                  (Code_Runtime.dynamic_value_strict
    5.37                    (Lseq_Random_Stats_Result.get, put_lseq_random_stats_result, "Predicate_Compile_Core.put_lseq_random_stats_result")
    5.38 @@ -1844,7 +1844,7 @@
    5.39                      |> Lazy_Sequence.mapa (apfst proc))
    5.40                      t' [] nrandom size seed depth))) ()))
    5.41              else rpair NONE
    5.42 -              (TimeLimit.timeLimit (Time.fromSeconds 20) (fn () => fst (Lazy_Sequence.yieldn k
    5.43 +              (TimeLimit.timeLimit (seconds 20.0) (fn () => fst (Lazy_Sequence.yieldn k
    5.44                  (Code_Runtime.dynamic_value_strict
    5.45                    (Lseq_Random_Result.get, put_lseq_random_result, "Predicate_Compile_Core.put_lseq_random_result")
    5.46                    thy NONE 
    5.47 @@ -1853,7 +1853,7 @@
    5.48                      t' [] nrandom size seed depth))) ())
    5.49            end
    5.50        | _ =>
    5.51 -          rpair NONE (TimeLimit.timeLimit (Time.fromSeconds 20) (fn () => fst (Predicate.yieldn k
    5.52 +          rpair NONE (TimeLimit.timeLimit (seconds 20.0) (fn () => fst (Predicate.yieldn k
    5.53              (Code_Runtime.dynamic_value_strict (Pred_Result.get, put_pred_result, "Predicate_Compile_Core.put_pred_result")
    5.54                thy NONE Predicate.map t' []))) ()))
    5.55       handle TimeLimit.TimeOut => error "Reached timeout during execution of values"
     6.1 --- a/src/HOL/Tools/async_manager.ML	Tue Nov 02 20:31:46 2010 +0100
     6.2 +++ b/src/HOL/Tools/async_manager.ML	Tue Nov 02 20:55:12 2010 +0100
     6.3 @@ -80,8 +80,8 @@
     6.4  
     6.5  (* main manager thread -- only one may exist *)
     6.6  
     6.7 -val min_wait_time = Time.fromMilliseconds 300;
     6.8 -val max_wait_time = Time.fromSeconds 10;
     6.9 +val min_wait_time = seconds 0.3;
    6.10 +val max_wait_time = seconds 10.0;
    6.11  
    6.12  fun replace_all bef aft =
    6.13    let
     7.1 --- a/src/HOL/Tools/try.ML	Tue Nov 02 20:31:46 2010 +0100
     7.2 +++ b/src/HOL/Tools/try.ML	Tue Nov 02 20:55:12 2010 +0100
     7.3 @@ -20,7 +20,7 @@
     7.4    ProofGeneralPgip.add_preference Preferences.category_tracing
     7.5        (Preferences.bool_pref auto "auto-try" "Try standard proof methods.")
     7.6  
     7.7 -val default_timeout = Time.fromSeconds 5
     7.8 +val default_timeout = seconds 5.0
     7.9  
    7.10  fun can_apply timeout_opt pre post tac st =
    7.11    let val {goal, ...} = Proof.goal st in
     8.1 --- a/src/Pure/Concurrent/future.ML	Tue Nov 02 20:31:46 2010 +0100
     8.2 +++ b/src/Pure/Concurrent/future.ML	Tue Nov 02 20:55:12 2010 +0100
     8.3 @@ -253,7 +253,7 @@
     8.4  val status_ticks = Unsynchronized.ref 0;
     8.5  
     8.6  val last_round = Unsynchronized.ref Time.zeroTime;
     8.7 -val next_round = Time.fromMilliseconds 50;
     8.8 +val next_round = seconds 0.05;
     8.9  
    8.10  fun scheduler_next () = (*requires SYNCHRONIZED*)
    8.11    let
     9.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML	Tue Nov 02 20:31:46 2010 +0100
     9.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Tue Nov 02 20:55:12 2010 +0100
     9.3 @@ -120,10 +120,10 @@
     9.4  fun tracing_time detailed time =
     9.5    tracing
     9.6     (if not detailed then 5
     9.7 -    else if Time.>= (time, Time.fromMilliseconds 1000) then 1
     9.8 -    else if Time.>= (time, Time.fromMilliseconds 100) then 2
     9.9 -    else if Time.>= (time, Time.fromMilliseconds 10) then 3
    9.10 -    else if Time.>= (time, Time.fromMilliseconds 1) then 4 else 5);
    9.11 +    else if Time.>= (time, seconds 1.0) then 1
    9.12 +    else if Time.>= (time, seconds 0.1) then 2
    9.13 +    else if Time.>= (time, seconds 0.01) then 3
    9.14 +    else if Time.>= (time, seconds 0.001) then 4 else 5);
    9.15  
    9.16  fun real_time f x =
    9.17    let
    9.18 @@ -202,13 +202,13 @@
    9.19                Posix.Signal.int)
    9.20        | NONE => ())
    9.21        handle OS.SysErr _ => () | IO.Io _ =>
    9.22 -        (OS.Process.sleep (Time.fromMilliseconds 100); if n > 0 then kill (n - 1) else ());
    9.23 +        (OS.Process.sleep (seconds 0.1); if n > 0 then kill (n - 1) else ());
    9.24  
    9.25      val _ =
    9.26        while ! result = Wait do
    9.27          let val res =
    9.28            sync_wait (SOME orig_atts)
    9.29 -            (SOME (Time.+ (Time.now (), Time.fromMilliseconds 100))) cond lock
    9.30 +            (SOME (Time.+ (Time.now (), seconds 0.1))) cond lock
    9.31          in if Exn.is_interrupt_exn res then kill 10 else () end;
    9.32  
    9.33      (*cleanup*)
    10.1 --- a/src/Pure/System/isabelle_process.ML	Tue Nov 02 20:31:46 2010 +0100
    10.2 +++ b/src/Pure/System/isabelle_process.ML	Tue Nov 02 20:55:12 2010 +0100
    10.3 @@ -81,7 +81,7 @@
    10.4        (case receive mbox of
    10.5          SOME msg =>
    10.6           (List.app (fn s => TextIO.output (out_stream, s)) msg;
    10.7 -          loop (Mailbox.receive_timeout (Time.fromMilliseconds 20)))
    10.8 +          loop (Mailbox.receive_timeout (seconds 0.02)))
    10.9        | NONE => (try TextIO.flushOut out_stream; loop (SOME o Mailbox.receive)));
   10.10    in fn () => loop (SOME o Mailbox.receive) end;
   10.11  
   10.12 @@ -165,7 +165,7 @@
   10.13  
   10.14  fun init in_fifo out_fifo = ignore (Simple_Thread.fork false (fn () =>
   10.15    let
   10.16 -    val _ = OS.Process.sleep (Time.fromMilliseconds 500);  (*yield to raw ML toplevel*)
   10.17 +    val _ = OS.Process.sleep (seconds 0.5);  (*yield to raw ML toplevel*)
   10.18      val _ = Output.raw_stdout Symbol.STX;
   10.19  
   10.20      val _ = quick_and_dirty := true;  (* FIXME !? *)