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


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