From 184bdfb95468ce3622db048148ae984d31a0305b Mon Sep 17 00:00:00 2001
From: Mitchell Buckley <mitchell.alan.buckley@gmail.com>
Date: Sat, 26 Jun 2021 18:13:22 +1000
Subject: [PATCH] refine: fix regression caused by bad theory import

Importing Init_R into ADT_H was causing EmptyFail_H to fail. Since
no other theories actually depend on Init_R we can instead include
it in the Refine session directly.

Signed-off-by: Mitchell Buckley <mitchell.alan.buckley@gmail.com>
---
 proof/ROOT                     | 3 +++
 proof/refine/ARM/ADT_H.thy     | 1 -
 proof/refine/ARM_HYP/ADT_H.thy | 1 -
 proof/refine/RISCV64/ADT_H.thy | 4 +---
 proof/refine/X64/ADT_H.thy     | 1 -
 5 files changed, 4 insertions(+), 6 deletions(-)

diff --git a/proof/ROOT b/proof/ROOT
index d462f6e22..8930d8a58 100644
--- a/proof/ROOT
+++ b/proof/ROOT
@@ -38,14 +38,17 @@ session Refine in "refine" = BaseRefine +
     "$L4V_ARCH/Refine"
     "$L4V_ARCH/RAB_FN"
     "$L4V_ARCH/EmptyFail_H"
+    "$L4V_ARCH/Init_R"
   theories [condition = "SKIP_REFINE_PROOFS", quick_and_dirty, skip_proofs]
     "$L4V_ARCH/Refine"
     "$L4V_ARCH/RAB_FN"
     "$L4V_ARCH/EmptyFail_H"
+    "$L4V_ARCH/Init_R"
   theories
     "$L4V_ARCH/Refine"
     "$L4V_ARCH/RAB_FN"
     "$L4V_ARCH/EmptyFail_H"
+    "$L4V_ARCH/Init_R"
 
 (*
  * This theory is in a separate session because the proofs currently
diff --git a/proof/refine/ARM/ADT_H.thy b/proof/refine/ARM/ADT_H.thy
index 20b379cd0..9c41d7d79 100644
--- a/proof/refine/ARM/ADT_H.thy
+++ b/proof/refine/ARM/ADT_H.thy
@@ -10,7 +10,6 @@ theory ADT_H
 imports
   "AInvs.ADT_AI"
   Syscall_R
-  Init_R
 begin
 
 text \<open>
diff --git a/proof/refine/ARM_HYP/ADT_H.thy b/proof/refine/ARM_HYP/ADT_H.thy
index 5f84cd8e4..01ec349f3 100644
--- a/proof/refine/ARM_HYP/ADT_H.thy
+++ b/proof/refine/ARM_HYP/ADT_H.thy
@@ -10,7 +10,6 @@ theory ADT_H
 imports
   "AInvs.ADT_AI"
   Syscall_R
-  Init_R
 begin
 
 text \<open>
diff --git a/proof/refine/RISCV64/ADT_H.thy b/proof/refine/RISCV64/ADT_H.thy
index 672a69d49..9892819f1 100644
--- a/proof/refine/RISCV64/ADT_H.thy
+++ b/proof/refine/RISCV64/ADT_H.thy
@@ -7,9 +7,7 @@
 chapter \<open>Abstract datatype for the executable specification\<close>
 
 theory ADT_H
-  imports
-    Syscall_R
-    Init_R
+  imports Syscall_R
 begin
 
 text \<open>
diff --git a/proof/refine/X64/ADT_H.thy b/proof/refine/X64/ADT_H.thy
index 1ea1d1640..65d8312c9 100644
--- a/proof/refine/X64/ADT_H.thy
+++ b/proof/refine/X64/ADT_H.thy
@@ -9,7 +9,6 @@ chapter \<open>Abstract datatype for the executable specification\<close>
 theory ADT_H
 imports
   "AInvs.ADT_AI"
-  Init_R
   Syscall_R
 begin