lib+proof: remove obsolete DupSkip cache mentions

DupSkip used to be a proof caching option since replaced by "defer proofs". It is no longer available in our Isabelle branch. Remove last mentions and related files. Signed-off-by: Gerwin Klein <[email protected]>
seL4 · Jun 4, 2024 · dd6295d · dd6295d
1 parent e9b2508
commit dd6295d
Show file tree

Hide file tree

Showing 13 changed files with 2 additions and 401 deletions.
diff --git a/lib/crunch-cmd.ML b/lib/crunch-cmd.ML
@@ -795,7 +795,7 @@ fun crunch cfg pre extra stack const' thms =
           val _ = writeln ("attempting: " ^ Syntax.string_of_term ctxt''' goal_prop);
           fun wp' wp_rules = wp ctxt (map snd (thms @ #wp_rules cfg) @ goals' @ wp_rules)
           val thm = Goal.prove_future ctxt''' [] [] goal_prop
-              ( (*DupSkip.goal_prove_wrapper *) (fn _ =>
+              (fn _ =>
               resolve_tac ctxt''' [rule] 1
                 THEN maybe_cheat_tac ctxt'''
               THEN ALLGOALS (simp_tac ctxt''')
@@ -820,7 +820,7 @@ fun crunch cfg pre extra stack const' thms =
                   CHANGED_GOAL (simp_tac ctxt''')
                 ) n))
               THEN proof_failed_warnings const stack cfg wp' ctxt'''
-              )) |> singleton (Proof_Context.export ctxt''' ctxt)
+              ) |> singleton (Proof_Context.export ctxt''' ctxt)
         in (SOME thm, (get_thm_name cfg const, thm) :: thms') end
     end
     handle WrongType =>

diff --git a/proof/crefine/ARM/BuildRefineCache_C.thy b/proof/crefine/ARM/BuildRefineCache_C.thy
diff --git a/proof/crefine/ARM/CACHE.ML b/proof/crefine/ARM/CACHE.ML
diff --git a/proof/crefine/ARM/Cache.thy b/proof/crefine/ARM/Cache.thy
diff --git a/proof/crefine/ARM_HYP/BuildRefineCache_C.thy b/proof/crefine/ARM_HYP/BuildRefineCache_C.thy
diff --git a/proof/crefine/ARM_HYP/CACHE.ML b/proof/crefine/ARM_HYP/CACHE.ML
diff --git a/proof/crefine/ARM_HYP/Cache.thy b/proof/crefine/ARM_HYP/Cache.thy
diff --git a/proof/refine/ARM/BuildRefineCache.thy b/proof/refine/ARM/BuildRefineCache.thy
diff --git a/proof/refine/ARM/Cache.thy b/proof/refine/ARM/Cache.thy
diff --git a/proof/refine/ARM_HYP/BuildRefineCache.thy b/proof/refine/ARM_HYP/BuildRefineCache.thy
diff --git a/proof/refine/ARM_HYP/Cache.thy b/proof/refine/ARM_HYP/Cache.thy
diff --git a/proof/refine/X64/BuildRefineCache.thy b/proof/refine/X64/BuildRefineCache.thy