src/HOL/TPTP/MaSh_Eval.thy
author wenzelm
Sat Jan 05 17:24:33 2019 +0100 (11 months ago)
changeset 69597 ff784d5a5bfb
parent 63167 0909deb8059b
child 69605 a96320074298
permissions -rw-r--r--
isabelle update -u control_cartouches;
     1 (*  Title:      HOL/TPTP/MaSh_Eval.thy
     2     Author:     Jasmin Blanchette, TU Muenchen
     3 *)
     4 
     5 section \<open>MaSh Evaluation Driver\<close>
     6 
     7 theory MaSh_Eval
     8 imports MaSh_Export_Base
     9 begin
    10 
    11 ML_file "mash_eval.ML"
    12 
    13 sledgehammer_params
    14   [provers = e, max_facts = 64, strict, dont_slice, type_enc = poly_guards??,
    15    lam_trans = combs, timeout = 30, dont_preplay, minimize]
    16 
    17 ML \<open>
    18 Multithreading.max_threads ()
    19 \<close>
    20 
    21 ML \<open>
    22 open MaSh_Eval
    23 \<close>
    24 
    25 ML \<open>
    26 val params = Sledgehammer_Commands.default_params \<^theory> []
    27 val prob_dir = prefix ^ "mash_problems"
    28 \<close>
    29 
    30 ML \<open>
    31 if do_it then
    32   Isabelle_System.mkdir (Path.explode prob_dir)
    33 else
    34   ()
    35 \<close>
    36 
    37 ML \<open>
    38 if do_it then
    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")
    46 else
    47   ()
    48 \<close>
    49 
    50 end