# 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")],