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 ocaml ocamlbuild 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

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

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