# HG changeset patch
# User blanchet
# Date 1572002730 -7200
# Node ID 9b69bb9c1c8d140bc416667b9be733f10f3838bb
# Parent  273fc913427b33a427bcbcf980607ebfa4b32df9
changed Satallax's setup to invoke E

diff -r 273fc913427b -r 9b69bb9c1c8d src/Doc/Sledgehammer/document/root.tex
--- a/src/Doc/Sledgehammer/document/root.tex	Wed Oct 23 16:09:24 2019 +0000
+++ b/src/Doc/Sledgehammer/document/root.tex	Fri Oct 25 13:25:30 2019 +0200
@@ -190,11 +190,12 @@
 for Alt-Ergo, set the environment variable \texttt{WHY3\_HOME} to the
 directory that contains the \texttt{why3} executable. Sledgehammer has been
 tested with AgsyHOL 1.0, Alt-Ergo 0.95.2, E 1.6 to 2.0, LEO-II 1.3.4, Leo-III
-1.1, and Satallax 2.2 to 2.7. Since the ATPs' output formats are neither
-documented nor stable, other versions might not work well with Sledgehammer.
-Ideally, you should also set \texttt{E\_VERSION}, \texttt{LEO2\_VERSION},
+1.1, and Satallax 2.7. Since the ATPs' output formats are neither documented
+nor stable, other versions might not work well with Sledgehammer. Ideally, you
+should also set \texttt{E\_VERSION}, \texttt{LEO2\_VERSION},
 \texttt{LEO3\_VERSION}, or \texttt{SATALLAX\_VERSION} to the prover's version
-number (e.g., ``2.7'').
+number (e.g., ``2.7''); this might help Sledgehammer invoke the prover
+optimally.
 
 Similarly, if you want to install CVC3, CVC4, veriT, or Z3, set the environment
 variable \texttt{CVC3\_\allowbreak SOLVER}, \texttt{CVC4\_\allowbreak SOLVER},
diff -r 273fc913427b -r 9b69bb9c1c8d src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Wed Oct 23 16:09:24 2019 +0000
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Fri Oct 25 13:25:30 2019 +0200
@@ -472,6 +472,9 @@
 val satallax_config : atp_config =
   {exec = K (["SATALLAX_HOME"], ["satallax.opt", "satallax"]),
    arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
+     (case getenv "E_HOME" of
+       "" => ""
+     | home => "-E " ^ home ^ "/eprover ") ^
      "-p tstp -t " ^ string_of_int (to_secs 1 timeout) ^ " " ^ file_name,
    proof_delims =
      [("% SZS output start Proof", "% SZS output end Proof")],