# HG changeset patch
# User paulson
# Date 1626462792 -3600
# Node ID 4cca14dc577c16c51252c01e85ea7f6799230b56
# Parent  1a0a536b8aafd19bf01d5bd5dda384c5b560e739# Parent  df976eefcba097c6a2119a7bbe31c139fb076ff9
merged

diff -r df976eefcba0 -r 4cca14dc577c src/Doc/Sledgehammer/document/root.tex
--- a/src/Doc/Sledgehammer/document/root.tex	Fri Jul 16 14:43:25 2021 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex	Fri Jul 16 20:13:12 2021 +0100
@@ -803,9 +803,6 @@
 \item[\labelitemi] \textbf{\textit{remote\_leo3}:} The remote version of Leo-III
 runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
 
-\item[\labelitemi] \textbf{\textit{remote\_vampire}:} The remote version of
-Vampire runs on Geoff Sutcliffe's Miami servers.
-
 \item[\labelitemi] \textbf{\textit{remote\_waldmeister}:} Waldmeister is a unit
 equality prover developed by Hillenbrand et al.\ \cite{waldmeister}. It can be
 used to prove universally quantified equations using unconditional equations,
diff -r df976eefcba0 -r 4cca14dc577c src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Fri Jul 16 14:43:25 2021 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Fri Jul 16 20:13:12 2021 +0100
@@ -47,7 +47,6 @@
   val iproverN : string
   val leo2N : string
   val leo3N : string
-  val pirateN : string
   val satallaxN : string
   val spassN : string
   val vampireN : string
@@ -110,7 +109,6 @@
 val iproverN = "iprover"
 val leo2N = "leo2"
 val leo3N = "leo3"
-val pirateN = "pirate"
 val satallaxN = "satallax"
 val spassN = "spass"
 val vampireN = "vampire"
@@ -638,32 +636,6 @@
    >> (fn ((((num, rule), deps), u), names) =>
           [((num, these names), Unknown, u, rule, map (rpair []) deps)])) x
 
-fun parse_pirate_dependency x = (Scan.option ($$ "-") |-- scan_general_id) x
-fun parse_pirate_dependencies x =
-  Scan.repeat (parse_pirate_dependency --| Scan.option ($$ "," || $$ " ")) x
-fun parse_pirate_file_source x =
-  ((Scan.this_string "Input" || Scan.this_string "Conj") |-- $$ "(" |-- scan_general_id
-     --| $$ ")") x
-fun parse_pirate_inference_source x =
-  (scan_general_id -- ($$ "(" |-- parse_pirate_dependencies --| $$ ")")) x
-fun parse_pirate_source x =
-  (parse_pirate_file_source >> (fn s => File_Source ("", SOME s))
-   || parse_pirate_inference_source >> Inference_Source) x
-
-(* Syntax: <num> <stuff> || <atoms> -> <atoms> . origin\(<origin>\) *)
-fun parse_pirate_line x =
-  (scan_general_id --| Scan.repeat (~$$ "|") -- parse_horn_clause --| $$ "."
-     --| Scan.this_string "origin" --| $$ "(" -- parse_pirate_source --| $$ ")"
-   >> (fn ((((num, u), source))) =>
-     let
-       val (names, rule, deps) =
-         (case source of
-           File_Source (_, SOME s) => ([s], spass_input_rule, [])
-         | Inference_Source (rule, deps) => ([], rule, deps))
-     in
-       [((num, names), Unknown, u, rule, map (rpair []) deps)]
-     end)) x
-
 fun core_inference inf fact = ((fact, [fact]), Unknown, dummy_phi, inf, [])
 
 (* Syntax: SZS core <name> ... <name> *)
@@ -674,7 +646,6 @@
 fun parse_line local_name problem =
   (* Satallax is handled separately, in "atp_satallax.ML". *)
   if local_name = spassN then parse_spass_line
-  else if local_name = pirateN then parse_pirate_line
   else if local_name = z3_tptpN then parse_z3_tptp_core_line
   else parse_tstp_line problem
 
diff -r df976eefcba0 -r 4cca14dc577c src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Fri Jul 16 14:43:25 2021 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Fri Jul 16 20:13:12 2021 +0100
@@ -482,9 +482,6 @@
 val vampire_full_proof_options =
   " --proof_extra free --forced_options avatar=off:equality_proxy=off:general_splitting=off:inequality_splitting=0:naming=0"
 
-val remote_vampire_command =
-  "vampire " ^ vampire_basic_options ^ " " ^ vampire_full_proof_options ^ " -t %d %s"
-
 val vampire_config : atp_config =
   let
     val format = TFF (Without_FOOL, Monomorphic)
@@ -663,9 +660,6 @@
 val remote_leo3 =
   remotify_atp leo3 "Leo-III" ["1.1"]
     (K (((150, ""), THF (Without_FOOL, Polymorphic, THF_Without_Choice), "poly_native_higher", keep_lamsN, false), "") (* FUDGE *))
-val remote_vampire =
-  remotify_atp vampire "Vampire" ["THF-4.4"]
-    (K (((400, ""), THF (Without_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), remote_vampire_command) (* FUDGE *))
 val remote_waldmeister = gen_remote_waldmeister waldmeisterN "raw_mono_tags??"
 val remote_zipperposition =
   remotify_atp zipperposition "Zipperpin" ["2.0"]
@@ -728,7 +722,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_vampire, remote_waldmeister, remote_zipperposition, dummy_tfx]
+   remote_waldmeister, remote_zipperposition, dummy_tfx]
 
 val _ = Theory.setup (fold add_atp atps)