412 and it cannot learn. |
412 and it cannot learn. |
413 |
413 |
414 \item[\labelitemi] |
414 \item[\labelitemi] |
415 An experimental, memoryful alternative to MePo is \emph{MaSh} |
415 An experimental, memoryful alternative to MePo is \emph{MaSh} |
416 (\underline{Ma}chine Learner for \underline{S}ledge\underline{h}ammer). It |
416 (\underline{Ma}chine Learner for \underline{S}ledge\underline{h}ammer). It |
417 relies on an external tool called \texttt{mash} that applies machine learning to |
417 relies on an external Python tool that applies machine learning to |
418 the problem of finding relevant facts. |
418 the problem of finding relevant facts. |
419 |
419 |
420 \item[\labelitemi] The \emph{Mesh} filter combines MePo and MaSh. |
420 \item[\labelitemi] The \emph{Mesh} filter combines MePo and MaSh. |
421 \end{enum} |
421 \end{enum} |
422 |
422 |
423 The default is either MePo or Mesh, depending on whether \texttt{mash} is |
423 The default is either MePo or Mesh, depending on whether the environment |
424 installed and what class of provers the target prover belongs to |
424 variable \texttt{MASH} is set and what class of provers the target prover |
425 (\S\ref{relevance-filter}). |
425 belongs to (\S\ref{relevance-filter}). |
426 |
426 |
427 The number of facts included in a problem varies from prover to prover, since |
427 The number of facts included in a problem varies from prover to prover, since |
428 some provers get overwhelmed more easily than others. You can show the number of |
428 some provers get overwhelmed more easily than others. You can show the number of |
429 facts given using the \textit{verbose} option (\S\ref{output-format}) and the |
429 facts given using the \textit{verbose} option (\S\ref{output-format}) and the |
430 actual facts using \textit{debug} (\S\ref{output-format}). |
430 actual facts using \textit{debug} (\S\ref{output-format}). |
1053 \begin{enum} |
1053 \begin{enum} |
1054 \item[\labelitemi] \textbf{\textit{mepo}:} |
1054 \item[\labelitemi] \textbf{\textit{mepo}:} |
1055 The traditional memoryless MePo relevance filter. |
1055 The traditional memoryless MePo relevance filter. |
1056 |
1056 |
1057 \item[\labelitemi] \textbf{\textit{mash}:} |
1057 \item[\labelitemi] \textbf{\textit{mash}:} |
1058 The memoryful MaSh machine learner. MaSh relies on the external program |
1058 The memoryful MaSh machine learner. MaSh relies on the external Python program |
1059 \texttt{mash}, which can be obtained from the author at \authoremail. To install |
1059 \texttt{mash.py}, which is part of Isabelle. To enable MaSh, set the environment |
1060 it, set the environment variable \texttt{MASH\_HOME} to the directory that |
1060 variable \texttt{MASH} to \texttt{yes}. Persistent data is stored in the |
1061 contains the \texttt{mash} executable. |
1061 directory \texttt{\$ISABELLE\_HOME\_USER/mash}. |
1062 Persistent data is stored in the \texttt{\$ISABELLE\_HOME\_USER/mash} directory. |
|
1063 |
1062 |
1064 \item[\labelitemi] \textbf{\textit{mesh}:} A combination of MePo and MaSh. |
1063 \item[\labelitemi] \textbf{\textit{mesh}:} A combination of MePo and MaSh. |
1065 |
1064 |
1066 \item[\labelitemi] \textbf{\textit{smart}:} Use Mesh if \texttt{mash} is |
1065 \item[\labelitemi] \textbf{\textit{smart}:} Use Mesh if MaSh is |
1067 installed and the target prover is an ATP; otherwise, use MePo. |
1066 enabled and the target prover is an ATP; otherwise, use MePo. |
1068 \end{enum} |
1067 \end{enum} |
1069 |
1068 |
1070 \opdefault{max\_facts}{smart\_int}{smart} |
1069 \opdefault{max\_facts}{smart\_int}{smart} |
1071 Specifies the maximum number of facts that may be returned by the relevance |
1070 Specifies the maximum number of facts that may be returned by the relevance |
1072 filter. If the option is set to \textit{smart}, it is set to a value that was |
1071 filter. If the option is set to \textit{smart}, it is set to a value that was |
1082 are relevant and 1 only theorems that refer to previously seen constants. |
1081 are relevant and 1 only theorems that refer to previously seen constants. |
1083 |
1082 |
1084 \optrue{learn}{dont\_learn} |
1083 \optrue{learn}{dont\_learn} |
1085 Specifies whether MaSh should be run automatically by Sledgehammer to learn the |
1084 Specifies whether MaSh should be run automatically by Sledgehammer to learn the |
1086 available theories (and hence provide more accurate results). Learning only |
1085 available theories (and hence provide more accurate results). Learning only |
1087 takes place if \texttt{mash} is installed. |
1086 takes place if MaSh is enabled. |
1088 |
1087 |
1089 \opdefault{max\_new\_mono\_instances}{int}{smart} |
1088 \opdefault{max\_new\_mono\_instances}{int}{smart} |
1090 Specifies the maximum number of monomorphic instances to generate beyond |
1089 Specifies the maximum number of monomorphic instances to generate beyond |
1091 \textit{max\_facts}. The higher this limit is, the more monomorphic instances |
1090 \textit{max\_facts}. The higher this limit is, the more monomorphic instances |
1092 are potentially generated. Whether monomorphization takes place depends on the |
1091 are potentially generated. Whether monomorphization takes place depends on the |