[isabelle] Sledgehammer/MaSh slowdown



Dear users,

Sledgehammer's machine-learning-based relevance filter, MaSh, accumulates data on disk in "~/.isabelle/mash_state". Over time, some users have experienced some noticeable slowdowns as this data grows.

Here's how to find out if you are affected. If you write

    sledgehammer [verbose, fact_filter = mash]

and it takes more than a couple of seconds (ideally ~200 ms) before Sledgehammer prints the 1000-or-so selected facts, whereas

    sledgehammer [verbose, fact_filter = mepo]

does it almost instantaneously, it means you are a victim of this issue. Three solutions:

1. Disable MaSh. This can be done through the Isabelle/jEdit options. See "isabelle doc sledgehammer" for details. Alternative: add "sledgehammer_params [fact_filter = mepo]" in your preamble.

2. Remove "~/.isabelle/mash_state", to start afresh. Removing the file every so often means that you lose some of the learning, though.

3. If you are using the repository version, change 6a5a188ab3e7 addresses this issue (and c982a4cc8dc4, 44f4ffe2b210 further speed up MaSh).

Sorry for any inconvenience.

Jasmin





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.