# HG changeset patch
# User desharna
# Date 1628106530 -7200
# Node ID 49884e54f13af00e280b0108ceb1d97d10765f47
# Parent  30ab39ab41177a35dbe4bcd0d7c1406546496b6e# Parent  8752420f337759ee0439e440283e08cf4bf3505f
merged

diff -r 8752420f3377 -r 49884e54f13a src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Wed Aug 04 21:00:37 2021 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Wed Aug 04 21:48:50 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"
 
diff -r 8752420f3377 -r 49884e54f13a src/HOL/Tools/Mirabelle/mirabelle.scala
--- a/src/HOL/Tools/Mirabelle/mirabelle.scala	Wed Aug 04 21:00:37 2021 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle.scala	Wed Aug 04 21:48:50 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,
diff -r 8752420f3377 -r 49884e54f13a src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Wed Aug 04 21:00:37 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Wed Aug 04 21:48:50 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)