# HG changeset patch
# User blanchet
# Date 1572009794 -7200
# Node ID 6d84c3c333d5e2f9efc2710d1bae0a4f646d71a9
# Parent  fe114eca312ebc43d0fce14ffcf37e9cb902d46e
removed support for old system E-MaLeS

diff -r fe114eca312e -r 6d84c3c333d5 src/Doc/Sledgehammer/document/root.tex
--- a/src/Doc/Sledgehammer/document/root.tex	Fri Oct 25 15:18:06 2019 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex	Fri Oct 25 15:23:14 2019 +0200
@@ -763,12 +763,6 @@
 install the prebuilt E package from \download. Sledgehammer has been tested with
 versions 1.6 to 1.8.
 
-\item[\labelitemi] \textbf{\textit{e\_males}:} E-MaLeS is a metaprover developed
-by Daniel K\"uhlwein that implements strategy scheduling on top of E. To use
-E-MaLeS, set the environment variable \texttt{E\_MALES\_HOME} to the directory
-that contains the \texttt{emales.py} script. Sledgehammer has been tested with
-version 1.1.
-
 \item[\labelitemi] \textbf{\textit{e\_par}:} E-Par is an experimental metaprover
 developed by Josef Urban that implements strategy scheduling on top of E. To use
 E-Par, set the environment variable \texttt{E\_HOME} to the directory that
diff -r fe114eca312e -r 6d84c3c333d5 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Fri Oct 25 15:18:06 2019 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Fri Oct 25 15:23:14 2019 +0200
@@ -47,10 +47,7 @@
   (* Named ATPs *)
   val agsyholN : string
   val alt_ergoN : string
-  val dummy_thfN : string
-  val dummy_thf_mlN : string
   val eN : string
-  val e_malesN : string
   val e_parN : string
   val ehohN : string
   val iproverN : string
@@ -114,10 +111,7 @@
 
 val agsyholN = "agsyhol"
 val alt_ergoN = "alt_ergo"
-val dummy_thfN = "dummy_thf" (* for experiments *)
-val dummy_thf_mlN = "dummy_thf_ml" (* for experiments *)
 val eN = "e"
-val e_malesN = "e_males"
 val e_parN = "e_par"
 val ehohN = "ehoh"
 val iproverN = "iprover"
diff -r fe114eca312e -r 6d84c3c333d5 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Fri Oct 25 15:18:06 2019 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Fri Oct 25 15:23:14 2019 +0200
@@ -311,12 +311,12 @@
 val e = (eN, fn () => e_config)
 
 
-(* E-MaLeS *)
+(* E-Par *)
 
-val e_males_config : atp_config =
-  {exec = K (["E_MALES_HOME"], ["emales.py"]),
+val e_par_config : atp_config =
+  {exec = K (["E_HOME"], ["runepar.pl"]),
    arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
-     "-t " ^ string_of_int (to_secs 1 timeout) ^ " -p " ^ file_name,
+     string_of_int (to_secs 1 timeout) ^ " 1 " (* SInE *) ^ file_name ^ " 2" (* proofs *),
    proof_delims = tstp_proof_delims,
    known_failures = #known_failures e_config,
    prem_role = Conjecture,
@@ -329,22 +329,6 @@
    best_max_mono_iters = default_max_mono_iters,
    best_max_new_mono_instances = default_max_new_mono_instances}
 
-val e_males = (e_malesN, fn () => e_males_config)
-
-
-(* E-Par *)
-
-val e_par_config : atp_config =
-  {exec = K (["E_HOME"], ["runepar.pl"]),
-   arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
-     string_of_int (to_secs 1 timeout) ^ " 1 " (* SInE *) ^ file_name ^ " 2" (* proofs *),
-   proof_delims = tstp_proof_delims,
-   known_failures = #known_failures e_config,
-   prem_role = Conjecture,
-   best_slices = #best_slices e_males_config,
-   best_max_mono_iters = default_max_mono_iters,
-   best_max_new_mono_instances = default_max_new_mono_instances}
-
 val e_par = (e_parN, fn () => e_par_config)
 
 
@@ -770,9 +754,9 @@
   end
 
 val atps =
-  [agsyhol, alt_ergo, e, e_males, e_par, ehoh, 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_snark, remote_pirate, remote_waldmeister]
+  [agsyhol, alt_ergo, e, e_par, ehoh, 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_snark, remote_pirate, remote_waldmeister]
 
 val _ = Theory.setup (fold add_atp atps)