added Isabelle system option 'mash'
authorblanchet
Tue May 20 22:28:08 2014 +0200 (2014-05-20)
changeset 57028e5466055e94f
parent 57027 80ffda443738
child 57029 75cc30d2b83f
added Isabelle system option 'mash'
NEWS
src/Doc/Sledgehammer/document/root.tex
src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
src/HOL/Tools/etc/options
     1.1 --- a/NEWS	Tue May 20 21:13:21 2014 +0200
     1.2 +++ b/NEWS	Tue May 20 22:28:08 2014 +0200
     1.3 @@ -382,8 +382,12 @@
     1.4    - New prover "z3_new" with support for Isar proofs
     1.5    - MaSh overhaul:
     1.6        - A new SML-based learning engine eliminates the dependency on Python
     1.7 -        and increases performance and reliability. See the Sledgehammer
     1.8 -        documentation for details.
     1.9 +        and increases performance and reliability.
    1.10 +      - Activation of MaSh now works via the "mash" system option (without
    1.11 +        requiring restart), instead of former settings variable "MASH".
    1.12 +        The option can be edited in Isabelle/jEdit menu Plugin
    1.13 +        Options / Isabelle / General. Allowed values include "sml" (for the new
    1.14 +        SML engine), "py" (for the Python engine), and "no".
    1.15    - New option:
    1.16        smt_proofs
    1.17    - Renamed options:
     2.1 --- a/src/Doc/Sledgehammer/document/root.tex	Tue May 20 21:13:21 2014 +0200
     2.2 +++ b/src/Doc/Sledgehammer/document/root.tex	Tue May 20 22:28:08 2014 +0200
     2.3 @@ -166,10 +166,10 @@
     2.4  \footnote{Vampire's and Yices's licenses prevent us from doing the same for
     2.5  these otherwise remarkable tools.}
     2.6  For Z3, you must additionally set the variable
     2.7 -\texttt{Z3\_NON\_COMMERCIAL} to ``yes'' to confirm that you are a
     2.8 +\texttt{Z3\_NON\_COMMERCIAL} to \textit{yes} to confirm that you are a
     2.9  noncommercial user---either in the environment in which Isabelle is
    2.10  launched, in your \texttt{\$ISABELLE\_HOME\_USER/etc/settings} file, or
    2.11 -via the ``z3\_non\_commercial'' option under ``Plugins > Plugin Options
    2.12 +via the ``Z3 Non Commercial'' option under ``Plugins > Plugin Options
    2.13  > Isabelle > General'' in Isabelle/jEdit.
    2.14  
    2.15  \item[\labelitemi] Alternatively, you can download the Isabelle-aware CVC3, E,
    2.16 @@ -907,10 +907,10 @@
    2.17  \item[\labelitemi] \textbf{\textit{z3}:} Z3 is an SMT solver developed at
    2.18  Microsoft Research \cite{z3}. To use Z3, set the environment variable
    2.19  \texttt{Z3\_SOLVER} to the complete path of the executable, including the file
    2.20 -name, and set \texttt{Z3\_NON\_COMMERCIAL} to ``yes'' to confirm that you are a
    2.21 +name, and set \texttt{Z3\_NON\_COMMERCIAL} to \textit{yes} to confirm that you are a
    2.22  noncommercial user---either in the environment in which Isabelle is
    2.23  launched, in your \texttt{\$ISABELLE\_HOME\_USER/etc/settings} file, or
    2.24 -via the ``z3\_non\_commercial'' option under ``Plugins > Plugin Options
    2.25 +via the ``Z3 Non Commercial'' option under ``Plugins > Plugin Options
    2.26  > Isabelle > General'' in Isabelle/jEdit. Sledgehammer has been tested with
    2.27  versions 3.0, 3.1, 3.2, and 4.0.
    2.28  
    2.29 @@ -918,7 +918,7 @@
    2.30  are treated as a different prover by Isabelle. To use these, set the environment
    2.31  variable \texttt{Z3\_NEW\_SOLVER} to the complete path of the executable,
    2.32  including the file name. You also need to set \texttt{Z3\_NON\_COMMERCIAL} to
    2.33 -``yes'', as described above. Sledgehammer has been tested with a pre-release
    2.34 +\textit{yes}, as described above. Sledgehammer has been tested with a pre-release
    2.35  version of 4.3.2.
    2.36  \end{enum}
    2.37  
    2.38 @@ -1067,19 +1067,27 @@
    2.39  The traditional memoryless MePo relevance filter.
    2.40  
    2.41  \item[\labelitemi] \textbf{\textit{mash}:}
    2.42 -The experimental MaSh machine learner.
    2.43 -Two learning engines are provided:
    2.44 +The experimental MaSh machine learner. Three learning engines are provided:
    2.45  
    2.46  \begin{enum}
    2.47 -\item[\labelitemi] \emph{sml} (also called \emph{sml\_knn}) refers to a Standard ML implementation
    2.48 -of $k$-nearest neighbors.
    2.49 +\item[\labelitemi] \textbf{\textit{sml}} (also called
    2.50 +\textbf{\textit{sml\_knn}}) is a Standard ML implementation of $k$-nearest
    2.51 +neighbors.
    2.52  
    2.53 -\item[\labelitemi] \emph{py} (also called \emph{yes}) refers to a Python implementation of naive
    2.54 -Bayes. The program is included with Isabelle as \texttt{mash.py}.
    2.55 +\item[\labelitemi] \textbf{\textit{sml\_nb}} is a Standard ML implementation of
    2.56 +naive Bayes.
    2.57 +
    2.58 +\item[\labelitemi] \textbf{\textit{py}} (also called \textbf{\textit{yes}}) is a
    2.59 +Python implementation of naive Bayes. The program is included with Isabelle as
    2.60 +\texttt{mash.py}.
    2.61  \end{enum}
    2.62  
    2.63 -To enable MaSh, set the environment variable \texttt{MASH} to the name of the desired engine.
    2.64 -Persistent data for both engines is stored in the directory \texttt{\$ISABELLE\_HOME\_USER/mash}.
    2.65 +To enable MaSh, set the variable \texttt{MASH} to the name of the desired
    2.66 +engine---either in the environment in which Isabelle is launched, in your
    2.67 +\texttt{\$ISABELLE\_HOME\_USER/etc/settings} file, or via the ``Mash'' option
    2.68 +under ``Plugins > Plugin Options > Isabelle > General'' in Isabelle/jEdit.
    2.69 +Persistent data for both engines is stored in the directory
    2.70 +\texttt{\$ISABELLE\_HOME\_USER/mash}.
    2.71  
    2.72  \item[\labelitemi] \textbf{\textit{mesh}:} The MeSh filter, which combines the
    2.73  rankings from MePo and MaSh.
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Tue May 20 21:13:21 2014 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Tue May 20 22:28:08 2014 +0200
     3.3 @@ -115,21 +115,23 @@
     3.4      ()
     3.5    end
     3.6  
     3.7 -datatype mash_flavor = MaSh_Py | MaSh_SML_KNN | MaSh_SML_NB
     3.8 +datatype mash_engine = MaSh_Py | MaSh_SML_KNN | MaSh_SML_NB
     3.9  
    3.10 -fun mash_flavor () =
    3.11 -  (case getenv "MASH" of
    3.12 -    "yes" => SOME MaSh_Py
    3.13 -  | "py" => SOME MaSh_Py
    3.14 -  | "sml" => SOME MaSh_SML_KNN
    3.15 -  | "sml_knn" => SOME MaSh_SML_KNN
    3.16 -  | "sml_nb" => SOME MaSh_SML_NB
    3.17 -  | _ => NONE)
    3.18 +fun mash_engine () =
    3.19 +  let val flag1 = Options.default_string @{system_option maSh} in
    3.20 +    (case if flag1 <> "none" (* default *) then flag1 else getenv "MASH" of
    3.21 +      "yes" => SOME MaSh_Py
    3.22 +    | "py" => SOME MaSh_Py
    3.23 +    | "sml" => SOME MaSh_SML_KNN
    3.24 +    | "sml_knn" => SOME MaSh_SML_KNN
    3.25 +    | "sml_nb" => SOME MaSh_SML_NB
    3.26 +    | _ => NONE)
    3.27 +  end
    3.28  
    3.29 -val is_mash_enabled = is_some o mash_flavor
    3.30 +val is_mash_enabled = is_some o mash_engine
    3.31  
    3.32  fun is_mash_sml_enabled () =
    3.33 -  (case mash_flavor () of
    3.34 +  (case mash_engine () of
    3.35      SOME MaSh_SML_KNN => true
    3.36    | SOME MaSh_SML_NB => true
    3.37    | _ => false)
     4.1 --- a/src/HOL/Tools/etc/options	Tue May 20 21:13:21 2014 +0200
     4.2 +++ b/src/HOL/Tools/etc/options	Tue May 20 22:28:08 2014 +0200
     4.3 @@ -35,3 +35,5 @@
     4.4  public option z3_non_commercial : string = "unknown"
     4.5    -- "status of Z3 activation for non-commercial use (yes, no, unknown)"
     4.6  
     4.7 +public option maSh : string = "none"
     4.8 +  -- "machine learning engine to use by Sledgehammer (sml, sml_knn, sml_nb, py, none)"