# HG changeset patch # User blanchet # Date 1572008114 -7200 # Node ID 25c1ff13dbdbd877058ebacec8abdc7bb1dc8c9c # Parent 600da8ccbe5b2eff750fdcfacdaa84a2f643a0cd removed E-SInE, a very old system by now (and SInE has been incorporated in many provers in the past decade) diff -r 600da8ccbe5b -r 25c1ff13dbdb src/Doc/Sledgehammer/document/root.tex --- a/src/Doc/Sledgehammer/document/root.tex Fri Oct 25 14:51:16 2019 +0200 +++ b/src/Doc/Sledgehammer/document/root.tex Fri Oct 25 14:55:14 2019 +0200 @@ -102,10 +102,10 @@ historical.} % The supported ATPs are AgsyHOL \cite{agsyHOL}, Alt-Ergo \cite{alt-ergo}, E -\cite{schulz-2002}, E-SInE \cite{sine}, E-ToFoF \cite{tofof}, 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}, Waldmeister \cite{waldmeister}, and +\cite{schulz-2002}, E-ToFoF \cite{tofof}, 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}, Waldmeister \cite{waldmeister}, and Zipperposition \cite{cruanes-2014}. The ATPs are run either locally or remotely via the System\-On\-TPTP web service \cite{sutcliffe-2000}. The supported SMT solvers are CVC3 \cite{cvc3}, CVC4 \cite{cvc4}, veriT @@ -147,10 +147,10 @@ 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-SInE, 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. +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. There are three main ways to install automatic provers on your machine: @@ -859,10 +859,6 @@ \item[\labelitemi] \textbf{\textit{remote\_e}:} The remote version of E runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}. -\item[\labelitemi] \textbf{\textit{remote\_e\_sine}:} E-SInE is a metaprover -developed by Kry\v stof Hoder \cite{sine} based on E. It runs on Geoff -Sutcliffe's Miami servers. - \item[\labelitemi] \textbf{\textit{remote\_e\_tofof}:} E-ToFoF is a metaprover developed by Geoff Sutcliffe \cite{tofof} based on E running on his Miami servers. This ATP supports the TPTP typed first-order format (TFF0). The @@ -897,9 +893,9 @@ runs on Geoff Sutcliffe's Miami servers. \end{enum} -By default, Sledgehammer runs a subset of CVC4, E, E-SInE, SPASS, Vampire, -veriT, and Z3 in parallel, either locally or remotely---depending on the number -of processor cores available and on which provers are actually installed. It is +By default, Sledgehammer runs a subset of CVC4, E, SPASS, Vampire, veriT, and +Z3 in parallel, either locally or remotely---depending on the number of +processor cores available and on which provers are actually installed. It is generally a good idea to run several provers in parallel. \opnodefault{prover}{string} diff -r 600da8ccbe5b -r 25c1ff13dbdb src/HOL/ATP.thy --- a/src/HOL/ATP.thy Fri Oct 25 14:51:16 2019 +0200 +++ b/src/HOL/ATP.thy Fri Oct 25 14:55:14 2019 +0200 @@ -137,6 +137,5 @@ ML_file \Tools/monomorph.ML\ ML_file \Tools/ATP/atp_problem_generate.ML\ ML_file \Tools/ATP/atp_proof_reconstruct.ML\ -ML_file \Tools/ATP/atp_systems.ML\ end diff -r 600da8ccbe5b -r 25c1ff13dbdb src/HOL/Sledgehammer.thy --- a/src/HOL/Sledgehammer.thy Fri Oct 25 14:51:16 2019 +0200 +++ b/src/HOL/Sledgehammer.thy Fri Oct 25 14:55:14 2019 +0200 @@ -16,6 +16,8 @@ lemma size_ne_size_imp_ne: "size x \ size y \ x \ y" by (erule contrapos_nn) (rule arg_cong) +ML_file \Tools/ATP/atp_systems.ML\ + ML_file \Tools/Sledgehammer/async_manager_legacy.ML\ ML_file \Tools/Sledgehammer/sledgehammer_util.ML\ ML_file \Tools/Sledgehammer/sledgehammer_fact.ML\ @@ -35,4 +37,7 @@ ML_file \Tools/Sledgehammer/sledgehammer.ML\ ML_file \Tools/Sledgehammer/sledgehammer_commands.ML\ +lemma "1 + 1 = 2" + sledgehammer [iprover, overlord, dont_minimize, dont_preplay] + end diff -r 600da8ccbe5b -r 25c1ff13dbdb src/HOL/Tools/ATP/atp_proof.ML --- a/src/HOL/Tools/ATP/atp_proof.ML Fri Oct 25 14:51:16 2019 +0200 +++ b/src/HOL/Tools/ATP/atp_proof.ML Fri Oct 25 14:55:14 2019 +0200 @@ -52,7 +52,6 @@ val eN : string val e_malesN : string val e_parN : string - val e_sineN : string val e_tofofN : string val ehohN : string val iproverN : string @@ -121,7 +120,6 @@ val eN = "e" val e_malesN = "e_males" val e_parN = "e_par" -val e_sineN = "e_sine" val e_tofofN = "e_tofof" val ehohN = "ehoh" val iproverN = "iprover" diff -r 600da8ccbe5b -r 25c1ff13dbdb src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Fri Oct 25 14:51:16 2019 +0200 +++ b/src/HOL/Tools/ATP/atp_systems.ML Fri Oct 25 14:55:14 2019 +0200 @@ -727,9 +727,6 @@ 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_e_sine = - remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Conjecture - (K (((500, ""), FOF, "mono_guards??", combsN, false), "") (* FUDGE *)) val remote_snark = remote_atp snarkN "SNARK" ["20120808r022", "20080805r029", "20080805r024"] [("refutation.", "end_refutation.")] [] Hypothesis @@ -774,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_e_sine, remote_e_tofof, remote_iprover, - remote_leo2, remote_leo3, remote_vampire, remote_snark, remote_pirate, remote_waldmeister] + z3_tptp, zipperposition, remote_agsyhol, remote_e, remote_e_tofof, remote_iprover, remote_leo2, + remote_leo3, remote_vampire, remote_snark, remote_pirate, remote_waldmeister] val _ = Theory.setup (fold add_atp atps) diff -r 600da8ccbe5b -r 25c1ff13dbdb src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Fri Oct 25 14:51:16 2019 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Fri Oct 25 14:55:14 2019 +0200 @@ -177,7 +177,7 @@ fun default_provers_param_value mode ctxt = [cvc4N] @ (if is_vampire_noncommercial_license_accepted () = SOME false then [] else [vampireN]) @ - [z3N, eN, spassN, veritN, e_sineN] + [z3N, eN, spassN, veritN] |> map_filter (remotify_prover_if_not_installed ctxt) (* In "try" mode, leave at least one thread to another slow tool (e.g. Nitpick) *) |> take (Multithreading.max_threads () - (if mode = Try then 1 else 0))