isabelle: src/HOL/Tools/Mirabelle/mirabelle_try0.ML@ee45e96eb7c5 (annotated)

76183 8089593a364a proper file headers; wenzelm parents: 75003 diff changeset	1	(* Title: HOL/Tools/Mirabelle/mirabelle_try0.ML
47891 e3627a83b114 added "try0" tool to Mirabelle blanchet parents: diff changeset	2	Author: Jasmin Blanchette, TU Munich
73691 2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive; wenzelm parents: 62519 diff changeset	3	Author: Makarius
73847 58f6b41efe88 refactored Mirabelle to produce output in real time desharna parents: 73691 diff changeset	4	Author: Martin Desharnais, UniBw Munich
73691 2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive; wenzelm parents: 62519 diff changeset	5
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive; wenzelm parents: 62519 diff changeset	6	Mirabelle action: "try0".
47891 e3627a83b114 added "try0" tool to Mirabelle blanchet parents: diff changeset	7	*)
e3627a83b114 added "try0" tool to Mirabelle blanchet parents: diff changeset	8
73847 58f6b41efe88 refactored Mirabelle to produce output in real time desharna parents: 73691 diff changeset	9	structure Mirabelle_Try0: MIRABELLE_ACTION =
47891 e3627a83b114 added "try0" tool to Mirabelle blanchet parents: diff changeset	10	struct
e3627a83b114 added "try0" tool to Mirabelle blanchet parents: diff changeset	11
73847 58f6b41efe88 refactored Mirabelle to produce output in real time desharna parents: 73691 diff changeset	12	fun make_action ({timeout, ...} : Mirabelle.action_context) =
58f6b41efe88 refactored Mirabelle to produce output in real time desharna parents: 73691 diff changeset	13	let
58f6b41efe88 refactored Mirabelle to produce output in real time desharna parents: 73691 diff changeset	14	val generous_timeout = Time.scale 10.0 timeout
58f6b41efe88 refactored Mirabelle to produce output in real time desharna parents: 73691 diff changeset	15
75003 f21e7e6172a0 renamed run_action to run in Mirabelle.action record desharna parents: 74948 diff changeset	16	fun run ({pre, ...} : Mirabelle.command) =
73847 58f6b41efe88 refactored Mirabelle to produce output in real time desharna parents: 73691 diff changeset	17	if Timeout.apply generous_timeout (Try0.try0 (SOME timeout) ([], [], [], [])) pre then
58f6b41efe88 refactored Mirabelle to produce output in real time desharna parents: 73691 diff changeset	18	"succeeded"
58f6b41efe88 refactored Mirabelle to produce output in real time desharna parents: 73691 diff changeset	19	else
58f6b41efe88 refactored Mirabelle to produce output in real time desharna parents: 73691 diff changeset	20	""
75003 f21e7e6172a0 renamed run_action to run in Mirabelle.action record desharna parents: 74948 diff changeset	21	in ("", {run = run, finalize = K ""}) end
73847 58f6b41efe88 refactored Mirabelle to produce output in real time desharna parents: 73691 diff changeset	22
58f6b41efe88 refactored Mirabelle to produce output in real time desharna parents: 73691 diff changeset	23	val () = Mirabelle.register_action "try0" make_action
47891 e3627a83b114 added "try0" tool to Mirabelle blanchet parents: diff changeset	24
e3627a83b114 added "try0" tool to Mirabelle blanchet parents: diff changeset	25	end

author	wenzelm
	Mon, 25 Mar 2024 15:11:48 +0100
changeset 79983	ee45e96eb7c5
parent 76183	8089593a364a
child 81362	f586fdabe670
permissions	-rw-r--r--