tuned
authorboehmes
Fri Sep 04 13:57:56 2009 +0200 (2009-09-04)
changeset 32518e3c4e337196c
parent 32517 bfe7573a239b
child 32520 4942abb40a55
child 32521 f20cc66b2c74
tuned
src/HOL/IsaMakefile
src/HOL/Mirabelle/MirabelleTest.thy
src/HOL/Mirabelle/Mirabelle_Test.thy
src/HOL/Mirabelle/ROOT.ML
src/HOL/Mirabelle/Tools/mirabelle_arith.ML
src/HOL/Mirabelle/Tools/mirabelle_metis.ML
src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML
src/HOL/Mirabelle/Tools/mirabelle_refute.ML
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
src/HOL/Mirabelle/lib/scripts/report.pl
     1.1 --- a/src/HOL/IsaMakefile	Fri Sep 04 10:58:50 2009 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Fri Sep 04 13:57:56 2009 +0200
     1.3 @@ -1124,7 +1124,7 @@
     1.4  
     1.5  HOL-Mirabelle: HOL $(LOG)/HOL-Mirabelle.gz
     1.6  
     1.7 -$(LOG)/HOL-Mirabelle.gz: $(OUT)/HOL Mirabelle/MirabelleTest.thy \
     1.8 +$(LOG)/HOL-Mirabelle.gz: $(OUT)/HOL Mirabelle/Mirabelle_Test.thy \
     1.9    Mirabelle/Mirabelle.thy Mirabelle/Tools/mirabelle.ML Mirabelle/ROOT.ML \
    1.10    Mirabelle/Tools/mirabelle_arith.ML \
    1.11    Mirabelle/Tools/mirabelle_metis.ML \
     2.1 --- a/src/HOL/Mirabelle/MirabelleTest.thy	Fri Sep 04 10:58:50 2009 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,22 +0,0 @@
     2.4 -(* Title: MirabelleTest.thy
     2.5 -   Author: Sascha Boehme
     2.6 -*)
     2.7 -
     2.8 -header {* Simple test theory for Mirabelle actions *}
     2.9 -
    2.10 -theory MirabelleTest
    2.11 -imports Main Mirabelle
    2.12 -uses
    2.13 -  "Tools/mirabelle_arith.ML"
    2.14 -  "Tools/mirabelle_metis.ML"
    2.15 -  "Tools/mirabelle_quickcheck.ML"
    2.16 -  "Tools/mirabelle_refute.ML"
    2.17 -  "Tools/mirabelle_sledgehammer.ML"
    2.18 -begin
    2.19 -
    2.20 -(*
    2.21 -  only perform type-checking of the actions,
    2.22 -  any reasonable test would be too complicated
    2.23 -*)
    2.24 -
    2.25 -end
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Mirabelle/Mirabelle_Test.thy	Fri Sep 04 13:57:56 2009 +0200
     3.3 @@ -0,0 +1,22 @@
     3.4 +(* Title: Mirabelle_Test.thy
     3.5 +   Author: Sascha Boehme
     3.6 +*)
     3.7 +
     3.8 +header {* Simple test theory for Mirabelle actions *}
     3.9 +
    3.10 +theory Mirabelle_Test
    3.11 +imports Main Mirabelle
    3.12 +uses
    3.13 +  "Tools/mirabelle_arith.ML"
    3.14 +  "Tools/mirabelle_metis.ML"
    3.15 +  "Tools/mirabelle_quickcheck.ML"
    3.16 +  "Tools/mirabelle_refute.ML"
    3.17 +  "Tools/mirabelle_sledgehammer.ML"
    3.18 +begin
    3.19 +
    3.20 +(*
    3.21 +  only perform type-checking of the actions,
    3.22 +  any reasonable test would be too complicated
    3.23 +*)
    3.24 +
    3.25 +end
     4.1 --- a/src/HOL/Mirabelle/ROOT.ML	Fri Sep 04 10:58:50 2009 +0200
     4.2 +++ b/src/HOL/Mirabelle/ROOT.ML	Fri Sep 04 13:57:56 2009 +0200
     4.3 @@ -1,1 +1,1 @@
     4.4 -use_thy "MirabelleTest";
     4.5 +use_thy "Mirabelle_Test";
     5.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_arith.ML	Fri Sep 04 10:58:50 2009 +0200
     5.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_arith.ML	Fri Sep 04 13:57:56 2009 +0200
     5.3 @@ -9,7 +9,7 @@
     5.4    if Mirabelle.can_apply timeout Arith_Data.arith_tac pre
     5.5    then log "arith: succeeded"
     5.6    else ()
     5.7 -  handle TimeLimit.TimeOut => log "arith: time out"
     5.8 +  handle TimeLimit.TimeOut => log "arith: timeout"
     5.9  
    5.10  fun invoke _ = Mirabelle.register (Mirabelle.catch "arith: " arith_action)
    5.11  
     6.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_metis.ML	Fri Sep 04 10:58:50 2009 +0200
     6.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_metis.ML	Fri Sep 04 13:57:56 2009 +0200
     6.3 @@ -20,7 +20,7 @@
     6.4      |> add_info
     6.5      |> log
     6.6    end
     6.7 -  handle TimeLimit.TimeOut => log "metis: time out"
     6.8 +  handle TimeLimit.TimeOut => log "metis: timeout"
     6.9  
    6.10  fun invoke _ = Mirabelle.register (Mirabelle.catch "metis: " metis_action)
    6.11  
     7.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML	Fri Sep 04 10:58:50 2009 +0200
     7.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML	Fri Sep 04 13:57:56 2009 +0200
     7.3 @@ -14,7 +14,7 @@
     7.4        NONE => log "quickcheck: no counterexample"
     7.5      | SOME _ => log "quickcheck: counterexample found")
     7.6    end
     7.7 -  handle TimeLimit.TimeOut => log "quickcheck: time out"
     7.8 +  handle TimeLimit.TimeOut => log "quickcheck: timeout"
     7.9  
    7.10  fun invoke args =
    7.11    Mirabelle.register (Mirabelle.catch "quickcheck: " (quickcheck_action args))
     8.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_refute.ML	Fri Sep 04 10:58:50 2009 +0200
     8.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_refute.ML	Fri Sep 04 13:57:56 2009 +0200
     8.3 @@ -27,7 +27,7 @@
     8.4          else SOME "real counterexample (bug?)"
     8.5        else
     8.6          if Substring.isSubstring "time limit" writ_log
     8.7 -        then SOME "no counterexample (time out)"
     8.8 +        then SOME "no counterexample (timeout)"
     8.9          else if Substring.isSubstring "Search terminated" writ_log
    8.10          then SOME "no counterexample (normal termination)"
    8.11          else SOME "no counterexample (unknown)"
     9.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Sep 04 10:58:50 2009 +0200
     9.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Sep 04 13:57:56 2009 +0200
     9.3 @@ -55,7 +55,7 @@
     9.4        TimeLimit.timeLimit timeout atp (Proof.get_goal st)
     9.5    in if success then (message, SOME (time, thm_names)) else (message, NONE) end
     9.6    handle ResHolClause.TOO_TRIVIAL => ("trivial", SOME (0, []))
     9.7 -       | TimeLimit.TimeOut => ("time out", NONE)
     9.8 +       | TimeLimit.TimeOut => ("timeout", NONE)
     9.9         | ERROR msg => ("error: " ^ msg, NONE)
    9.10  
    9.11  in
    9.12 @@ -87,7 +87,7 @@
    9.13      fun apply_metis thms = Mirabelle.can_apply timeout (metis thms) st
    9.14      fun timed_metis thms =
    9.15        uncurry with_time (Mirabelle.cpu_time apply_metis thms)
    9.16 -      handle TimeLimit.TimeOut => "time out"
    9.17 +      handle TimeLimit.TimeOut => "timeout"
    9.18             | ERROR msg => "error: " ^ msg
    9.19      fun log_metis s = log (metis_tag ^ s)
    9.20    in
    10.1 --- a/src/HOL/Mirabelle/lib/scripts/report.pl	Fri Sep 04 10:58:50 2009 +0200
    10.2 +++ b/src/HOL/Mirabelle/lib/scripts/report.pl	Fri Sep 04 13:57:56 2009 +0200
    10.3 @@ -39,7 +39,7 @@
    10.4      $metis_succeeded++;
    10.5      $metis_time += $1;
    10.6    }
    10.7 -  if (m/^metis \(sledgehammer\): time out/) {
    10.8 +  if (m/^metis \(sledgehammer\): timeout/) {
    10.9      $metis_timeout++;
   10.10    }
   10.11  }