From 771f041a48f611a4869a7a19fa39672581b5ba9a Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Sat, 29 Dec 2018 14:59:09 +0000
Subject: Coq: ensure that recursive functions compute

---
 lib/coq/Sail2_prompt.v | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)

(limited to 'lib')

diff --git a/lib/coq/Sail2_prompt.v b/lib/coq/Sail2_prompt.v
index 85ca95f6..bd0d7750 100644
--- a/lib/coq/Sail2_prompt.v
+++ b/lib/coq/Sail2_prompt.v
@@ -86,6 +86,27 @@ red.
 omega.
 Defined.
 
+(* A version of well-foundedness of measures with a guard to ensure that
+   definitions can be reduced without inspecting proofs, based on a coq-club
+   thread featuring Barras, Gonthier and Gregoire, see
+     https://sympa.inria.fr/sympa/arc/coq-club/2007-07/msg00014.html *)
+
+Fixpoint pos_guard_wf {A:Type} {R:A -> A -> Prop} (p:positive) : well_founded R -> well_founded R :=
+ match p with
+ | xH => fun wfR x => Acc_intro x (fun y _ => wfR y)
+ | xO p' => fun wfR x => let F := pos_guard_wf p' in Acc_intro x (fun y _ => F (F 
+wfR) y)
+ | xI p' => fun wfR x => let F := pos_guard_wf p' in Acc_intro x (fun y _ => F (F 
+wfR) y)
+ end.
+
+Definition Zwf_guarded (z:Z) : Acc (Zwf 0) z :=
+  match z with
+  | Zpos p => pos_guard_wf p (Zwf_well_founded _) _
+  | _ => Zwf_well_founded _ _
+  end.
+
+
 (*val whileM : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) ->
                 ('vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e
 let rec whileM vars cond body =
-- 
cgit v1.2.3


From 3e311bd2a9072146f53bf6c2db9a811d38aee601 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Tue, 1 Jan 2019 13:54:31 +0000
Subject: Coq: update instr_kinds from Lem

---
 lib/coq/Sail2_instr_kinds.v | 15 +++++++++++++--
 1 file changed, 13 insertions(+), 2 deletions(-)

(limited to 'lib')

diff --git a/lib/coq/Sail2_instr_kinds.v b/lib/coq/Sail2_instr_kinds.v
index eadc567a..c6fb866b 100644
--- a/lib/coq/Sail2_instr_kinds.v
+++ b/lib/coq/Sail2_instr_kinds.v
@@ -157,6 +157,7 @@ Inductive barrier_kind :=
   | Barrier_RISCV_rw_r
   | Barrier_RISCV_r_w
   | Barrier_RISCV_w_r
+  | Barrier_RISCV_tso
   | Barrier_RISCV_i
   (* X86 *)
   | Barrier_x86_MFENCE.
@@ -182,6 +183,11 @@ instance (Show barrier_kind)
     | Barrier_RISCV_r_r   -> "Barrier_RISCV_r_r"
     | Barrier_RISCV_rw_w  -> "Barrier_RISCV_rw_w"
     | Barrier_RISCV_w_w   -> "Barrier_RISCV_w_w"
+    | Barrier_RISCV_w_rw  -> "Barrier_RISCV_w_rw"
+    | Barrier_RISCV_rw_r  -> "Barrier_RISCV_rw_r"
+    | Barrier_RISCV_r_w   -> "Barrier_RISCV_r_w"
+    | Barrier_RISCV_w_r   -> "Barrier_RISCV_w_r"
+    | Barrier_RISCV_tso   -> "Barrier_RISCV_tso"
     | Barrier_RISCV_i     -> "Barrier_RISCV_i"
     | Barrier_x86_MFENCE  -> "Barrier_x86_MFENCE"
   end
@@ -295,8 +301,13 @@ instance (EnumerationType barrier_kind)
     | Barrier_RISCV_r_r -> 15
     | Barrier_RISCV_rw_w -> 16
     | Barrier_RISCV_w_w -> 17
-    | Barrier_RISCV_i -> 18
-    | Barrier_x86_MFENCE -> 19
+    | Barrier_RISCV_w_rw -> 18
+    | Barrier_RISCV_rw_r -> 19
+    | Barrier_RISCV_r_w -> 20
+    | Barrier_RISCV_w_r -> 21
+    | Barrier_RISCV_tso -> 22
+    | Barrier_RISCV_i -> 23
+    | Barrier_x86_MFENCE -> 24
   end
 end
 *)
-- 
cgit v1.2.3


From 31adf7edc7957562555037df1df6bad0cca51cf6 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Wed, 9 Jan 2019 11:01:42 +0000
Subject: Coq: add truncateLSB and import Zeuclid by default

---
 lib/coq/Sail2_operators_mwords.v | 9 +++++++++
 lib/coq/Sail2_values.v           | 1 +
 2 files changed, 10 insertions(+)

(limited to 'lib')

diff --git a/lib/coq/Sail2_operators_mwords.v b/lib/coq/Sail2_operators_mwords.v
index 809f9d89..7e4abe29 100644
--- a/lib/coq/Sail2_operators_mwords.v
+++ b/lib/coq/Sail2_operators_mwords.v
@@ -185,10 +185,19 @@ assert ((Z.to_nat m <= Z.to_nat n)%nat).
 { apply Z2Nat.inj_le; omega. }
 omega.
 Qed.
+Lemma truncateLSB_eq {m n} : m >= 0 -> m <= n -> (Z.to_nat n = (Z.to_nat n - Z.to_nat m) + Z.to_nat m)%nat.
+intros.
+assert ((Z.to_nat m <= Z.to_nat n)%nat).
+{ apply Z2Nat.inj_le; omega. }
+omega.
+Qed.
 
 Definition vector_truncate {n} (v : mword n) (m : Z) `{ArithFact (m >= 0)} `{ArithFact (m <= n)} : mword m :=
   cast_to_mword (Word.split1 _ _ (cast_word (get_word v) (ltac:(unwrap_ArithFacts; apply truncate_eq; auto) : Z.to_nat n = Z.to_nat m + (Z.to_nat n - Z.to_nat m))%nat)) (ltac:(unwrap_ArithFacts; apply Z2Nat.id; omega) : Z.of_nat (Z.to_nat m) = m).
 
+Definition vector_truncateLSB {n} (v : mword n) (m : Z) `{ArithFact (m >= 0)} `{ArithFact (m <= n)} : mword m :=
+  cast_to_mword (Word.split2 _ _ (cast_word (get_word v) (ltac:(unwrap_ArithFacts; apply truncateLSB_eq; auto) : Z.to_nat n = (Z.to_nat n - Z.to_nat m) + Z.to_nat m)%nat)) (ltac:(unwrap_ArithFacts; apply Z2Nat.id; omega) : Z.of_nat (Z.to_nat m) = m).
+
 Lemma concat_eq {a b} : a >= 0 -> b >= 0 -> Z.of_nat (Z.to_nat b + Z.to_nat a)%nat = a + b.
 intros.
 rewrite Nat2Z.inj_add.
diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index e3e039c2..2eabacb3 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -9,6 +9,7 @@ Require Export List.
 Require Export Sumbool.
 Require Export DecidableClass.
 Require Import Eqdep_dec.
+Require Export Zeuclid.
 Import ListNotations.
 
 Open Scope Z.
-- 
cgit v1.2.3


From 1c80d84c47faef38149e87e000c6721f6aa6245e Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Wed, 9 Jan 2019 13:43:16 +0000
Subject: Coq: the division used in smt.sail should be Euclidean

---
 lib/coq/Sail2_values.v | 4 ++--
 lib/smt.sail           | 4 ++--
 2 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'lib')

diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index 2eabacb3..219a6f84 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -1655,8 +1655,8 @@ end
 (* Arithmetic functions which return proofs that match the expected Sail
    types in smt.sail. *)
 
-Definition div_with_eq n m : {o : Z & ArithFact (o = Z.quot n m)} := build_ex (Z.quot n m).
-Definition mod_with_eq n m : {o : Z & ArithFact (o = Z.rem n m)} := build_ex (Z.rem n m).
+Definition ediv_with_eq n m : {o : Z & ArithFact (o = ZEuclid.div n m)} := build_ex (ZEuclid.div n m).
+Definition emod_with_eq n m : {o : Z & ArithFact (o = ZEuclid.modulo n m)} := build_ex (ZEuclid.modulo n m).
 Definition abs_with_eq n   : {o : Z & ArithFact (o = Z.abs n)} := build_ex (Z.abs n).
 
 (* Similarly, for ranges (currently in MIPS) *)
diff --git a/lib/smt.sail b/lib/smt.sail
index c57f7bd1..7006b190 100644
--- a/lib/smt.sail
+++ b/lib/smt.sail
@@ -8,7 +8,7 @@ val div = {
   ocaml: "quotient",
   lem: "integerDiv",
   c: "tdiv_int",
-  coq: "div_with_eq"
+  coq: "ediv_with_eq"
 } : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o == div('n, 'm). atom('o)}
 
 overload operator / = {div}
@@ -18,7 +18,7 @@ val mod = {
   ocaml: "modulus",
   lem: "integerMod",
   c: "tmod_int",
-  coq: "mod_with_eq"
+  coq: "emod_with_eq"
 } : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o == mod('n, 'm). atom('o)}
 
 overload operator % = {mod}
-- 
cgit v1.2.3


From 07cf22289b1b4bb2300d4670573a7faee7211a04 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Mon, 21 Jan 2019 18:53:20 +0000
Subject: Fix build of Isabelle documentation

---
 lib/isabelle/Makefile | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'lib')

diff --git a/lib/isabelle/Makefile b/lib/isabelle/Makefile
index 57459b82..f9c061b3 100644
--- a/lib/isabelle/Makefile
+++ b/lib/isabelle/Makefile
@@ -7,7 +7,7 @@ EXTRA_THYS = Sail2_state_monad_lemmas.thy Sail2_state_lemmas.thy \
   Sail2_prompt_monad_lemmas.thy \
   Sail2_operators_mwords_lemmas.thy Hoare.thy
 
-RISCV_DIR = ../../riscv
+RISCV ?= ../../../sail-riscv
 
 .PHONY: all heap-img clean
 
@@ -24,8 +24,8 @@ heap-img: thys $(EXTRA_THYS) ROOT
 
 manual: heap-img manual/Manual.thy manual/ROOT manual/document/root.tex
 	cp output/document/session_graph.pdf manual/document/Sail_session_graph.pdf
-	make -C $(RISCV_DIR) Riscv_duopod.thy
-	isabelle build -d manual -d $(RISCV_DIR) Sail-Manual
+	make -C $(RISCV) riscv_duopod
+	isabelle build -d manual -d $(RISCV)/generated_definitions/isabelle Sail-Manual
 
 Sail2_instr_kinds.thy: ../../src/lem_interp/sail2_instr_kinds.lem
 	lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $<
-- 
cgit v1.2.3


From aeb0f82f67ff829cd7a4b57c638b44a07d39ba3b Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Mon, 21 Jan 2019 19:53:59 +0000
Subject: Don't require manual set up of Isabelle session directories

Since Isabelle 2018, specifying the same directory both on the command
line and persistently in the user's ROOTS file is allowed, so we don't
have to choose between one or the other any more.
---
 lib/isabelle/Makefile | 8 ++------
 1 file changed, 2 insertions(+), 6 deletions(-)

(limited to 'lib')

diff --git a/lib/isabelle/Makefile b/lib/isabelle/Makefile
index f9c061b3..3ce9b9d8 100644
--- a/lib/isabelle/Makefile
+++ b/lib/isabelle/Makefile
@@ -16,16 +16,12 @@ all: thys
 thys: $(THYS)
 
 heap-img: thys $(EXTRA_THYS) ROOT
-	@echo '*** To build a heap image with the Sail library, please'
-	@echo '*** add this directory to your ROOTS file'
-	@echo '*** (e.g. $$HOME/.isabelle/Isabelle<version>/ROOTS)'
-	@echo '*** and add the isabelle binary to your PATH.'
-	isabelle build -b Sail
+	isabelle build -D .
 
 manual: heap-img manual/Manual.thy manual/ROOT manual/document/root.tex
 	cp output/document/session_graph.pdf manual/document/Sail_session_graph.pdf
 	make -C $(RISCV) riscv_duopod
-	isabelle build -d manual -d $(RISCV)/generated_definitions/isabelle Sail-Manual
+	isabelle build -d . -d $(RISCV)/generated_definitions/isabelle -D manual
 
 Sail2_instr_kinds.thy: ../../src/lem_interp/sail2_instr_kinds.lem
 	lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $<
-- 
cgit v1.2.3


From 365cf2015c77551e37d31336220497f6ca84794c Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Mon, 21 Jan 2019 23:16:47 +0000
Subject: Pass Lem library path to Isabelle

---
 lib/isabelle/Makefile | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

(limited to 'lib')

diff --git a/lib/isabelle/Makefile b/lib/isabelle/Makefile
index 3ce9b9d8..a1500292 100644
--- a/lib/isabelle/Makefile
+++ b/lib/isabelle/Makefile
@@ -7,6 +7,11 @@ EXTRA_THYS = Sail2_state_monad_lemmas.thy Sail2_state_lemmas.thy \
   Sail2_prompt_monad_lemmas.thy \
   Sail2_operators_mwords_lemmas.thy Hoare.thy
 
+LEM_ISA_LIB?=$(shell opam config var lem:share)/isabelle-lib
+ifeq ($(wildcard $(LEM_ISA_LIB)/ROOT),)
+$(error isabelle-lib directory of Lem not found. Please set the LEM_ISA_LIB environment variable)
+endif
+
 RISCV ?= ../../../sail-riscv
 
 .PHONY: all heap-img clean
@@ -16,12 +21,12 @@ all: thys
 thys: $(THYS)
 
 heap-img: thys $(EXTRA_THYS) ROOT
-	isabelle build -D .
+	isabelle build -d $(LEM_ISA_LIB) -D .
 
 manual: heap-img manual/Manual.thy manual/ROOT manual/document/root.tex
 	cp output/document/session_graph.pdf manual/document/Sail_session_graph.pdf
 	make -C $(RISCV) riscv_duopod
-	isabelle build -d . -d $(RISCV)/generated_definitions/isabelle -D manual
+	isabelle build -d $(LEM_ISA_LIB) -d . -d $(RISCV)/generated_definitions/isabelle -D manual
 
 Sail2_instr_kinds.thy: ../../src/lem_interp/sail2_instr_kinds.lem
 	lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $<
-- 
cgit v1.2.3


From 8a3c75dfd07d7264a82450aaebce86b5e82c974b Mon Sep 17 00:00:00 2001
From: Prashanth Mundkur
Date: Mon, 21 Jan 2019 18:42:12 -0800
Subject: The RISCV environment variable collides with common usage by the
 RISC-V toolchain; use SAIL_RISCV instead to refer to sail-riscv.

---
 lib/isabelle/Makefile | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'lib')

diff --git a/lib/isabelle/Makefile b/lib/isabelle/Makefile
index a1500292..975810a1 100644
--- a/lib/isabelle/Makefile
+++ b/lib/isabelle/Makefile
@@ -12,7 +12,7 @@ ifeq ($(wildcard $(LEM_ISA_LIB)/ROOT),)
 $(error isabelle-lib directory of Lem not found. Please set the LEM_ISA_LIB environment variable)
 endif
 
-RISCV ?= ../../../sail-riscv
+SAIL_RISCV ?= ../../../sail-riscv
 
 .PHONY: all heap-img clean
 
@@ -25,8 +25,8 @@ heap-img: thys $(EXTRA_THYS) ROOT
 
 manual: heap-img manual/Manual.thy manual/ROOT manual/document/root.tex
 	cp output/document/session_graph.pdf manual/document/Sail_session_graph.pdf
-	make -C $(RISCV) riscv_duopod
-	isabelle build -d $(LEM_ISA_LIB) -d . -d $(RISCV)/generated_definitions/isabelle -D manual
+	make -C $(SAIL_RISCV) riscv_duopod
+	isabelle build -d $(LEM_ISA_LIB) -d . -d $(SAIL_RISCV)/generated_definitions/isabelle -D manual
 
 Sail2_instr_kinds.thy: ../../src/lem_interp/sail2_instr_kinds.lem
 	lem -isa -outdir . -auxiliary_level none -lib ../../src/lem_interp -lib ../../src/gen_lib $<
-- 
cgit v1.2.3


From 63a3cdcd18972cdc2b6fa24d6a2deb5cae7549cc Mon Sep 17 00:00:00 2001
From: Alasdair
Date: Tue, 22 Jan 2019 03:08:46 +0000
Subject: Make sure we optimize constrained union constructors

---
 lib/rts.c | 15 +++++++++++++++
 lib/rts.h |  3 +++
 2 files changed, 18 insertions(+)

(limited to 'lib')

diff --git a/lib/rts.c b/lib/rts.c
index bc0d4732..eacf0a70 100644
--- a/lib/rts.c
+++ b/lib/rts.c
@@ -238,6 +238,21 @@ bool write_ram(const mpz_t addr_size,     // Either 32 or 64
   return true;
 }
 
+sbits fast_read_ram(const int64_t data_size,
+		    const uint64_t addr)
+{
+  uint64_t r = 0;
+  
+  uint64_t byte;
+  for(uint64_t i = (uint64_t) data_size; i > 0; --i) {
+    byte = read_mem(addr + (i - 1));
+    r = r << 8;
+    r = r + byte;
+  }
+  sbits res = {.len = data_size * 8, .bits = r };
+  return res;
+}
+
 void read_ram(lbits *data,
 	      const mpz_t addr_size,
 	      const mpz_t data_size_mpz,
diff --git a/lib/rts.h b/lib/rts.h
index f5e5e3b1..c7c1259f 100644
--- a/lib/rts.h
+++ b/lib/rts.h
@@ -65,6 +65,9 @@ void read_ram(lbits *data,
 	      const lbits hex_ram,
 	      const lbits addr_bv);
 
+sbits fast_read_ram(const int64_t data_size,
+		    const uint64_t addr_bv);
+
 unit write_tag_bool(const fbits, const bool);
 bool read_tag_bool(const fbits);
 
-- 
cgit v1.2.3


From d7c68715687a4a65129cafaa10b9c0e0b89c5897 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Tue, 22 Jan 2019 13:30:24 +0000
Subject: Don't hardcode location of BBV library

---
 lib/coq/Makefile | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'lib')

diff --git a/lib/coq/Makefile b/lib/coq/Makefile
index a5f2874b..6dd962d1 100644
--- a/lib/coq/Makefile
+++ b/lib/coq/Makefile
@@ -1,8 +1,8 @@
-BBV_DIR=../../../bbv/theories
+BBV_DIR?=../../../bbv
 
 SRC=Sail2_prompt_monad.v  Sail2_prompt.v  Sail2_impl_base.v  Sail2_instr_kinds.v  Sail2_operators_bitlists.v  Sail2_operators_mwords.v  Sail2_operators.v  Sail2_values.v  Sail2_state_monad.v  Sail2_state.v  Sail2_string.v  Sail2_real.v
 
-COQ_LIBS = -R . Sail -R "$(BBV_DIR)" bbv
+COQ_LIBS = -R . Sail -R "$(BBV_DIR)/theories" bbv
 
 TARGETS=$(SRC:.v=.vo)
 
-- 
cgit v1.2.3


From 1951607813f73688297840fc4ae4b3059b7528c5 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Wed, 23 Jan 2019 16:29:49 +0000
Subject: Don't let "make" fail unnecessarily in lib/isabelle

Only check for availability of Lem library if actually trying to build
an Isabelle heap image.
---
 lib/isabelle/Makefile | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'lib')

diff --git a/lib/isabelle/Makefile b/lib/isabelle/Makefile
index 975810a1..039a81f1 100644
--- a/lib/isabelle/Makefile
+++ b/lib/isabelle/Makefile
@@ -8,9 +8,6 @@ EXTRA_THYS = Sail2_state_monad_lemmas.thy Sail2_state_lemmas.thy \
   Sail2_operators_mwords_lemmas.thy Hoare.thy
 
 LEM_ISA_LIB?=$(shell opam config var lem:share)/isabelle-lib
-ifeq ($(wildcard $(LEM_ISA_LIB)/ROOT),)
-$(error isabelle-lib directory of Lem not found. Please set the LEM_ISA_LIB environment variable)
-endif
 
 SAIL_RISCV ?= ../../../sail-riscv
 
@@ -21,6 +18,9 @@ all: thys
 thys: $(THYS)
 
 heap-img: thys $(EXTRA_THYS) ROOT
+ifeq ($(wildcard $(LEM_ISA_LIB)/ROOT),)
+	$(error isabelle-lib directory of Lem not found. Please set the LEM_ISA_LIB environment variable)
+endif
 	isabelle build -d $(LEM_ISA_LIB) -D .
 
 manual: heap-img manual/Manual.thy manual/ROOT manual/document/root.tex
-- 
cgit v1.2.3


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')

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')

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