[isabelle-dev] NEWS: enabled MaSh by default

Jasmin Christian Blanchette jasmin.blanchette at gmail.com
Wed Jun 18 13:37:03 CEST 2014

      - 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.


More information about the isabelle-dev mailing list