From b89abf9c9e1a32892c14ab3c2e92656b1410ecac Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Fri, 29 Jun 2018 12:07:00 +0100
Subject: Coq building rule in MIPS makefile

---
 mips/Makefile | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

(limited to 'mips/Makefile')

diff --git a/mips/Makefile b/mips/Makefile
index a8bce143..d3a21957 100644
--- a/mips/Makefile
+++ b/mips/Makefile
@@ -47,6 +47,13 @@ mips.v: $(MIPS_PRE) $(MIPS_TLB) $(MIPS_SAILS)
 	$(SAIL) -coq -dcoq_undef_axioms -o mips -coq_lib mips_extras -undefined_gen -memo_z3 $^
 mips_types.v: mips.v
 
+MIPS_COQ = mips_types.v mips_extras.v mips.v
+COQ_LIBS = -R ../../bbv bbv -R ../lib/coq Sail
+
+%.vo: %.v
+	coqc $(COQ_LIBS) $<
+mips.vo: mips_types.vo mips_extras.vo
+
 M%.thy: m%.lem m%_types.lem mips_extras.lem
 	lem -isa -outdir . -lib $(SAIL_DIR)/src/gen_lib -lib $(SAIL_DIR)/src/lem_interp $^
 	sed -i 's/datatype ast/datatype (plugins only: size) ast/' M$*_types.thy
@@ -63,5 +70,5 @@ include ../etc/loc.mk
 clean:
 	rm -rf mips Mips.thy mips.lem mips_types.lem _sbuild mips.c mips_c
 	rm -f mipsScript.sml mips_typesScript.sml mips_extrasScript.sml
-	rm -f mips.v mips_types.v
+	rm -f mips.v mips_types.v $(MIPS_COQ:%.v=%.vo) $(MIPS_COQ:%.v=%.glob) $(MIPS_COQ:%.v=.%.aux)
 	-Holmake cleanAll
-- 
cgit v1.2.3


From e5654331c24391e984484e590993887b499af9f8 Mon Sep 17 00:00:00 2001
From: Robert Norton
Date: Thu, 5 Jul 2018 16:30:31 +0100
Subject: mips: ignore unused functions warnings caused by making some
 functions static.

---
 mips/Makefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'mips/Makefile')

diff --git a/mips/Makefile b/mips/Makefile
index d3a21957..f8b7588f 100644
--- a/mips/Makefile
+++ b/mips/Makefile
@@ -18,7 +18,7 @@ mips: $(MIPS_PRE) $(MIPS_TLB) $(MIPS_SAILS) $(MIPS_MAIN) ../sail
 mips.c: $(MIPS_PRE) $(MIPS_TLB) $(MIPS_SAILS) $(MIPS_MAIN) Makefile ../sail
 	$(SAIL) -O -memo_z3 -c $(filter %.sail, $^) 1> $@
 
-C_WARNINGS=-Wall -Wno-unused-but-set-variable -Wno-unused-label -Wno-maybe-uninitialized -Wno-return-type
+C_WARNINGS=-Wall -Wno-unused-but-set-variable -Wno-unused-label -Wno-unused-function -Wno-maybe-uninitialized -Wno-return-type
 C_OPT=-O2
 GCOV_FLAGS=
 mips_c: mips.c ../lib/sail.h ../lib/*.c Makefile 
-- 
cgit v1.2.3


From 5ee9dfaf970de672aa379ea466bf48292bcd41cf Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Sat, 7 Jul 2018 16:37:00 +0100
Subject: Coq: bbv have reorganised their repository

---
 mips/Makefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'mips/Makefile')

diff --git a/mips/Makefile b/mips/Makefile
index f8b7588f..062ccd8b 100644
--- a/mips/Makefile
+++ b/mips/Makefile
@@ -48,7 +48,7 @@ mips.v: $(MIPS_PRE) $(MIPS_TLB) $(MIPS_SAILS)
 mips_types.v: mips.v
 
 MIPS_COQ = mips_types.v mips_extras.v mips.v
-COQ_LIBS = -R ../../bbv bbv -R ../lib/coq Sail
+COQ_LIBS = -R ../../bbv/theories bbv -R ../lib/coq Sail
 
 %.vo: %.v
 	coqc $(COQ_LIBS) $<
-- 
cgit v1.2.3


From 497c8bf636619988203f8a868806fb04903db2dd Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Tue, 10 Jul 2018 16:50:06 +0100
Subject: Make HOL build properly again for all of the models

---
 mips/Makefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'mips/Makefile')

diff --git a/mips/Makefile b/mips/Makefile
index 062ccd8b..9fdda4d3 100644
--- a/mips/Makefile
+++ b/mips/Makefile
@@ -59,7 +59,7 @@ M%.thy: m%.lem m%_types.lem mips_extras.lem
 	sed -i 's/datatype ast/datatype (plugins only: size) ast/' M$*_types.thy
 
 %Script.sml: %.lem %_types.lem $(MIPS_SAIL_DIR)/mips_extras.lem
-	lem -hol -outdir . -lib $(SAIL_DIR)/lib/hol -lib $(SAIL_DIR)/src/gen_lib -lib $(SAIL_DIR)/src/lem_interp $^
+	lem -hol -outdir . -lib $(SAIL_DIR)/lib/hol -i $(SAIL_DIR)/lib/hol/sail2_prompt_monad.lem -i $(SAIL_DIR)/lib/hol/sail2_prompt.lem -lib $(SAIL_DIR)/src/gen_lib -lib $(SAIL_DIR)/src/lem_interp $^
 
 %Theory.uo: %Script.sml
 	Holmake $@
-- 
cgit v1.2.3