--- a/NEWS Fri Aug 28 13:37:06 2015 +0200
+++ b/NEWS Fri Aug 28 16:48:05 2015 +0200
@@ -193,6 +193,8 @@
cases where Sledgehammer gives a proof that does not work.
- Auto Sledgehammer now minimizes and preplays the results.
- Handle Vampire 4.0 proof output without raising exception.
+ - Eliminated "MASH" environment variable. Use the "MaSh" option in
+ Isabelle/jEdit instead. INCOMPATIBILITY.
* Nitpick:
- Removed "check_potential" and "check_genuine" options.
--- a/src/Doc/Sledgehammer/document/root.tex Fri Aug 28 13:37:06 2015 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex Fri Aug 28 16:48:05 2015 +0200
@@ -370,7 +370,7 @@
Sledgehammer heuristically selects a few hundred relevant lemmas from the
currently loaded libraries. The component that performs this selection is
-called \emph{relevance filter}.
+called \emph{relevance filter} (\S\ref{relevance-filter}).
\begin{enum}
\item[\labelitemi]
@@ -390,13 +390,10 @@
\underline{S}ledge\underline{h}ammer). It applies machine learning to the
problem of finding relevant facts.
-\item[\labelitemi] The \emph{MeSh} filter combines MePo and MaSh.
+\item[\labelitemi] The \emph{MeSh} filter combines MePo and MaSh. This is
+the default.
\end{enum}
-The default is either MePo or MeSh, depending on whether the environment
-variable \texttt{MASH} is set and what class of provers the target prover
-belongs to (\S\ref{relevance-filter}).
-
The number of facts included in a problem varies from prover to prover, since
some provers get overwhelmed more easily than others. You can show the number of
facts given using the \textit{verbose} option (\S\ref{output-format}) and the
@@ -1018,10 +1015,7 @@
default (cf.\ \textit{smart} below).
The default algorithm is \textit{nb\_knn}. The algorithm can be selected by
-setting \texttt{MASH}---either in the environment in which Isabelle is launched,
-in your
-\texttt{\$ISABELLE\_\allowbreak HOME\_\allowbreak USER/\allowbreak etc/\allowbreak settings}
-file, or via the ``MaSh'' option under ``Plugins > Plugin Options > Isabelle >
+setting the ``MaSh'' option under ``Plugins > Plugin Options > Isabelle >
General'' in Isabelle/jEdit. Persistent data for both algorithms is stored in
the directory \texttt{\$ISABELLE\_\allowbreak HOME\_\allowbreak USER/\allowbreak
mash}.
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Aug 28 13:37:06 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Aug 28 16:48:05 2015 +0200
@@ -138,20 +138,18 @@
| MaSh_NB_Ext
| MaSh_kNN_Ext
-(* TODO: eliminate "MASH" environment variable after Isabelle2014 release *)
fun mash_algorithm () =
- let val flag1 = Options.default_string @{system_option MaSh} in
- (case if flag1 <> "none" (* default *) then flag1 else getenv "MASH" of
- "yes" => SOME MaSh_NB_kNN
- | "sml" => SOME MaSh_NB_kNN
- | "nb" => SOME MaSh_NB
- | "knn" => SOME MaSh_kNN
- | "nb_knn" => SOME MaSh_NB_kNN
- | "nb_ext" => SOME MaSh_NB_Ext
- | "knn_ext" => SOME MaSh_kNN_Ext
- | "" => NONE
- | algorithm => (warning ("Unknown MaSh algorithm: " ^ quote algorithm ^ "."); NONE))
- end
+ (case Options.default_string @{system_option MaSh} of
+ "yes" => SOME MaSh_NB_kNN
+ | "sml" => SOME MaSh_NB_kNN
+ | "nb" => SOME MaSh_NB
+ | "knn" => SOME MaSh_kNN
+ | "nb_knn" => SOME MaSh_NB_kNN
+ | "nb_ext" => SOME MaSh_NB_Ext
+ | "knn_ext" => SOME MaSh_kNN_Ext
+ | "none" => NONE
+ | "" => NONE
+ | algorithm => (warning ("Unknown MaSh algorithm: " ^ quote algorithm ^ "."); NONE))
val is_mash_enabled = is_some o mash_algorithm
val the_mash_algorithm = the_default MaSh_NB_kNN o mash_algorithm