Add support for building a binary Linux release

This adds initial support for building a binary Linux tarball in CI. It is built on Rocky 8 so it doesn't have glibc compatibility issues with the ancient Linux distros that EDA tool vendors force us to use.

The way it finds the SAIL_DIR has changed. Instead of baking an absolute path in at build time, we get the path relative to the sail binary. This makes it portable and works for opam installs and for tarball downloads, and means you don't really need to worry about `opam var sail:share`.

Z3 is included for convenience, in a slightly hacky way just by copying z3 from PATH into the tarball.

The main dependency that is not included is libgmp. However this is required to actually use the C output anyway, and fortunately it is easy to install even on RHEL 8.

The CI action has to be run manually, and then it will upload the tarball as an artifact.

.github/workflows/release.yml

@@ -0,0 +1,116 @@
+name: Release tarball
+
+on: [workflow_dispatch]
+
+env:
+  OPAMVERBOSE: 1
+
+jobs:
+  build:
+    strategy:
+      matrix:
+        include:
+          - os: ubuntu-latest
+            container: rockylinux:8
+            ocaml_version: 5.0.0
+            opam_cache_key: rocky8-5.0.0
+
+    runs-on: ${{ matrix.os }}
+    container: ${{ matrix.container }}
+
+    env:
+      # Disable opam warning about running as root.
+      OPAMROOTISOK: 1
+
+    steps:
+    # This must be before checkout otherwise Github will use a zip of the
+    # code instead of git clone.
+    - name: System dependencies
+      run: |
+        dnf install --assumeyes \
+          gmp-devel \
+          pkg-config \
+          zlib-devel \
+          openssl \
+          curl \
+          git \
+          make \
+          unzip \
+          patch \
+          gcc \
+          gcc-c++ \
+          cmake \
+          bzip2 \
+          python3 \
+          findutils \
+          diffutils \
+          rsync \
+          which
+
+    - uses: actions/checkout@v4
+
+    # Retreive git history (but not files) so that `git desribe` works. This is
+    # used to set the version info in the compiler (printed by `sail --version`).
+    # The safe.directory command is needed because the current user does not
+    # own the git repo directory and that can be a security issue in some case
+    # (but not this one).
+    - name: Unshallow git history
+      run: |
+        git config --global --add safe.directory '*'
+        git fetch --unshallow --filter=tree:0
+
+    - name: Download OPAM
+      run: |
+        curl -L -o /usr/local/bin/opam https://github.com/ocaml/opam/releases/download/2.1.5/opam-2.1.5-i686-linux
+        chmod +x /usr/local/bin/opam
+
+    - name: Restore cached ~/.opam
+      id: cache-opam-restore
+      uses: actions/cache/restore@v4
+      with:
+        path: ~/.opam
+        key: ${{ matrix.opam_cache_key }}
+
+    - name: Init opam
+      if: steps.cache-opam-restore.outputs.cache-hit != 'true'
+      run: |
+        # Sandboxing doesn't work in Docker.
+        opam init --disable-sandboxing --yes --no-setup --shell=sh --compiler=${{ matrix.ocaml_version }} && \
+        eval "$(opam env)" && \
+        ocaml --version
+
+    - name: Save cached opam
+      if: steps.cache-opam-restore.outputs.cache-hit != 'true'
+      id: cache-opam-save
+      uses: actions/cache/save@v4
+      with:
+        path: ~/.opam
+        key: ${{ steps.cache-opam-restore.outputs.cache-primary-key }}
+
+    - name: Install Sail
+      run: |
+        eval $(opam env)
+        opam pin --yes --no-action add .
+        opam install sail --yes
+
+    # Build Z3 from source since the binary releases only support glibc 2.31
+    # and old distros like RHEL 8 have 2.28.
+    - name: Build Z3
+      run: |
+        git clone --depth 1 --branch z3-4.13.0 https://github.com/Z3Prover/z3.git
+        mkdir z3/build
+        cd z3/build
+        cmake -DCMAKE_BUILD_TYPE=Release ..
+        make -j4
+        make install
+
+    - name: Make release tarball
+      run: |
+        eval $(opam env)
+        make tarball TARBALL_EXTRA_BIN=$(which z3)
+
+    - name: Upload tarball
+      uses: actions/upload-artifact@v4
+      with:
+        name: sail
+        path: _build/sail.tar.gz

Makefile

@@ -10,6 +10,17 @@ sail:
 install: sail
 	dune install
 
+
+# Build binary tarball. The lib directory is very large and not needed
+# for running the compiler. TARBALL_EXTRA_BIN can be used to bundle z3.
+tarball: sail
+	dune install --relocatable --prefix=_build/tarball/sail
+	rm -rf _build/tarball/sail/lib
+ifdef TARBALL_EXTRA_BIN
+	cp $(TARBALL_EXTRA_BIN) _build/tarball/sail/bin/
+endif
+	tar czvf _build/sail.tar.gz -C _build/tarball sail
+
 coverage:
 	dune build --release --instrument-with bisect_ppx
 

src/bin/locations.ml

@@ -0,0 +1,17 @@
+(*
+Directory containing the lib and src directories. The most important is the
+lib directory which contains the standard library .sail files, e.g. `option.sail`
+and the C runtime files (`sail.c`, `rts.c`, etc).
+
+When installed by OPAM, Manifest.dir will be Some absolute_path so we just
+return that. When installed by dune we look relative to the location of
+the Sail binary. This allows it to be a portable installation which we make
+use of to provide a binary tarball.
+*)
+
+let sail_dir =
+  match Manifest.dir with
+  | Some opam_dir -> opam_dir
+  | None ->
+      let open Filename in
+      concat (concat (dirname Sys.executable_name) parent_dir_name) "share"

src/bin/manifest.ml.in

@@ -1,4 +1,13 @@
-let dir = "%{sail:share}%"
+(*
+This file is used to generate manifest.ml when you use OPAM to install Sail.
+If instead you use Dune then manifest.ml will not exist and Dune will use
+sail_manifest.ml to generate it.
+
+So in this file we use OPAM to find the share directory. In sail_manifest.ml
+we set `dir` to `None` so that Sail will look relative to the `sail` binary.
+*)
+
+let dir = Some "%{sail:share}%"
 
 let commit = "opam-v%{opam-version}% %{sail:version}%"
 

src/bin/repl.ml

@@ -105,13 +105,13 @@ let initial_istate config options env effect_info ast =
     ast;
     effect_info;
     env;
-    ref_state = ref (Interactive.initial_istate config Manifest.dir);
+    ref_state = ref (Interactive.initial_istate config Locations.sail_dir);
     vs_ids = ref (val_spec_ids ast.defs);
     options;
     mode = Normal;
     clear = true;
     state = initial_state ~registers:false empty_ast Type_check.initial_env !Value.primops;
-    default_sail_dir = Manifest.dir;
+    default_sail_dir = Locations.sail_dir;
     config;
   }
 

src/bin/sail.ml

@@ -420,7 +420,7 @@ let run_sail (config : Yojson.Basic.t option) tgt =
     | [], [] ->
         (* If there are no provided project files, we concatenate all
            the free file arguments into one big blob like before *)
-        Frontend.load_files ~target:tgt Manifest.dir !options Type_check.initial_env frees
+        Frontend.load_files ~target:tgt Locations.sail_dir !options Type_check.initial_env frees
     (* Allows project files from either free arguments via suffix, or
        from -project, but not both as the ordering between them would
        be unclear. *)
@@ -458,7 +458,7 @@ let run_sail (config : Yojson.Basic.t option) tgt =
         Profile.finish "parsing project" t;
         if !opt_just_parse_project then exit 0;
         let env = Type_check.initial_env_with_modules proj in
-        Frontend.load_modules ~target:tgt Manifest.dir !options env proj mod_ids
+        Frontend.load_modules ~target:tgt Locations.sail_dir !options env proj mod_ids
     | _, _ ->
         raise
           (Reporting.err_general Parse_ast.Unknown
@@ -477,7 +477,7 @@ let run_sail (config : Yojson.Basic.t option) tgt =
   Target.run_pre_rewrites_hook tgt ast effect_info env;
   let ast, effect_info, env = Rewrites.rewrite effect_info env (Target.rewrites tgt) ast in
 
-  Target.action tgt config Manifest.dir !opt_file_out ast effect_info env;
+  Target.action tgt config Locations.sail_dir !opt_file_out ast effect_info env;
 
   (ast, env, effect_info)
 
@@ -603,7 +603,7 @@ let main () =
     exit 0
   );
   if !opt_show_sail_dir then (
-    print_endline (Reporting.get_sail_dir Manifest.dir);
+    print_endline (Reporting.get_sail_dir Locations.sail_dir);
     exit 0
   );
 

src/sail_manifest/sail_manifest.ml

@@ -79,7 +79,8 @@ let git_command args =
   with _ -> None
 
 let gen_manifest () =
-  ksprintf print_endline "let dir = \"%s\"" (Sys.getcwd ());
+  (* See manifest.ml.in for more information about `dir`. *)
+  ksprintf print_endline "let dir = None";
   ksprintf print_endline "let commit = \"%s\"" (Option.value (git_command "rev-parse HEAD") ~default:"unknown commit");
   ksprintf print_endline "let branch = \"%s\""
     (Option.value (git_command "rev-parse --abbrev-ref HEAD") ~default:"unknown branch")