From 33402308d861bf5067107a83c97e69f870cf3710 Mon Sep 17 00:00:00 2001
From: Tim Hutt <timothy.hutt@codasip.com>
Date: Thu, 8 Aug 2024 10:28:21 +0100
Subject: [PATCH] Install Sail from binary in CI

This should be a lot faster. It also means the version is pinned properly which wasn't the case before.

I also recommended users to do the same in the README do they don't have to deal with OPAM.
---
 .github/workflows/compile.yml | 12 ++++----
 Makefile                      | 57 ++++++++---------------------------
 README.md                     |  2 +-
 3 files changed, 19 insertions(+), 52 deletions(-)

diff --git a/.github/workflows/compile.yml b/.github/workflows/compile.yml
index 865c748a5..129d80c34 100644
--- a/.github/workflows/compile.yml
+++ b/.github/workflows/compile.yml
@@ -7,19 +7,19 @@ jobs:
     runs-on: ubuntu-22.04
     steps:
     - name: Install packages
-      run: sudo apt install -y opam zlib1g-dev pkg-config libgmp-dev z3 device-tree-compiler
+      run: sudo apt install -y --no-install-recommends ocaml zlib1g-dev pkg-config libgmp-dev device-tree-compiler curl
     - name: Check out repository code
       uses: actions/checkout@HEAD
       with:
         submodules: true
     - name: Ensure pre-commit checks pass
       run: pip install pre-commit && pre-commit run --all-files --show-diff-on-failure --color=always
-    - name: Init opam
-      run: opam init --disable-sandboxing -y
-    - name: Install sail
-      run: opam install -y sail
+    - name: Install sail from binary
+      run: |
+        sudo mkdir -p /usr/local
+        curl --location https://github.com/rems-project/sail/releases/download/0.18-linux-binary/sail.tar.gz | sudo tar xvz --directory=/usr/local --strip-components=1
     - name: Build and test simulators
-      run: eval $(opam env) && test/run_tests.sh
+      run: test/run_tests.sh
     - name: Upload test results
       if: always()
       uses: actions/upload-artifact@v4
diff --git a/Makefile b/Makefile
index e26ee2901..869c97c20 100644
--- a/Makefile
+++ b/Makefile
@@ -7,9 +7,6 @@ else ifeq ($(ARCH),64)
   override ARCH := RV64
 endif
 
-# Set OPAMCLI to 2.0 to supress warnings about opam config var
-export OPAMCLI := 2.0
-
 ifeq ($(ARCH),RV32)
   SAIL_XLEN := riscv_xlen32.sail
 else ifeq ($(ARCH),RV64)
@@ -130,24 +127,15 @@ PLATFORM_OCAML_SRCS = $(addprefix ocaml_emulator/,platform.ml platform_impl.ml s
 SAIL_FLAGS += -dno_cast
 SAIL_DOC_FLAGS ?= -doc_embed plain
 
-# Attempt to work with either sail from opam or built from repo in SAIL_DIR
-ifneq ($(SAIL_DIR),)
-# Use sail repo in SAIL_DIR
-SAIL:=$(SAIL_DIR)/sail
-export SAIL_DIR
-EXPLICIT_COQ_SAIL=yes
-else
-# Use sail from opam package
-SAIL_DIR:=$(shell OPAMCLI=$(OPAMCLI) opam config var sail:share)
-SAIL:=sail
-endif
-SAIL_LIB_DIR:=$(SAIL_DIR)/lib
-export SAIL_LIB_DIR
-SAIL_SRC_DIR:=$(SAIL_DIR)/src
+# Sail command to use.
+SAIL := sail
 
-ifndef LEM_DIR
-LEM_DIR:=$(shell OPAMCLI=$(OPAMCLI) opam config var lem:share)
-endif
+# <sail install dir>/share/sail
+SAIL_DIR := $(shell $(SAIL) --dir)
+SAIL_LIB_DIR := $(SAIL_DIR)/lib
+SAIL_SRC_DIR := $(SAIL_DIR)/src
+
+LEM_DIR := $(SAIL_DIR)/../lem
 export LEM_DIR
 
 C_WARNINGS ?=
@@ -375,27 +363,10 @@ riscv_hol: generated_definitions/hol4/$(ARCH)/riscvScript.sml
 riscv_hol_build: generated_definitions/hol4/$(ARCH)/riscvTheory.uo
 .PHONY: riscv_hol riscv_hol_build
 
-ifdef BBV_DIR
-  EXPLICIT_COQ_BBV := yes
-else
-  EXPLICIT_COQ_BBV := $(shell if OPAMCLI=$(OPAMCLI) opam config var coq-bbv:share >/dev/null 2>/dev/null; then echo no; else echo yes; fi)
-  ifeq ($(EXPLICIT_COQ_BBV),yes)
-    #Coq BBV library hopefully checked out in directory above us
-    BBV_DIR = ../bbv
-  endif
-endif
-
-ifndef EXPLICIT_COQ_SAIL
-  EXPLICIT_COQ_SAIL := $(shell if OPAMCLI=$(OPAMCLI) opam config var coq-sail:share >/dev/null 2>/dev/null; then echo no; else echo yes; fi)
-endif
 
 COQ_LIBS = -R generated_definitions/coq Riscv -R generated_definitions/coq/$(ARCH) $(ARCH) -R handwritten_support Riscv_common
-ifeq ($(EXPLICIT_COQ_BBV),yes)
-  COQ_LIBS += -Q $(BBV_DIR)/src/bbv bbv
-endif
-ifeq ($(EXPLICIT_COQ_SAIL),yes)
-  COQ_LIBS += -Q $(SAIL_LIB_DIR)/coq Sail
-endif
+COQ_LIBS += -Q $(BBV_DIR)/src/bbv bbv
+COQ_LIBS += -Q $(SAIL_LIB_DIR)/coq Sail
 
 riscv_coq: $(addprefix generated_definitions/coq/$(ARCH)/,riscv.v riscv_types.v)
 riscv_coq_build: generated_definitions/coq/$(ARCH)/riscv.vo
@@ -406,15 +377,11 @@ $(addprefix generated_definitions/coq/$(ARCH)/,riscv.v riscv_types.v): $(SAIL_CO
 	$(SAIL) $(SAIL_FLAGS) -dcoq_undef_axioms -coq -coq_output_dir generated_definitions/coq/$(ARCH) -o riscv -coq_lib riscv_extras -coq_lib mem_metadata $(SAIL_COQ_SRCS)
 
 %.vo: %.v
-ifeq ($(EXPLICIT_COQ_BBV),yes)
-  ifeq ($(wildcard $(BBV_DIR)/src),)
+ifeq ($(wildcard $(BBV_DIR)/src),)
 	$(error BBV directory not found. Please set the BBV_DIR environment variable)
-  endif
 endif
-ifeq ($(EXPLICIT_COQ_SAIL),yes)
-  ifeq ($(wildcard $(SAIL_LIB_DIR)/coq),)
+ifeq ($(wildcard $(SAIL_LIB_DIR)/coq),)
 	$(error lib directory of Sail not found. Please set the SAIL_LIB_DIR environment variable)
-  endif
 endif
 	coqc $(COQ_LIBS) $<
 
diff --git a/README.md b/README.md
index 25057078d..11ee98575 100644
--- a/README.md
+++ b/README.md
@@ -275,7 +275,7 @@ Getting started
 
 ### Building the model
 
-Install [Sail](https://github.com/rems-project/sail/) [using opam](https://github.com/rems-project/sail/blob/sail2/INSTALL.md) then:
+Install [Sail](https://github.com/rems-project/sail/). On Linux you can download a [binary release](https://github.com/rems-project/sail/releases) (strongly recommended), or you can install from source [using opam](https://github.com/rems-project/sail/blob/sail2/INSTALL.md). Then:
 
 ```
 $ make