Email Gateway (Aug 22 2022 at 11:40): Email Gateway (Aug 22 2022 at 11:40):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
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:
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.
Remove "~/.isabelle/mash_state", to start afresh. Removing the file every so often means that you lose some of the learning, though.
If you are using the repository version, change 6a5a188ab3e7 addresses this issue (and c982a4cc8dc4, 44f4ffe2b210 further speed up MaSh).
Sorry for any inconvenience.
Jasmin
Last updated: Apr 26 2024 at 08:19 UTC