Add snapshots of auto-generated lemmas

CTSRD-CHERI · Apr 22, 2022 · f917601 · f917601
1 parent 72f8720
commit f917601
Show file tree

Hide file tree

Showing 7 changed files with 48,277 additions and 6 deletions.
diff --git a/.gitignore b/.gitignore
@@ -1,8 +1,8 @@
-CHERI_Gen_Lemmas.thy
-CHERI_Cap_Properties.thy
-CHERI_Mem_Properties.thy
-CHERI_Fetch_Properties.thy
-CHERI_Invariant.thy
+# CHERI_Gen_Lemmas.thy
+# CHERI_Cap_Properties.thy
+# CHERI_Mem_Properties.thy
+# CHERI_Fetch_Properties.thy
+# CHERI_Invariant.thy
 *.thy~
 *.smt2
 z3_problems

diff --git a/CHERI_Cap_Properties.thy b/CHERI_Cap_Properties.thy
diff --git a/CHERI_Fetch_Properties.thy b/CHERI_Fetch_Properties.thy
diff --git a/CHERI_Gen_Lemmas.thy b/CHERI_Gen_Lemmas.thy
diff --git a/CHERI_Invariant.thy b/CHERI_Invariant.thy
diff --git a/CHERI_Mem_Properties.thy b/CHERI_Mem_Properties.thy
diff --git a/Makefile b/Makefile
@@ -22,12 +22,21 @@ else
 LEM_DIR:=$(shell opam config var lem:share)
 endif
 
+# Check if the sail-morello directory has snapshots of the Lem and Sail Isabelle libraries
+ifneq ($(wildcard $(MORELLO_DIR)/lib/isabelle),)
+  SAIL_LEM_LIB = $(MORELLO_DIR)/lib/isabelle/lem
+  SAIL_ISA_LIB = $(MORELLO_DIR)/lib/isabelle/sail
+else
+  SAIL_LEM_LIB = $(LEM_DIR)/isabelle-lib
+  SAIL_ISA_LIB = $(SAIL_DIR)/lib/isabelle
+endif
+
 GEN_LEMMAS = $(T_CHERI_DIR)/tools/gen_lemmas
 MORELLO_SAIL_DIR = $(MORELLO_DIR)/src
 MORELLO_ISA_DIR = $(MORELLO_DIR)/isabelle
 MORELLO_PATCHES_DIR = $(MORELLO_SAIL_DIR)/patches
 
-ISA_DEPS = $(LEM_DIR)/isabelle-lib $(SAIL_DIR)/lib/isabelle $(AFP_DIR)/thys/Word_Lib $(T_CHERI_DIR)/model/isabelle $(MORELLO_ISA_DIR)
+ISA_DEPS = $(SAIL_LEM_LIB) $(SAIL_ISA_LIB) $(AFP_DIR)/thys/Word_Lib $(T_CHERI_DIR)/model/isabelle $(MORELLO_ISA_DIR)
 ISA_DEP_FLAGS = $(foreach dir,$(ISA_DEPS),-d $(dir))
 ISA_BUILD_FLAGS = -v $(ISA_DEP_FLAGS)