1 (* Title: HOL/TPTP/MaSh_Export.thy
2 Author: Jasmin Blanchette, TU Muenchen
5 header {* MaSh Exporter *}
11 ML_file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML" (*###*)
12 ML_file "mash_export.ML"
15 [provers = spass, max_facts = 32, strict, dont_slice, type_enc = mono_native,
16 lam_trans = lifting, timeout = 2, dont_preplay, minimize]
18 declare [[sledgehammer_instantiate_inducts = false]]
20 hide_fact (open) HOL.ext
23 Multithreading.max_threads_value ()
31 val do_it = true (*###*) (* switch to "true" to generate the files *)
32 val thys = [@{theory List}]
33 val params as {provers, ...} = Sledgehammer_Commands.default_params @{theory} []
34 val prover = hd provers
35 val range = (1, (* ### NONE *) SOME 100)
38 val max_suggestions = 1024
40 val prefix = "/tmp/" ^ dir ^ "/"
45 Isabelle_System.mkdir (Path.explode prefix)
50 ML {* Options.put_default @{system_option MaSh} "sml_knn" *}
54 generate_mash_suggestions @{context} params (range, step) thys linearize max_suggestions
55 (prefix ^ "mash_sml_knn_suggestions")
60 ML {* Options.put_default @{system_option MaSh} "sml_nb" *}
64 generate_mepo_suggestions @{context} params (range, step) thys linearize max_suggestions
65 (prefix ^ "mash_sml_nb_suggestions")
70 ML {* Options.put_default @{system_option MaSh} "py" *}
74 generate_mepo_suggestions @{context} params (range, step) thys linearize max_suggestions
75 (prefix ^ "mepo_suggestions")
82 generate_accessibility @{context} thys linearize (prefix ^ "mash_accessibility")
89 generate_features @{context} thys (prefix ^ "mash_features")
96 generate_isar_dependencies @{context} range thys linearize (prefix ^ "mash_dependencies")
103 generate_isar_commands @{context} prover (range, step) thys linearize max_suggestions
104 (prefix ^ "mash_commands")
111 generate_mepo_suggestions @{context} params (range, step) thys linearize max_suggestions
112 (prefix ^ "mepo_suggestions")
119 generate_mesh_suggestions max_suggestions (prefix ^ "mash_suggestions")
120 (prefix ^ "mepo_suggestions") (prefix ^ "mesh_suggestions")
127 generate_prover_dependencies @{context} params range thys linearize
128 (prefix ^ "mash_prover_dependencies")
135 generate_prover_commands @{context} params (range, step) thys linearize max_suggestions
136 (prefix ^ "mash_prover_commands")
143 generate_mesh_suggestions max_suggestions (prefix ^ "mash_prover_suggestions")
144 (prefix ^ "mepo_suggestions") (prefix ^ "mesh_prover_suggestions")