- MaSh and MeSh are now used by default together with the traditional
MePo (Meng-Paulson) relevance filter. To disable MaSh, set the "MaSh"
system option in Plugin Options / Isabelle / General to "none". Other
allowed values include "sml" (for the default SML engine) and "py"
(for the old Python engine).
This refers to Isabelle/fd539459a112.
Older NEWS made this possible:
- New SML-based learning engines eliminate the dependency on Python
and increase performance and reliability.
Some users have been using MaSh for quite some time now, and with the new ML
implementation, due to Cezary Kaliszyk, the residual technical issues should be
all gone.
To actually see MaSh in action, you can try calling Sledgehammer with the
verbose option, e.g. "sledgehammer [verbose]". You should then see three lists
of fact (MePo, MaSh, MeSh). If you enable spying (by setting "export
SLEDGEHAMMER_SPY=yes" in "~/.isabelle/etc/settings", and why not "export
NITPICK_SPY=yes" while at it), you will be locally collecting data about MaSh
vs. MePo that might one day be useful for data-mining.
IMPORTANT: Please let me know quickly if you run into any technical issues
connected to this. As much as I would like to have MaSh enabled in the release
version (thereby increasing Sledgehammer's success rate quite a bit), we should
thread carefully and disable it if any serious issues arise until the release.
Jasmin
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
