--- a/src/HOL/Tools/ATP/atp_proof.ML Wed Aug 04 21:03:25 2021 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML Wed Aug 04 21:49:17 2021 +0200
@@ -54,6 +54,7 @@
val z3_tptpN : string
val zipperpositionN : string
val remote_prefix : string
+ val dummy_fofN : string
val dummy_tfxN : string
val dummy_thfN : string
@@ -117,6 +118,7 @@
val z3_tptpN = "z3_tptp"
val zipperpositionN = "zipperposition"
val remote_prefix = "remote_"
+val dummy_fofN = "dummy_fof"
val dummy_tfxN = "dummy_tfx"
val dummy_thfN = "dummy_thf"
--- a/src/HOL/Tools/Mirabelle/mirabelle.scala Wed Aug 04 21:03:25 2021 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle.scala Wed Aug 04 21:49:17 2021 +0200
@@ -62,7 +62,9 @@
val build_options =
options + "timeout_build=false" +
("mirabelle_actions=" + actions.mkString(";")) +
- ("mirabelle_theories=" + theories.mkString(","))
+ ("mirabelle_theories=" + theories.mkString(",")) +
+ ("mirabelle_output_dir=" + output_dir.implode)
+
progress.echo("Running Mirabelle ...")
@@ -192,8 +194,6 @@
"v" -> (_ => verbose = true),
"x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
- options = options + ("mirabelle_output_dir=" + output_dir.implode)
-
val sessions = getopts(args)
if (actions.isEmpty) getopts.usage()
@@ -207,7 +207,7 @@
val results =
progress.interrupt_handler {
- mirabelle(options, actions, output_dir,
+ mirabelle(options, actions, output_dir.absolute,
theories = theories,
selection = Sessions.Selection(
all_sessions = all_sessions,
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Wed Aug 04 21:03:25 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Wed Aug 04 21:49:17 2021 +0200
@@ -681,6 +681,11 @@
best_max_mono_iters = default_max_mono_iters,
best_max_new_mono_instances = default_max_new_mono_instances}
+
+val dummy_fof_format = FOF
+val dummy_fof_config = dummy_config Hypothesis dummy_fof_format "mono_guards??" false
+val dummy_fof = (dummy_fofN, fn () => dummy_fof_config)
+
val dummy_tfx_format = TFF (With_FOOL, Polymorphic)
val dummy_tfx_config = dummy_config Hypothesis dummy_tfx_format "mono_native_fool" false
val dummy_tfx = (dummy_tfxN, fn () => dummy_tfx_config)
@@ -725,7 +730,7 @@
val atps =
[agsyhol, alt_ergo, e, iprover, leo2, leo3, satallax, spass, vampire, z3_tptp, zipperposition,
remote_agsyhol, remote_alt_ergo, remote_e, remote_iprover, remote_leo2, remote_leo3,
- remote_waldmeister, remote_zipperposition, dummy_tfx, dummy_thf]
+ remote_waldmeister, remote_zipperposition, dummy_fof, dummy_tfx, dummy_thf]
val _ = Theory.setup (fold add_atp atps)