author | wenzelm |
Sun, 21 May 2017 23:41:46 +0200 | |
changeset 65895 | 744878d72021 |
parent 63167 | 0909deb8059b |
child 69597 | ff784d5a5bfb |
permissions | -rw-r--r-- |
48285 | 1 |
(* Title: HOL/TPTP/MaSh_Eval.thy |
48234 | 2 |
Author: Jasmin Blanchette, TU Muenchen |
3 |
*) |
|
4 |
||
63167 | 5 |
section \<open>MaSh Evaluation Driver\<close> |
48234 | 6 |
|
48285 | 7 |
theory MaSh_Eval |
58206
3e22d3ed829f
refactored MaSh files to avoid regenerating exports on each eval
blanchet
parents:
57456
diff
changeset
|
8 |
imports MaSh_Export_Base |
48234 | 9 |
begin |
10 |
||
48891 | 11 |
ML_file "mash_eval.ML" |
12 |
||
48284 | 13 |
sledgehammer_params |
57456 | 14 |
[provers = e, max_facts = 64, strict, dont_slice, type_enc = poly_guards??, |
15 |
lam_trans = combs, timeout = 30, dont_preplay, minimize] |
|
48236 | 16 |
|
63167 | 17 |
ML \<open> |
62925 | 18 |
Multithreading.max_threads () |
63167 | 19 |
\<close> |
50458
85739c08d126
(re)introduce (even more) aggressive parallelism, for the benefit of those users with dozens of CPU cores
blanchet
parents:
50448
diff
changeset
|
20 |
|
63167 | 21 |
ML \<open> |
48285 | 22 |
open MaSh_Eval |
63167 | 23 |
\<close> |
48235 | 24 |
|
63167 | 25 |
ML \<open> |
55208 | 26 |
val params = Sledgehammer_Commands.default_params @{theory} [] |
50513 | 27 |
val prob_dir = prefix ^ "mash_problems" |
63167 | 28 |
\<close> |
48235 | 29 |
|
63167 | 30 |
ML \<open> |
48250
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48245
diff
changeset
|
31 |
if do_it then |
50448
0a740d127187
have MaSh evaluator keep all raw problem/solution files in a directory
blanchet
parents:
50437
diff
changeset
|
32 |
Isabelle_System.mkdir (Path.explode prob_dir) |
0a740d127187
have MaSh evaluator keep all raw problem/solution files in a directory
blanchet
parents:
50437
diff
changeset
|
33 |
else |
0a740d127187
have MaSh evaluator keep all raw problem/solution files in a directory
blanchet
parents:
50437
diff
changeset
|
34 |
() |
63167 | 35 |
\<close> |
50448
0a740d127187
have MaSh evaluator keep all raw problem/solution files in a directory
blanchet
parents:
50437
diff
changeset
|
36 |
|
63167 | 37 |
ML \<open> |
50448
0a740d127187
have MaSh evaluator keep all raw problem/solution files in a directory
blanchet
parents:
50437
diff
changeset
|
38 |
if do_it then |
57456 | 39 |
evaluate_mash_suggestions @{context} params range (SOME prob_dir) |
40 |
[prefix ^ "mepo_suggestions", |
|
41 |
prefix ^ "mash_suggestions", |
|
42 |
prefix ^ "mash_prover_suggestions", |
|
43 |
prefix ^ "mesh_suggestions", |
|
44 |
prefix ^ "mesh_prover_suggestions"] |
|
45 |
(prefix ^ "mash_eval") |
|
48250
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48245
diff
changeset
|
46 |
else |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48245
diff
changeset
|
47 |
() |
63167 | 48 |
\<close> |
48235 | 49 |
|
48234 | 50 |
end |