From 2bb0bc45b6aa4f02b4e88d14a82baa64747cd483 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Fri, 1 Feb 2019 11:57:18 +0000
Subject: Make hol libraries use opam Lem library by default

---
 lib/hol/Holmakefile | 8 ++++----
 lib/hol/Makefile    | 4 +++-
 2 files changed, 7 insertions(+), 5 deletions(-)

(limited to 'lib/hol')

diff --git a/lib/hol/Holmakefile b/lib/hol/Holmakefile
index 8e8403f3..08155507 100644
--- a/lib/hol/Holmakefile
+++ b/lib/hol/Holmakefile
@@ -1,3 +1,5 @@
+# Ensure LEM_DIR is set before running Holmake, e.g., by using the accompanying Makefile
+
 LEM_SCRIPTS = sail2_instr_kindsScript.sml sail2_valuesScript.sml sail2_operatorsScript.sml \
   sail2_operators_mwordsScript.sml sail2_operators_bitlistsScript.sml \
   sail2_state_monadScript.sml sail2_stateScript.sml sail2_promptScript.sml sail2_prompt_monadScript.sml \
@@ -10,9 +12,7 @@ SCRIPTS = $(LEM_SCRIPTS) \
 
 THYS = $(patsubst %Script.sml,%Theory.uo,$(SCRIPTS))
 
-LEMDIR=../../../lem/hol-lib
-
-INCLUDES = $(LEMDIR)
+INCLUDES = $(LEM_DIR)
 
 all: $(THYS)
 .PHONY: all
@@ -23,7 +23,7 @@ ifdef POLY
 HOLHEAP = sail-heap
 EXTRA_CLEANS = $(LEM_CLEANS) $(HOLHEAP) $(HOLHEAP).o
 
-BASE_HEAP = $(LEMDIR)/lemheap
+BASE_HEAP = $(LEM_DIR)/lemheap
 
 $(HOLHEAP): $(BASE_HEAP)
 	$(protect $(HOLDIR)/bin/buildheap) -o $(HOLHEAP) -b $(BASE_HEAP)
diff --git a/lib/hol/Makefile b/lib/hol/Makefile
index 783ef23d..204328d4 100644
--- a/lib/hol/Makefile
+++ b/lib/hol/Makefile
@@ -1,3 +1,5 @@
+LEM_DIR?=$(shell opam config var lem:share)/hol-lib
+
 LEMSRC =  \
   ../../src/lem_interp/sail2_instr_kinds.lem \
   ../../src/gen_lib/sail2_values.lem \
@@ -25,7 +27,7 @@ $(SCRIPTS): $(LEMSRC)
 	lem -hol -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $(LEMSRC)
 
 $(THYS) sail-heap: $(SCRIPTS)
-	Holmake
+	LEM_DIR=$(LEM_DIR) Holmake
 
 # Holmake will also clear out the generated $(SCRIPTS) files
 clean:
-- 
cgit v1.2.3


From 8fa50e9e2fc4752e9c7e14b59ad0c749f56914b4 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Fri, 1 Feb 2019 14:28:30 +0000
Subject: Tweak HOL LEM_DIR to match riscv makefile

---
 lib/hol/Holmakefile | 4 ++--
 lib/hol/Makefile    | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'lib/hol')

diff --git a/lib/hol/Holmakefile b/lib/hol/Holmakefile
index 08155507..0da5813f 100644
--- a/lib/hol/Holmakefile
+++ b/lib/hol/Holmakefile
@@ -12,7 +12,7 @@ SCRIPTS = $(LEM_SCRIPTS) \
 
 THYS = $(patsubst %Script.sml,%Theory.uo,$(SCRIPTS))
 
-INCLUDES = $(LEM_DIR)
+INCLUDES = $(LEM_DIR)/hol-lib
 
 all: $(THYS)
 .PHONY: all
@@ -23,7 +23,7 @@ ifdef POLY
 HOLHEAP = sail-heap
 EXTRA_CLEANS = $(LEM_CLEANS) $(HOLHEAP) $(HOLHEAP).o
 
-BASE_HEAP = $(LEM_DIR)/lemheap
+BASE_HEAP = $(LEM_DIR)/hol-lib/lemheap
 
 $(HOLHEAP): $(BASE_HEAP)
 	$(protect $(HOLDIR)/bin/buildheap) -o $(HOLHEAP) -b $(BASE_HEAP)
diff --git a/lib/hol/Makefile b/lib/hol/Makefile
index 204328d4..c863a05b 100644
--- a/lib/hol/Makefile
+++ b/lib/hol/Makefile
@@ -1,4 +1,4 @@
-LEM_DIR?=$(shell opam config var lem:share)/hol-lib
+LEM_DIR?=$(shell opam config var lem:share)
 
 LEMSRC =  \
   ../../src/lem_interp/sail2_instr_kinds.lem \
-- 
cgit v1.2.3