isabelle: src/HOL/TPTP/MaSh_Eval.thy@e0dc738eb08c (annotated)

48285 902ab51dd12a renaming blanchet parents: 48284 diff changeset	1	(* Title: HOL/TPTP/MaSh_Eval.thy
48234 06216c789ac9 moved MaSh into own files blanchet parents: diff changeset	2	Author: Jasmin Blanchette, TU Muenchen
06216c789ac9 moved MaSh into own files blanchet parents: diff changeset	3	*)
06216c789ac9 moved MaSh into own files blanchet parents: diff changeset	4
58889 5b7a9633cfa8 modernized header uniformly as section; wenzelm parents: 58206 diff changeset	5	section {* MaSh Evaluation Driver *}
48234 06216c789ac9 moved MaSh into own files blanchet parents: diff changeset	6
48285 902ab51dd12a renaming blanchet parents: 48284 diff changeset	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 06216c789ac9 moved MaSh into own files blanchet parents: diff changeset	9	begin
06216c789ac9 moved MaSh into own files blanchet parents: diff changeset	10
48891 c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 48333 diff changeset	11	ML_file "mash_eval.ML"
c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 48333 diff changeset	12
48284 a3cb8901d60c clean up dependencies blanchet parents: 48251 diff changeset	13	sledgehammer_params
57456 eb5515784992 clean up MaSh evaluation driver blanchet parents: 57434 diff changeset	14	[provers = e, max_facts = 64, strict, dont_slice, type_enc = poly_guards??,
eb5515784992 clean up MaSh evaluation driver blanchet parents: 57434 diff changeset	15	lam_trans = combs, timeout = 30, dont_preplay, minimize]
48236 e174ecc4f5a4 instantiate induction rules blanchet parents: 48235 diff changeset	16
48235 40655464a93b MaSh evaluation driver blanchet parents: 48234 diff changeset	17	ML {*
54717 42c209a6c225 support for polml-5.5.2; wenzelm parents: 51182 diff changeset	18	Multithreading.max_threads_value ()
50458 85739c08d126 (re)introduce (even more) aggressive parallelism, for the benefit of those users with dozens of CPU cores blanchet parents: 50448 diff changeset	19	*}
85739c08d126 (re)introduce (even more) aggressive parallelism, for the benefit of those users with dozens of CPU cores blanchet parents: 50448 diff changeset	20
85739c08d126 (re)introduce (even more) aggressive parallelism, for the benefit of those users with dozens of CPU cores blanchet parents: 50448 diff changeset	21	ML {*
48285 902ab51dd12a renaming blanchet parents: 48284 diff changeset	22	open MaSh_Eval
48235 40655464a93b MaSh evaluation driver blanchet parents: 48234 diff changeset	23	*}
40655464a93b MaSh evaluation driver blanchet parents: 48234 diff changeset	24
40655464a93b MaSh evaluation driver blanchet parents: 48234 diff changeset	25	ML {*
55208 11dd3d1da83b compile blanchet parents: 55198 diff changeset	26	val params = Sledgehammer_Commands.default_params @{theory} []
50513 cacf3cdb3276 tuning blanchet parents: 50484 diff changeset	27	val prob_dir = prefix ^ "mash_problems"
48235 40655464a93b MaSh evaluation driver blanchet parents: 48234 diff changeset	28	*}
40655464a93b MaSh evaluation driver blanchet parents: 48234 diff changeset	29
40655464a93b MaSh evaluation driver blanchet parents: 48234 diff changeset	30	ML {*
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	()
0a740d127187 have MaSh evaluator keep all raw problem/solution files in a directory blanchet parents: 50437 diff changeset	35	*}
0a740d127187 have MaSh evaluator keep all raw problem/solution files in a directory blanchet parents: 50437 diff changeset	36
0a740d127187 have MaSh evaluator keep all raw problem/solution files in a directory blanchet parents: 50437 diff changeset	37	ML {*
0a740d127187 have MaSh evaluator keep all raw problem/solution files in a directory blanchet parents: 50437 diff changeset	38	if do_it then
57456 eb5515784992 clean up MaSh evaluation driver blanchet parents: 57434 diff changeset	39	evaluate_mash_suggestions @{context} params range (SOME prob_dir)
eb5515784992 clean up MaSh evaluation driver blanchet parents: 57434 diff changeset	40	[prefix ^ "mepo_suggestions",
eb5515784992 clean up MaSh evaluation driver blanchet parents: 57434 diff changeset	41	prefix ^ "mash_suggestions",
eb5515784992 clean up MaSh evaluation driver blanchet parents: 57434 diff changeset	42	prefix ^ "mash_prover_suggestions",
eb5515784992 clean up MaSh evaluation driver blanchet parents: 57434 diff changeset	43	prefix ^ "mesh_suggestions",
eb5515784992 clean up MaSh evaluation driver blanchet parents: 57434 diff changeset	44	prefix ^ "mesh_prover_suggestions"]
eb5515784992 clean up MaSh evaluation driver blanchet parents: 57434 diff changeset	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	()
48235 40655464a93b MaSh evaluation driver blanchet parents: 48234 diff changeset	48	*}
40655464a93b MaSh evaluation driver blanchet parents: 48234 diff changeset	49
48234 06216c789ac9 moved MaSh into own files blanchet parents: diff changeset	50	end

author	wenzelm
	Tue, 31 Mar 2015 22:31:05 +0200
changeset 59886	e0dc738eb08c
parent 58889	5b7a9633cfa8
child 62925	f1bdf10f95d8
permissions	-rw-r--r--