--- a/NEWS Tue May 20 21:13:21 2014 +0200
+++ b/NEWS Tue May 20 22:28:08 2014 +0200
@@ -382,8 +382,12 @@
- New prover "z3_new" with support for Isar proofs
- MaSh overhaul:
- A new SML-based learning engine eliminates the dependency on Python
- and increases performance and reliability. See the Sledgehammer
- documentation for details.
+ and increases performance and reliability.
+ - Activation of MaSh now works via the "mash" system option (without
+ requiring restart), instead of former settings variable "MASH".
+ The option can be edited in Isabelle/jEdit menu Plugin
+ Options / Isabelle / General. Allowed values include "sml" (for the new
+ SML engine), "py" (for the Python engine), and "no".
- New option:
smt_proofs
- Renamed options:
--- a/src/Doc/Sledgehammer/document/root.tex Tue May 20 21:13:21 2014 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex Tue May 20 22:28:08 2014 +0200
@@ -166,10 +166,10 @@
\footnote{Vampire's and Yices's licenses prevent us from doing the same for
these otherwise remarkable tools.}
For Z3, you must additionally set the variable
-\texttt{Z3\_NON\_COMMERCIAL} to ``yes'' to confirm that you are a
+\texttt{Z3\_NON\_COMMERCIAL} to \textit{yes} to confirm that you are a
noncommercial user---either in the environment in which Isabelle is
launched, in your \texttt{\$ISABELLE\_HOME\_USER/etc/settings} file, or
-via the ``z3\_non\_commercial'' option under ``Plugins > Plugin Options
+via the ``Z3 Non Commercial'' option under ``Plugins > Plugin Options
> Isabelle > General'' in Isabelle/jEdit.
\item[\labelitemi] Alternatively, you can download the Isabelle-aware CVC3, E,
@@ -907,10 +907,10 @@
\item[\labelitemi] \textbf{\textit{z3}:} Z3 is an SMT solver developed at
Microsoft Research \cite{z3}. To use Z3, set the environment variable
\texttt{Z3\_SOLVER} to the complete path of the executable, including the file
-name, and set \texttt{Z3\_NON\_COMMERCIAL} to ``yes'' to confirm that you are a
+name, and set \texttt{Z3\_NON\_COMMERCIAL} to \textit{yes} to confirm that you are a
noncommercial user---either in the environment in which Isabelle is
launched, in your \texttt{\$ISABELLE\_HOME\_USER/etc/settings} file, or
-via the ``z3\_non\_commercial'' option under ``Plugins > Plugin Options
+via the ``Z3 Non Commercial'' option under ``Plugins > Plugin Options
> Isabelle > General'' in Isabelle/jEdit. Sledgehammer has been tested with
versions 3.0, 3.1, 3.2, and 4.0.
@@ -918,7 +918,7 @@
are treated as a different prover by Isabelle. To use these, set the environment
variable \texttt{Z3\_NEW\_SOLVER} to the complete path of the executable,
including the file name. You also need to set \texttt{Z3\_NON\_COMMERCIAL} to
-``yes'', as described above. Sledgehammer has been tested with a pre-release
+\textit{yes}, as described above. Sledgehammer has been tested with a pre-release
version of 4.3.2.
\end{enum}
@@ -1067,19 +1067,27 @@
The traditional memoryless MePo relevance filter.
\item[\labelitemi] \textbf{\textit{mash}:}
-The experimental MaSh machine learner.
-Two learning engines are provided:
+The experimental MaSh machine learner. Three learning engines are provided:
\begin{enum}
-\item[\labelitemi] \emph{sml} (also called \emph{sml\_knn}) refers to a Standard ML implementation
-of $k$-nearest neighbors.
+\item[\labelitemi] \textbf{\textit{sml}} (also called
+\textbf{\textit{sml\_knn}}) is a Standard ML implementation of $k$-nearest
+neighbors.
-\item[\labelitemi] \emph{py} (also called \emph{yes}) refers to a Python implementation of naive
-Bayes. The program is included with Isabelle as \texttt{mash.py}.
+\item[\labelitemi] \textbf{\textit{sml\_nb}} is a Standard ML implementation of
+naive Bayes.
+
+\item[\labelitemi] \textbf{\textit{py}} (also called \textbf{\textit{yes}}) is a
+Python implementation of naive Bayes. The program is included with Isabelle as
+\texttt{mash.py}.
\end{enum}
-To enable MaSh, set the environment variable \texttt{MASH} to the name of the desired engine.
-Persistent data for both engines is stored in the directory \texttt{\$ISABELLE\_HOME\_USER/mash}.
+To enable MaSh, set the variable \texttt{MASH} to the name of the desired
+engine---either in the environment in which Isabelle is launched, in your
+\texttt{\$ISABELLE\_HOME\_USER/etc/settings} file, or via the ``Mash'' option
+under ``Plugins > Plugin Options > Isabelle > General'' in Isabelle/jEdit.
+Persistent data for both engines is stored in the directory
+\texttt{\$ISABELLE\_HOME\_USER/mash}.
\item[\labelitemi] \textbf{\textit{mesh}:} The MeSh filter, which combines the
rankings from MePo and MaSh.
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Tue May 20 21:13:21 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Tue May 20 22:28:08 2014 +0200
@@ -115,21 +115,23 @@
()
end
-datatype mash_flavor = MaSh_Py | MaSh_SML_KNN | MaSh_SML_NB
+datatype mash_engine = MaSh_Py | MaSh_SML_KNN | MaSh_SML_NB
-fun mash_flavor () =
- (case getenv "MASH" of
- "yes" => SOME MaSh_Py
- | "py" => SOME MaSh_Py
- | "sml" => SOME MaSh_SML_KNN
- | "sml_knn" => SOME MaSh_SML_KNN
- | "sml_nb" => SOME MaSh_SML_NB
- | _ => NONE)
+fun mash_engine () =
+ let val flag1 = Options.default_string @{system_option maSh} in
+ (case if flag1 <> "none" (* default *) then flag1 else getenv "MASH" of
+ "yes" => SOME MaSh_Py
+ | "py" => SOME MaSh_Py
+ | "sml" => SOME MaSh_SML_KNN
+ | "sml_knn" => SOME MaSh_SML_KNN
+ | "sml_nb" => SOME MaSh_SML_NB
+ | _ => NONE)
+ end
-val is_mash_enabled = is_some o mash_flavor
+val is_mash_enabled = is_some o mash_engine
fun is_mash_sml_enabled () =
- (case mash_flavor () of
+ (case mash_engine () of
SOME MaSh_SML_KNN => true
| SOME MaSh_SML_NB => true
| _ => false)
--- a/src/HOL/Tools/etc/options Tue May 20 21:13:21 2014 +0200
+++ b/src/HOL/Tools/etc/options Tue May 20 22:28:08 2014 +0200
@@ -35,3 +35,5 @@
public option z3_non_commercial : string = "unknown"
-- "status of Z3 activation for non-commercial use (yes, no, unknown)"
+public option maSh : string = "none"
+ -- "machine learning engine to use by Sledgehammer (sml, sml_knn, sml_nb, py, none)"