# HG changeset patch
# User blanchet
# Date 1400617688 -7200
# Node ID e5466055e94f2a42bf1e0bc14dc82f46f2cfb60a
# Parent  80ffda443738d146c84e06b27e89a53cf362d12c
added Isabelle system option 'mash'

diff -r 80ffda443738 -r e5466055e94f NEWS
--- 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:
diff -r 80ffda443738 -r e5466055e94f src/Doc/Sledgehammer/document/root.tex
--- 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.
diff -r 80ffda443738 -r e5466055e94f src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- 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)
diff -r 80ffda443738 -r e5466055e94f src/HOL/Tools/etc/options
--- 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)"