isabelle: src/HOL/TPTP/MaSh_Eval.thy@d01ca5e9e0da (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
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 62925 diff changeset	5	section \<open>MaSh Evaluation Driver\<close>
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
69605 a96320074298 isabelle update -u path_cartouches; wenzelm parents: 69597 diff changeset	11	ML_file \<open>mash_eval.ML\<close>
48891 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
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 62925 diff changeset	17	ML \<open>
62925 f1bdf10f95d8 tuned signature; wenzelm parents: 58889 diff changeset	18	Multithreading.max_threads ()
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 62925 diff changeset	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 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 62925 diff changeset	21	ML \<open>
48285 902ab51dd12a renaming blanchet parents: 48284 diff changeset	22	open MaSh_Eval
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 62925 diff changeset	23	\<close>
48235 40655464a93b MaSh evaluation driver blanchet parents: 48234 diff changeset	24
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 62925 diff changeset	25	ML \<open>
69597 ff784d5a5bfb isabelle update -u control_cartouches; wenzelm parents: 63167 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"
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 62925 diff changeset	28	\<close>
48235 40655464a93b MaSh evaluation driver blanchet parents: 48234 diff changeset	29
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 62925 diff changeset	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
73315 d01ca5e9e0da tuned; wenzelm parents: 69605 diff changeset	32	ignore (Isabelle_System.make_directory (Path.explode prob_dir))
50448 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 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 62925 diff changeset	35	\<close>
50448 0a740d127187 have MaSh evaluator keep all raw problem/solution files in a directory blanchet parents: 50437 diff changeset	36
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 62925 diff changeset	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
69597 ff784d5a5bfb isabelle update -u control_cartouches; wenzelm parents: 63167 diff changeset	39	evaluate_mash_suggestions \<^context> params range (SOME prob_dir)
57456 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	()
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 62925 diff changeset	48	\<close>
48235 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
	Sat, 27 Feb 2021 17:32:02 +0100
changeset 73315	d01ca5e9e0da
parent 69605	a96320074298
permissions	-rw-r--r--