[isabelle] Localization of code generator (and thus quickcheck)



This is a continuation of the thread "bogus simplifier trace messages"
from isabelle-users (Jan-2016).

On 29/01/16 17:07, Makarius wrote:

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

After the release, I've made the following change:

changeset:   62980:ba9072b303a2
user:        wenzelm
date:        Thu Apr 14 16:59:47 2016 +0200
files:       src/Pure/Tools/simplifier_trace.ML src/Tools/quickcheck.ML
description:
avoid misleading Simplifier trace in quickcheck, notably in auto quickcheck;


That is not suffient, though. Spurious traces remain. The attached
experimental setup (ch-test and Test.thy) helps to find the place where
it happens. To make this work, Pure + HOL need to be build with debugger
information:

  isabelle build -c -b -o ML_debugger Pure HOL

This takes approx. 25min on my machine (the exclusion of Complex_Main
helps a lot).

The included trace1 and trace2 show the situation before and after the
following change:

changeset:   63072:413184c7a2a2
user:        wenzelm
date:        Mon May 09 14:37:47 2016 +0200
files:       src/Doc/more_antiquote.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML
src/HOL/Tools/Predicate_Compile/predicate_compile.ML
src/HOL/Tools/record.ML src/Pure/Isar/code.ML src/Pure/axclass.ML
src/Tools/Code/code_preproc.ML src/Tools/Code/code_thingol.ML
description:
clarified context, notably for internal use of Simplifier;


The codegen setup has quite a few uses Proof_Context.init_global left:
that seems to be required for a hard reset of the logical context
(fixes, sorts of type variables etc.), but it disrupts the use of
options in the context to control other tools (notably the Simplifier).

Is there a chance to make the code generator fully context-conformant?


    Makarius



# HG changeset patch
# User wenzelm
# Date 1462803847 -7200
#      Mon May 09 16:24:07 2016 +0200
# Node ID 2aec5467cd04c33ce7f6e52c3c0ded440713c819
# Parent  413184c7a2a270046279ca6dd9275a7bee4b763c
test

diff -r 413184c7a2a2 -r 2aec5467cd04 src/HOL/ROOT
--- a/src/HOL/ROOT	Mon May 09 14:37:47 2016 +0200
+++ b/src/HOL/ROOT	Mon May 09 16:24:07 2016 +0200
@@ -6,7 +6,6 @@
   *}
   global_theories
     Main
-    Complex_Main
   files
     "Tools/Quickcheck/Narrowing_Engine.hs"
     "Tools/Quickcheck/PNF_Narrowing_Engine.hs"
diff -r 413184c7a2a2 -r 2aec5467cd04 src/Pure/Tools/simplifier_trace.ML
--- a/src/Pure/Tools/simplifier_trace.ML	Mon May 09 14:37:47 2016 +0200
+++ b/src/Pure/Tools/simplifier_trace.ML	Mon May 09 16:24:07 2016 +0200
@@ -307,7 +307,7 @@
     (case mk_generic_result Markup.simp_trace_recurseN text true payload ctxt of
       NONE => put 0
     | SOME res =>
-       (if depth = 1 then writeln (see_panel ()) else ();
+       (if depth = 1 then (raise Fail "FIXME"; writeln (see_panel ())) else ();
         output_result res;
         put (#1 res)))
   end
theory Test
imports Main
begin

declare [[simp_trace_new, ML_exception_debugger]]

lemma "(\<exists>x. P x) \<or> Q \<equiv> \<exists>x. P x \<or> Q"
  quickcheck [tester = random]
  oops

end
Exception trace - exception Fail raised (line 310 of "Tools/simplifier_trace.ML")
  Simplifier_Trace.recurse (line 291 of "Tools/simplifier_trace.ML")
  Raw_Simplifier.trace_invoke (line 821 of "raw_simplifier.ML")
  Raw_Simplifier.rewrite_cterm(4)ctxt-(1) (line 1305 of "raw_simplifier.ML")
  Raw_Simplifier.rewrite_cterm (line 1292 of "raw_simplifier.ML")
  Code_Preproc.trans_conv_rule (line 123 of "~~/src/Tools/Code/code_preproc.ML")
  Code_Preproc.Sandwich.lift (line 141 of "~~/src/Tools/Code/code_preproc.ML")
  Code_Preproc.Sandwich.evaluation (line 154 of "~~/src/Tools/Code/code_preproc.ML")
  Code_Runtime.dynamic_value_exn (line 125 of "~~/src/Tools/Code/code_runtime.ML")
  Code_Runtime.dynamic_value_strict (line 135 of "~~/src/Tools/Code/code_runtime.ML")
  Random_Generators.compile_generator_expr_raw (line 413 of "~~/src/HOL/Tools/Quickcheck/random_generators.ML")
  Random_Generators.compile_generator_expr (line 464 of "~~/src/HOL/Tools/Quickcheck/random_generators.ML")
  Quickcheck_Common.test_term_with_cardinality(5)comp_time|test_fun-(1) (line 176 of "~~/src/HOL/Tools/Quickcheck/quickcheck_common.ML")
  Timing.timing (line 68 of "General/timing.ML")
  Quickcheck_Common.cpu_time (line 84 of "~~/src/HOL/Tools/Quickcheck/quickcheck_common.ML")
  Quickcheck_Common.test_term_with_cardinality (line 149 of "~~/src/HOL/Tools/Quickcheck/quickcheck_common.ML")
  Quickcheck_Common.generator_test_goal_terms(5)test_term' (line 340 of "~~/src/HOL/Tools/Quickcheck/quickcheck_common.ML")
  Quickcheck_Common.collect_results (line 325 of "~~/src/HOL/Tools/Quickcheck/quickcheck_common.ML")
  Quickcheck_Common.generator_test_goal_terms (line 332 of "~~/src/HOL/Tools/Quickcheck/quickcheck_common.ML")
  Quickcheck.test_terms(5)(1)(1) (line 303 of "~~/src/Tools/quickcheck.ML")
  Par_List.get_some(2)results-(1) (line 61 of "Concurrent/par_list.ML")
  Par_Exn.release_first (line 73 of "Concurrent/par_exn.ML")
  Par_List.get_some (line 56 of "Concurrent/par_list.ML")
  Quickcheck.test_terms(5)(1) (line 302 of "~~/src/Tools/quickcheck.ML")
  Timeout.apply(3)(1)result-(1)(1) (line 29 of "Concurrent/timeout.ML")
  Timeout.apply(3)(1)result-(1) (line 29 of "Concurrent/timeout.ML")
  Timeout.apply(3)(1) (line 20 of "Concurrent/timeout.ML")
  Timeout.apply (line 19 of "Concurrent/timeout.ML")
  Quickcheck.limit (line 283 of "~~/src/Tools/quickcheck.ML")
  Quickcheck.test_terms (line 296 of "~~/src/Tools/quickcheck.ML")
  Quickcheck.test_goal (line 341 of "~~/src/Tools/quickcheck.ML")
  Quickcheck.gen_quickcheck(3)(2) (line 508 of "~~/src/Tools/quickcheck.ML")
  Quickcheck.gen_quickcheck (line 503 of "~~/src/Tools/quickcheck.ML")
  Quickcheck.quickcheck_cmd (line 516 of "~~/src/Tools/quickcheck.ML")
  Toplevel.keep_proof(1)(1) (line 347 of "Isar/toplevel.ML")
  Toplevel.apply_tr(3)(1) (line 263 of "Isar/toplevel.ML") 
Exception trace - exception Fail raised (line 310 of "Tools/simplifier_trace.ML")
  Simplifier_Trace.recurse (line 291 of "Tools/simplifier_trace.ML")
  Raw_Simplifier.trace_invoke (line 821 of "raw_simplifier.ML")
  Raw_Simplifier.rewrite_cterm(4)ctxt-(1) (line 1305 of "raw_simplifier.ML")
  Raw_Simplifier.rewrite_cterm (line 1292 of "raw_simplifier.ML")
  Code_Thingol.ensure_inst(6)translate_classparam_instance (line 573 of "~~/src/Tools/Code/code_thingol.ML")
  Library.curry (line 228 of "library.ML")
  Code_Thingol.ensure_stmt (line 368 of "~~/src/Tools/Code/code_thingol.ML")
  Code_Thingol.translate_const (line 633 of "~~/src/Tools/Code/code_thingol.ML")
  Code_Thingol.maybe_permissive (line 410 of "~~/src/Tools/Code/code_thingol.ML")
  Library.curry (line 228 of "library.ML")
  Code_Thingol.ensure_stmt (line 368 of "~~/src/Tools/Code/code_thingol.ML")
  Code_Thingol.translate_const (line 633 of "~~/src/Tools/Code/code_thingol.ML")
  Code_Thingol.maybe_permissive (line 410 of "~~/src/Tools/Code/code_thingol.ML")
  Library.curry (line 228 of "library.ML")
  Code_Thingol.ensure_stmt (line 368 of "~~/src/Tools/Code/code_thingol.ML")
  Code_Thingol.translate_const (line 633 of "~~/src/Tools/Code/code_thingol.ML")
  Code_Thingol.maybe_permissive (line 410 of "~~/src/Tools/Code/code_thingol.ML")
  Library.curry (line 228 of "library.ML")
  Code_Thingol.ensure_stmt (line 368 of "~~/src/Tools/Code/code_thingol.ML")
  Code_Thingol.translate_const (line 633 of "~~/src/Tools/Code/code_thingol.ML")
  Code_Thingol.maybe_permissive (line 410 of "~~/src/Tools/Code/code_thingol.ML")
  Library.curry (line 228 of "library.ML")
  Code_Thingol.ensure_stmt (line 368 of "~~/src/Tools/Code/code_thingol.ML")
  Code_Thingol.translate_const (line 633 of "~~/src/Tools/Code/code_thingol.ML")
  Library.curry (line 228 of "library.ML")
  Code_Thingol.ensure_stmt (line 368 of "~~/src/Tools/Code/code_thingol.ML")
  Code_Thingol.invoke_generation(6)(1) (line 784 of "~~/src/Tools/Code/code_thingol.ML")
  Code.change_yield_data (line 337 of "Isar/code.ML")
  Code_Data().change_yield (line 1339 of "Isar/code.ML")
  Code_Thingol.invoke_generation (line 782 of "~~/src/Tools/Code/code_thingol.ML")
  Code_Thingol.dynamic_evaluator (line 845 of "~~/src/Tools/Code/code_thingol.ML")
  Code_Preproc.dynamic_evaluator (line 545 of "~~/src/Tools/Code/code_preproc.ML")
  Code_Preproc.Sandwich.evaluation (line 154 of "~~/src/Tools/Code/code_preproc.ML")
  Code_Runtime.dynamic_value_exn (line 125 of "~~/src/Tools/Code/code_runtime.ML")
  Code_Runtime.dynamic_value_strict (line 135 of "~~/src/Tools/Code/code_runtime.ML")
  Random_Generators.compile_generator_expr_raw (line 413 of "~~/src/HOL/Tools/Quickcheck/random_generators.ML")
  Random_Generators.compile_generator_expr (line 464 of "~~/src/HOL/Tools/Quickcheck/random_generators.ML")
  Quickcheck_Common.test_term_with_cardinality(5)comp_time|test_fun-(1) (line 176 of "~~/src/HOL/Tools/Quickcheck/quickcheck_common.ML")
  Timing.timing (line 68 of "General/timing.ML")
  Quickcheck_Common.cpu_time (line 84 of "~~/src/HOL/Tools/Quickcheck/quickcheck_common.ML")
  Quickcheck_Common.test_term_with_cardinality (line 149 of "~~/src/HOL/Tools/Quickcheck/quickcheck_common.ML")
  Quickcheck_Common.generator_test_goal_terms(5)test_term' (line 340 of "~~/src/HOL/Tools/Quickcheck/quickcheck_common.ML")
  Quickcheck_Common.collect_results (line 325 of "~~/src/HOL/Tools/Quickcheck/quickcheck_common.ML")
  Quickcheck_Common.generator_test_goal_terms (line 332 of "~~/src/HOL/Tools/Quickcheck/quickcheck_common.ML")
  Quickcheck.test_terms(5)(1)(1) (line 303 of "~~/src/Tools/quickcheck.ML")
  Par_List.get_some(2)results-(1) (line 61 of "Concurrent/par_list.ML")
  Par_Exn.release_first (line 73 of "Concurrent/par_exn.ML")
  Par_List.get_some (line 56 of "Concurrent/par_list.ML")
  Quickcheck.test_terms(5)(1) (line 302 of "~~/src/Tools/quickcheck.ML")
  Timeout.apply(3)(1)result-(1)(1) (line 29 of "Concurrent/timeout.ML")
  Timeout.apply(3)(1)result-(1) (line 29 of "Concurrent/timeout.ML")
  Timeout.apply(3)(1) (line 20 of "Concurrent/timeout.ML")
  Timeout.apply (line 19 of "Concurrent/timeout.ML")
  Quickcheck.limit (line 283 of "~~/src/Tools/quickcheck.ML")
  Quickcheck.test_terms (line 296 of "~~/src/Tools/quickcheck.ML")
  Quickcheck.test_goal (line 341 of "~~/src/Tools/quickcheck.ML")
  Quickcheck.gen_quickcheck(3)(2) (line 508 of "~~/src/Tools/quickcheck.ML")
  Quickcheck.gen_quickcheck (line 503 of "~~/src/Tools/quickcheck.ML")
  Quickcheck.quickcheck_cmd (line 516 of "~~/src/Tools/quickcheck.ML")
  Toplevel.keep_proof(1)(1) (line 347 of "Isar/toplevel.ML")
  Toplevel.apply_tr(3)(1) (line 263 of "Isar/toplevel.ML") 


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