Re: [isabelle] Failing afp-2015 build



On Thu, 19 Nov 2015, Makarius wrote:

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.

That is almost 3 weeks old, and nothing has happened yet. I am routinely on afp-devel, but not the official release branches. Ultimately, it is the job of the AFP authors to maintain their material.


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.

This is also something that can be easily done to improve the maintainability of ConcurrentGC.


	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.