isabelle: src/HOL/Tools/Mirabelle/mirabelle_try0.ML@8f866fd6fae1 (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
82364 5af097d05e99 tuned signature desharna parents: 81363 diff changeset	15	val try0 = Try0.try0 (SOME timeout) Try0.empty_facts
73847 58f6b41efe88 refactored Mirabelle to produce output in real time desharna parents: 73691 diff changeset	16
75003 f21e7e6172a0 renamed run_action to run in Mirabelle.action record desharna parents: 74948 diff changeset	17	fun run ({pre, ...} : Mirabelle.command) =
82364 5af097d05e99 tuned signature desharna parents: 81363 diff changeset	18	if Timeout.apply generous_timeout (not o null o try0) pre then
73847 58f6b41efe88 refactored Mirabelle to produce output in real time desharna parents: 73691 diff changeset	19	"succeeded"
58f6b41efe88 refactored Mirabelle to produce output in real time desharna parents: 73691 diff changeset	20	else
58f6b41efe88 refactored Mirabelle to produce output in real time desharna parents: 73691 diff changeset	21	""
75003 f21e7e6172a0 renamed run_action to run in Mirabelle.action record desharna parents: 74948 diff changeset	22	in ("", {run = run, finalize = K ""}) end
73847 58f6b41efe88 refactored Mirabelle to produce output in real time desharna parents: 73691 diff changeset	23
58f6b41efe88 refactored Mirabelle to produce output in real time desharna parents: 73691 diff changeset	24	val () = Mirabelle.register_action "try0" make_action
47891 e3627a83b114 added "try0" tool to Mirabelle blanchet parents: diff changeset	25
e3627a83b114 added "try0" tool to Mirabelle blanchet parents: diff changeset	26	end

author	wenzelm
	Wed, 25 Jun 2025 16:35:25 +0200
changeset 82768	8f866fd6fae1
parent 82364	5af097d05e99
permissions	-rw-r--r--