# HG changeset patch # User blanchet # Date 1572009486 -7200 # Node ID fe114eca312ebc43d0fce14ffcf37e9cb902d46e # Parent 646651bcf261d101695e7662a78e1bb9ffbf98e3 added support for repote Alt-Ergo diff -r 646651bcf261 -r fe114eca312e src/Doc/Sledgehammer/document/root.tex --- a/src/Doc/Sledgehammer/document/root.tex Fri Oct 25 15:05:03 2019 +0200 +++ b/src/Doc/Sledgehammer/document/root.tex Fri Oct 25 15:18:06 2019 +0200 @@ -101,7 +101,7 @@ \footnote{The distinction between ATPs and SMT solvers is convenient but mostly historical.} % -The supported ATPs are AgsyHOL \cite{agsyHOL}, Alt-Ergo \cite{alt-ergo}, E +The supported ATPs are agsyHOL \cite{agsyHOL}, Alt-Ergo \cite{alt-ergo}, E \cite{schulz-2002}, iProver \cite{korovin-2009}, LEO-II \cite{leo2}, Leo-III \cite{leo3}, Satallax \cite{satallax}, SNARK \cite{snark}, SPASS \cite{weidenbach-et-al-2009}, Vampire \cite{riazanov-voronkov-2002}, @@ -146,11 +146,11 @@ Sledgehammer is part of Isabelle, so you do not need to install it. However, it relies on third-party automatic provers (ATPs and SMT solvers). -Among the ATPs, AgsyHOL, Alt-Ergo, E, LEO-II, Leo-III, Satallax, SPASS, Vampire, and -Zipperposition can be run locally; in addition, AgsyHOL, E, E-ToFoF, iProver, -LEO-II, Leo-III, Satallax, SNARK, Vampire, and Waldmeister are available -remotely via System\-On\-TPTP \cite{sutcliffe-2000}. The SMT solvers CVC3, -CVC4, veriT, and Z3 can be run locally. +Among the ATPs, agsyHOL, Alt-Ergo, E, LEO-II, Leo-III, Satallax, SPASS, +Vampire, and Zipperposition can be run locally; in addition, agsyHOL, +Alt-Ergo, E, iProver, LEO-II, Leo-III, Satallax, SNARK, Vampire, and +Waldmeister are available remotely via System\-On\-TPTP \cite{sutcliffe-2000}. +The SMT solvers CVC3, CVC4, veriT, and Z3 can be run locally. There are three main ways to install automatic provers on your machine: @@ -179,7 +179,7 @@ in it. -\item[\labelitemi] If you prefer to build AgsyHOL, Alt-Ergo, E, LEO-II, +\item[\labelitemi] If you prefer to build agsyHOL, Alt-Ergo, E, LEO-II, Leo-III, or Satallax manually, set the environment variable \texttt{AGSYHOL\_HOME}, \texttt{E\_HOME}, \texttt{LEO2\_HOME}, \texttt{LEO3\_HOME}, or \texttt{SATALLAX\_HOME} @@ -188,7 +188,7 @@ \texttt{leo}, \texttt{leo3}, or \texttt{satallax} executable; 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 +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.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}, @@ -731,9 +731,9 @@ \begin{sloppy} \begin{enum} -\item[\labelitemi] \textbf{\textit{agsyhol}:} AgsyHOL is an automatic +\item[\labelitemi] \textbf{\textit{agsyhol}:} agsyHOL is an automatic higher-order prover developed by Fredrik Lindblad \cite{agsyHOL}. To use -AgsyHOL, set the environment variable \texttt{AGSYHOL\_HOME} to the directory +agsyHOL, set the environment variable \texttt{AGSYHOL\_HOME} to the directory that contains the \texttt{agsyHOL} executable. Sledgehammer has been tested with version 1.0. @@ -853,7 +853,10 @@ \begin{enum} \item[\labelitemi] \textbf{\textit{remote\_agsyhol}:} The remote version of -AgsyHOL runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}. +agsyHOL runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}. + +\item[\labelitemi] \textbf{\textit{remote\_alt\_ergo}:} The remote version of +Alt-Ergo runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}. \item[\labelitemi] \textbf{\textit{remote\_e}:} The remote version of E runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}. diff -r 646651bcf261 -r fe114eca312e src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Fri Oct 25 15:05:03 2019 +0200 +++ b/src/HOL/Tools/ATP/atp_systems.ML Fri Oct 25 15:18:06 2019 +0200 @@ -712,6 +712,9 @@ val remote_agsyhol = remotify_atp agsyhol "agsyHOL" ["1.0", "1"] (K (((60, ""), THF (Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), "") (* FUDGE *)) +val remote_alt_ergo = + remotify_atp alt_ergo "Alt-Ergo" ["0.95.2"] + (K (((250, ""), TFF Polymorphic, "poly_native", keep_lamsN, false), "") (* FUDGE *)) val remote_e = remotify_atp e "E" ["2.0", "1.9.1", "1.8"] (K (((750, ""), TFF Monomorphic, "mono_native", combsN, false), "") (* FUDGE *)) @@ -724,13 +727,13 @@ val remote_leo3 = remotify_atp leo3 "Leo-III" ["1.1"] (K (((150, ""), THF (Polymorphic, THF_Without_Choice), "poly_native_higher", keep_lamsN, false), "") (* FUDGE *)) -val remote_vampire = - remotify_atp vampire "Vampire" ["4.2", "4.1", "4.0"] - (K (((400, ""), TFF Monomorphic, "mono_native", combs_or_liftingN, false), remote_vampire_full_proof_command) (* FUDGE *)) val remote_snark = remote_atp snarkN "SNARK" ["20120808r022", "20080805r029", "20080805r024"] [("refutation.", "end_refutation.")] [] Hypothesis (K (((100, ""), TFF Monomorphic, "mono_native", liftingN, false), "") (* FUDGE *)) +val remote_vampire = + remotify_atp vampire "Vampire" ["4.2", "4.1", "4.0"] + (K (((400, ""), TFF Monomorphic, "mono_native", combs_or_liftingN, false), remote_vampire_full_proof_command) (* FUDGE *)) val remote_waldmeister = gen_remote_waldmeister waldmeisterN "raw_mono_tags??" @@ -768,8 +771,8 @@ val atps = [agsyhol, alt_ergo, e, e_males, e_par, ehoh, iprover, leo2, leo3, satallax, spass, vampire, - z3_tptp, zipperposition, remote_agsyhol, remote_e, remote_iprover, remote_leo2, remote_leo3, - remote_vampire, remote_snark, remote_pirate, remote_waldmeister] + 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)