diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml new file mode 100644 index 000000000..8bc8bbc35 --- /dev/null +++ b/.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 diff --git a/Makefile b/Makefile index 38f2562ca..1def00f29 100644 --- a/Makefile +++ b/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 diff --git a/src/bin/locations.ml b/src/bin/locations.ml new file mode 100644 index 000000000..d1aa3df0b --- /dev/null +++ b/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" diff --git a/src/bin/manifest.ml.in b/src/bin/manifest.ml.in index e641faaf2..659b10ce1 100644 --- a/src/bin/manifest.ml.in +++ b/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}%" diff --git a/src/bin/repl.ml b/src/bin/repl.ml index 935245dfc..236504654 100644 --- a/src/bin/repl.ml +++ b/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; } diff --git a/src/bin/sail.ml b/src/bin/sail.ml index 7c356cfb7..61ab7c927 100644 --- a/src/bin/sail.ml +++ b/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 ); diff --git a/src/sail_manifest/sail_manifest.ml b/src/sail_manifest/sail_manifest.ml index e752fedcb..27d82df51 100644 --- a/src/sail_manifest/sail_manifest.ml +++ b/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")