Re: [isabelle] Failing afp-2015 build



On Tue, 17 Nov 2015, Makarius wrote:

 * There is one more occurrence in "Isabelle_Meta_Model", but that
   seems like a copy of what happens in the simplifier.

I will standardize all occurrences, but only in afp-devel.

The relevant changeset for Isabelle_Meta_Model is AFP/c4abbb09645a, but it merely conflates proper use of (PARALLEL_GOALS o ALLGOALS) to PARALLEL_ALLGOALS.


The remaining change for ConcurrentGC is included here -- I leave it to the author/maintainer to apply it on afp-2015 and/or afp-devel. (E.g. with "hg import".)

That is the result of staring a rather long time at not-quite-canonical tactic definitions, to figure out how subgoal addressing is used. Non-standard indentation and overlong source lines make it more difficult to read the text than necessary.


Earlier on this thread, I claimed that there was merely a confusion of PARALLEL_GOALS vs. the newer PARALLEL_ALLGOALS, but basic goal addressing without parallelism was already unclear. Here are relevant paragraphs from the "implementation" manual:

  Operating on a particular subgoal means to replace it by an interval
  of zero or more subgoals in the same place; other subgoals must not
  be affected, apart from instantiating schematic variables ranging
  over the whole goal state.

  A common pattern of composing tactics with subgoal addressing is to
  try the first one, and then the second one only if the subgoal has
  not been solved yet.  Special care is required here to avoid bumping
  into unrelated subgoals that happen to come after the original
  subgoal.  Assuming that there is only a single initial subgoal is a
  very common error when implementing tactics!

  ...

  Some of these conditions are checked by higher-level goal
  infrastructure (\secref{sec:struct-goals}); others are not checked
  explicitly, and violating them merely results in ill-behaved tactics
  experienced by the user (e.g.\ tactics that insist in being
  applicable only to singleton goals, or prevent composition via
  standard tacticals such as @{ML REPEAT}).


Testing this minor change required exceedingly long time, just to get 4-5 attempts work out eventually.

Are there deeper reasons for these proofs to be so slow? The elapsed time of ConncurrentIMP is about that of all of the rest of AFP taken together.

As another peepwhole optimization, it should be possible to conflate

  apply m1
  apply m2
  done

to

  by m1 m2

This is forked in Isabelle/jEdit. Unlike batch builds, more complex proofs are still not forked in the Prover IDE after all these years.


	Makarius
# HG changeset patch
# User wenzelm
# Date 1447942215 -3600
#      Thu Nov 19 15:10:15 2015 +0100
# Node ID c42a363746a571f498ffafbacc5dfe627dfc56cf
# Parent  aa96ef3c08ec968ed1cdaacf18757fb25db26fa1
more robust subgoal addressing of tactics;
prefer canonical PARALLEL_ALLGOALS;

diff -r aa96ef3c08ec -r c42a363746a5 thys/ConcurrentGC/Handshakes.thy
--- a/thys/ConcurrentGC/Handshakes.thy	Wed Nov 18 15:22:17 2015 +0000
+++ b/thys/ConcurrentGC/Handshakes.thy	Thu Nov 19 15:10:15 2015 +0100
@@ -256,14 +256,14 @@
 lemma (in mut_m') handshake_invL[intro]:
   "\<lbrace> handshake_invL \<rbrace> mutator m'"
 apply vcg_nihe
-apply vcg_ni
+apply vcg_ni+
 done
 
 lemma (in gc) mut_handshake_invL[intro]:
   notes mut_m.handshake_invL_def[inv]
   shows "\<lbrace> handshake_invL and mut_m.handshake_invL m \<rbrace> gc \<lbrace> mut_m.handshake_invL m \<rbrace>"
 apply vcg_nihe
-apply vcg_ni
+apply vcg_ni+
 done
 
 lemma (in sys) mut_handshake_invL[intro]:
@@ -275,7 +275,7 @@
   notes gc.handshake_invL_def[inv]
   shows "\<lbrace> handshake_invL and gc.handshake_invL \<rbrace> mutator m \<lbrace> gc.handshake_invL \<rbrace>"
 apply vcg_nihe
-apply vcg_ni
+apply vcg_ni+
 done
 
 lemma (in mut_m) handshake_phase_inv[intro]:
diff -r aa96ef3c08ec -r c42a363746a5 thys/ConcurrentGC/MarkObject.thy
--- a/thys/ConcurrentGC/MarkObject.thy	Wed Nov 18 15:22:17 2015 +0000
+++ b/thys/ConcurrentGC/MarkObject.thy	Thu Nov 19 15:10:15 2015 +0100
@@ -1019,6 +1019,7 @@
   apply (erule greyI)
  apply (clarsimp split: obj_at_splits)
 apply (clarsimp simp: obj_at_field_on_heap_def split: option.splits)
+apply vcg_ni+
 done
 
 lemma (in mut_m) gc_mark_mark_object_invL[intro]:
diff -r aa96ef3c08ec -r c42a363746a5 thys/ConcurrentGC/StrongTricolour.thy
--- a/thys/ConcurrentGC/StrongTricolour.thy	Wed Nov 18 15:22:17 2015 +0000
+++ b/thys/ConcurrentGC/StrongTricolour.thy	Thu Nov 19 15:10:15 2015 +0100
@@ -1932,9 +1932,9 @@
 apply(tactic {*
 let val ctxt = @{context} in
 
-  TRY o vcg_clarsimp_tac ctxt
-THEN'
-  PARALLEL_GOALS o (
+  TRY (HEADGOAL (vcg_clarsimp_tac ctxt))
+THEN
+  PARALLEL_ALLGOALS (
                vcg_sem_tac ctxt
          THEN' (SELECT_GOAL (Local_Defs.unfold_tac ctxt (Inv.get ctxt)))
          THEN' (TRY o REPEAT_ALL_NEW (Tactic.match_tac ctxt @{thms conjI})) (* expose the location predicates, do not split the consequents *)
@@ -1946,11 +1946,9 @@
   THEN_ALL_NEW (TRY o REPEAT_ALL_NEW (Tactic.ematch_tac ctxt @{thms thin_locs} THEN' REPEAT1 o assume_tac ctxt))
   THEN_ALL_NEW asm_full_simp_tac (ss_only (@{thms loc_simps} @ Loc.get ctxt) ctxt)
   THEN_ALL_NEW (TRY o REPEAT_ALL_NEW (Rule_Insts.thin_tac ctxt "True" []))
-  THEN_ALL_NEW clarsimp_tac ctxt
-
-)
-
-end 1
+  THEN_ALL_NEW clarsimp_tac ctxt)
+
+end
 *})
 
 (* hs_noop_done *)
diff -r aa96ef3c08ec -r c42a363746a5 thys/ConcurrentGC/Tactics.thy
--- a/thys/ConcurrentGC/Tactics.thy	Wed Nov 18 15:22:17 2015 +0000
+++ b/thys/ConcurrentGC/Tactics.thy	Thu Nov 19 15:10:15 2015 +0100
@@ -254,18 +254,19 @@
     (Method.sections clasimp_modifiers >> K (SIMPLE_METHOD' o vcg_sem_tac))
     "turn VCG goal into semantics and clarsimp")
 
-fun vcg_jackhammer_gen_tac terminal_method ctxt =
-  vcg_clarsimp_tac ctxt
-THEN'
-  PARALLEL_GOALS o (
-               vcg_sem_tac ctxt
-  THEN_ALL_NEW (full_simp_tac (Splitter.add_split @{thm lcond_split_asm} (ctxt addsimps Inv.get ctxt)))
-  THEN_ALL_NEW ( (TRY o REPEAT_ALL_NEW (Tactic.ematch_tac ctxt @{thms conjE}))
-           THEN' (TRY o REPEAT_ALL_NEW (Tactic.ematch_tac ctxt @{thms thin_locs} THEN' REPEAT1 o assume_tac ctxt))
-           THEN' asm_full_simp_tac (ss_only (@{thms loc_simps} @ Loc.get ctxt) ctxt)
-           THEN_ALL_NEW (TRY o REPEAT_ALL_NEW (Rule_Insts.thin_tac ctxt "True" [])) (* FIXME weird, must be a standard way to do this. Leaving them in can cause simp to diverge ?? *)
-           THEN_ALL_NEW clarsimp_tac (ctxt addsimps (Loc.get ctxt @ @{thms atS_simps})) (* FIXME smelly *)
-           THEN_ALL_NEW TRY o terminal_method ctxt))
+fun vcg_jackhammer_gen_tac terminal_tac ctxt =
+  SELECT_GOAL (
+    HEADGOAL (vcg_clarsimp_tac ctxt)
+  THEN
+    PARALLEL_ALLGOALS (
+                 vcg_sem_tac ctxt
+    THEN_ALL_NEW (full_simp_tac (Splitter.add_split @{thm lcond_split_asm} (ctxt addsimps Inv.get ctxt)))
+    THEN_ALL_NEW ( (TRY o REPEAT_ALL_NEW (Tactic.ematch_tac ctxt @{thms conjE}))
+             THEN' (TRY o REPEAT_ALL_NEW (Tactic.ematch_tac ctxt @{thms thin_locs} THEN' REPEAT1 o assume_tac ctxt))
+             THEN' asm_full_simp_tac (ss_only (@{thms loc_simps} @ Loc.get ctxt) ctxt)
+             THEN_ALL_NEW (TRY o REPEAT_ALL_NEW (Rule_Insts.thin_tac ctxt "True" [])) (* FIXME weird, must be a standard way to do this. Leaving them in can cause simp to diverge ?? *)
+             THEN_ALL_NEW clarsimp_tac (ctxt addsimps (Loc.get ctxt @ @{thms atS_simps})) (* FIXME smelly *)
+             THEN_ALL_NEW TRY o terminal_tac ctxt)))
 
 val _ =
   Theory.setup (Method.setup @{binding vcg_jackhammer}
@@ -278,28 +279,30 @@
     "VCG supertactic, fastforce the survivors")
 
 fun vcg_ni_tac ctxt =
-  TRY o vcg_clarsimp_tac ctxt
-THEN'
-  PARALLEL_GOALS o (
-               vcg_sem_tac ctxt
-         THEN' (TRY o SELECT_GOAL (Local_Defs.unfold_tac ctxt (Inv.get ctxt)))
-         THEN' (TRY o REPEAT_ALL_NEW (Tactic.match_tac ctxt @{thms conjI})) (* expose the location predicates, do not split the consequents *)
-  THEN_ALL_NEW (TRY o REPEAT_ALL_NEW (Tactic.match_tac ctxt @{thms impI}))
-                   (* Preserve the label sets in atS but normalise the label in at; turn s' into s *)
-  THEN_ALL_NEW asm_full_simp_tac ctxt (* FIXME diverges on some invariants *)
-  THEN_ALL_NEW (TRY o REPEAT_ALL_NEW (Tactic.ematch_tac ctxt @{thms conjE}))
-                   (* The effect of vcg_pre: should be cheap *)
-  THEN_ALL_NEW (TRY o REPEAT_ALL_NEW (Tactic.ematch_tac ctxt @{thms thin_locs} THEN' REPEAT1 o assume_tac ctxt))
-  THEN_ALL_NEW asm_full_simp_tac (ss_only (@{thms loc_simps} @ Loc.get ctxt) ctxt)
-  THEN_ALL_NEW (TRY o REPEAT_ALL_NEW (Rule_Insts.thin_tac ctxt "True" [])) (* FIXME weird, must be a standard way to do this. Leaving them in can cause simp to diverge ?? *)
-  THEN_ALL_NEW clarsimp_tac ctxt)
+  SELECT_GOAL (
+    HEADGOAL (TRY o vcg_clarsimp_tac ctxt)
+  THEN
+    PARALLEL_ALLGOALS (
+                   vcg_sem_tac ctxt
+             THEN' (TRY o SELECT_GOAL (Local_Defs.unfold_tac ctxt (Inv.get ctxt)))
+             THEN' (TRY o REPEAT_ALL_NEW (Tactic.match_tac ctxt @{thms conjI})) (* expose the location predicates, do not split the consequents *)
+      THEN_ALL_NEW (TRY o REPEAT_ALL_NEW (Tactic.match_tac ctxt @{thms impI}))
+                       (* Preserve the label sets in atS but normalise the label in at; turn s' into s *)
+      THEN_ALL_NEW asm_full_simp_tac ctxt (* FIXME diverges on some invariants *)
+      THEN_ALL_NEW (TRY o REPEAT_ALL_NEW (Tactic.ematch_tac ctxt @{thms conjE}))
+                       (* The effect of vcg_pre: should be cheap *)
+      THEN_ALL_NEW (TRY o REPEAT_ALL_NEW (Tactic.ematch_tac ctxt @{thms thin_locs} THEN' REPEAT1 o assume_tac ctxt))
+      THEN_ALL_NEW asm_full_simp_tac (ss_only (@{thms loc_simps} @ Loc.get ctxt) ctxt)
+      THEN_ALL_NEW (TRY o REPEAT_ALL_NEW (Rule_Insts.thin_tac ctxt "True" [])) (* FIXME weird, must be a standard way to do this. Leaving them in can cause simp to diverge ?? *)
+      THEN_ALL_NEW clarsimp_tac ctxt))
 
 fun vcg_nihe_tac ctxt =
-  vcg_clarsimp_tac ctxt
-THEN'
-  PARALLEL_GOALS o (
-        (vcg_sem_tac ctxt THEN_ALL_NEW (Tactic.ematch_tac ctxt (NIE.get ctxt) THEN_ALL_NEW clarsimp_tac ctxt THEN_ALL_NEW SELECT_GOAL no_tac))
-ORELSE' SELECT_GOAL all_tac) (* FIXME perhaps replace with vcg_ni? but less diagnosable then *)
+  SELECT_GOAL (
+    HEADGOAL (vcg_clarsimp_tac ctxt)
+  THEN
+    PARALLEL_ALLGOALS (
+      (vcg_sem_tac ctxt THEN_ALL_NEW (Tactic.ematch_tac ctxt (NIE.get ctxt) THEN_ALL_NEW clarsimp_tac ctxt THEN_ALL_NEW SELECT_GOAL no_tac))
+      ORELSE' SELECT_GOAL all_tac)) (* FIXME perhaps replace with vcg_ni? but less diagnosable then *)
 
 val _ =
   Theory.setup (Method.setup @{binding vcg_ni}


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