Re: [isabelle] Isabelle2016-RC2: bogus simplifier trace messages
On Thu, 28 Jan 2016, Lars Hupel wrote:
(This problem is present in Isabelle2015, too.)
I've attached a screenshot of the behaviour. The second screenshot is
the trace shown after clicking on one of the messages.
The trace clearly shows traces of quickcheck. This conjecture can be
verified by disabling auto quickcheck in Isabelle/jEdit plugin options and
using the 'quickcheck' command explicitly.
I've made some attempts to let quickcheck disable the simplifier trace
(both old and new) before doing its own business, but did not get to the
bottom of it. It seems that quickcheck is not properly localized: it does
not observe local context options.
E.g. try this instead of a global "declare [[simp_trace_new]]":
context notes [[simp_trace_new]]
lemma "(âx. P x) â Q â âx. P x â Q"
Here quickcheck will not see that option, and not produce unwanted traces.
This can already serve as practical workaround for Isabelle2015 and
Further efforts to localize quickcheck should follow after the release.
This archive was generated by a fusion of
Pipermail (Mailman edition) and