From abfb8f57b6f71d162ee6016ab0fd2e00219ada6a Mon Sep 17 00:00:00 2001 From: Tim Hutt 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 | 14 ++++----- Makefile | 57 ++++++++--------------------------- README.md | 8 ++--- 3 files changed, 23 insertions(+), 56 deletions(-) diff --git a/.github/workflows/compile.yml b/.github/workflows/compile.yml index 865c748a5..333d8ee79 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 zlib1g-dev pkg-config libgmp-dev 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 diff --git a/Makefile b/Makefile index 34fd2bf68..929a93468 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) @@ -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 +# /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) $< diff --git a/README.md b/README.md index 79ca3f6d1..245a71a28 100644 --- a/README.md +++ b/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_