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

@@ -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 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
+      run: python3 -m pip install pre-commit && pre-commit run --all-files --show-diff-on-failure --color=always
+    - 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

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)
@@ -133,24 +130,15 @@ SAIL_FLAGS += --strict-var
 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 ?=
@@ -343,27 +331,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
@@ -374,15 +345,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) $<
 

README.md

@@ -256,13 +256,13 @@ 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
 ```
 
-will build the C simulator in `c_emulator/riscv_sim_RV64`.
+will build the simulator in `c_emulator/riscv_sim_RV64`.
 
 If you get an error message saying `sail: unknown option '--require-version'.` it's because your Sail compiler is too old. You need version 0.18 or later.
 
@@ -275,7 +275,7 @@ built using:
 $ ARCH=RV32 make
 ```
 
-which creates the C simulator in `c_emulator/riscv_sim_RV32`.
+which creates the simulator in `c_emulator/riscv_sim_RV32`.
 
 The Makefile targets `riscv_isa_build`, `riscv_coq_build`, and
 `riscv_hol_build` invoke the respective prover to process the
@@ -291,7 +291,7 @@ corresponding prover libraries in the Sail directory
 
 ### Executing test binaries
 
-The C simulator can be used to execute small test binaries.
+The simulator can be used to execute small test binaries.
 
 ```
 $ ./c_emulator/riscv_sim_<arch> <elf-file>