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 }