Email Gateway (Aug 22 2022 at 12:20): Email Gateway (Aug 22 2022 at 12:20):From: Lars Hupel <hupel@in.tum.de>
(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.
Cheers
Lars
Screenshot_20160128_151205.png
Screenshot_20160128_151254.png
Email Gateway (Aug 22 2022 at 12:22):From: Makarius <makarius@sketis.net>
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]]
begin
lemma "(∃x. P x) ∨ Q ≡ ∃x. P x ∨ Q"
quickcheck
by auto
end
Here quickcheck will not see that option, and not produce unwanted traces.
This can already serve as practical workaround for Isabelle2015 and
Isabelle2016.
Further efforts to localize quickcheck should follow after the release.
Makarius
Last updated: Apr 18 2024 at 08:19 UTC