Support Windows compilation by disabling the REPL on Windows

This also currently includes some incidental CI improvements that I made when trying to punch Github CI in the face until it worked:

* Use explicit `os` versions
* Use `runner.os ==` instead of `startswith(matrix.os`
* Use the `setup-z3` action to set up Z3
* Use the `setup-ocaml` action. This includes caching.

Also some of the tarball generation logic is moved from the Makefile into `sail_maker` (OCaml) because it's difficult to make portable Makefiles.

Author: Timmmm

.github/workflows/build.yml

@@ -2,69 +2,89 @@ name: Build matrix
 
 on: [push, workflow_dispatch]
 
+# Required for vcpkg binary caching. See
+# https://learn.microsoft.com/en-us/vcpkg/github-integration
+permissions:
+  contents: write
+
 env:
+  GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+  VCPKG_FEATURE_FLAGS: dependencygraph
   OPAMVERBOSE: 1
 
 jobs:
   build:
     strategy:
       matrix:
-        version: [4.08.1, 5.2.1]
-        os: [ubuntu-latest, ubuntu-24.04-arm, macos-latest]
+        ocaml_version: [4.08.1, 5.2.1]
+        os: [ubuntu-24.04, ubuntu-24.04-arm, macos-26, windows-2025]
         exclude:
-        - os: macos-latest
-          version: 4.08.1
+        - os: macos-26
+          ocaml_version: 4.08.1
+        # Windows is only supported by OCaml 5 or later.
+        - os: windows-2025
+          ocaml_version: 4.08.1
 
     runs-on: ${{ matrix.os }}
 
     steps:
     - uses: actions/checkout@v4
 
-    - name: System dependencies (ubuntu)
-      if: startsWith(matrix.os, 'ubuntu')
-      run: |
-        sudo apt install build-essential libgmp-dev z3 cvc4 opam
+    - name: System dependencies (Linux)
+      if: runner.os == 'Linux'
+      run: sudo apt install build-essential libgmp-dev cvc4
 
     - name: System dependencies (macOS)
-      if: startsWith(matrix.os, 'macos')
-      run: |
-        brew install --force --overwrite gpatch gmp z3 pkgconf opam
+      if: runner.os == 'macOS'
+      run: brew install --force --overwrite gpatch gmp pkgconf
 
-    - name: Restore cached opam
-      id: cache-opam-restore
-      uses: actions/cache/restore@v4
-      with:
-        path: ~/.opam
-        key: ${{ matrix.os }}-${{ matrix.version }}
+    - name: System dependencies (Windows)
+      if: runner.os == 'Windows'
+      run: vcpkg install gmp
 
-    - name: Setup opam
-      if: steps.cache-opam-restore.outputs.cache-hit != 'true'
-      run: |
-        opam init --yes --no-setup --shell=sh --compiler=${{ matrix.version }}
+    - name: Setup Z3
+      id: z3
+      uses: cda-tum/setup-z3@v1
+      with:
+        version: 4.15.3
 
-    - name: Save cached opam
-      if: steps.cache-opam-restore.outputs.cache-hit != 'true'
-      id: cache-opam-save
-      uses: actions/cache/save@v4
+    - name: Set-up OCaml
+      uses: ocaml/setup-ocaml@v3
       with:
-        path: ~/.opam
-        key: ${{ steps.cache-opam-restore.outputs.cache-primary-key }}
+        ocaml-compiler: ${{ matrix.ocaml_version }}
+
+    - name: Set LEMLIB env var
+      if: runner.os == 'Windows'
+      # Note we can't use `opam var lem:share` because lem hasn't been installed yet.
+      run: echo "LEMLIB=$(opam var share)\lem\library" >> $env:GITHUB_ENV
+
+    # This contains a fix for paths on Windows but hasn't been released yet.
+    - name: Pin latest linksem
+      if: runner.os == 'Windows'
+      run: opam pin add linksem https://github.com/rems-project/linksem.git
+
+    # Workaround for https://github.com/rems-project/lem/issues/38
+    - name: Install and fix lem
+      if: runner.os == 'Windows'
+      run: |
+        opam install lem
+        Rename-Item -Path "$(opam var lem:bin)\lem" -NewName "lem.exe"
 
     - name: Install Sail
       run: |
-        eval $(opam env)
         opam pin --yes --no-action add .
         opam install sail --yes
 
     - name: Test Sail
+      # Tests use lots of unix-isms currently (fork, mkdir -p, etc).
+      if: runner.os != 'Windows'
       run: |
-        eval $(opam env)
-        etc/ci_core_tests.sh
+        opam exec -- bash etc/ci_core_tests.sh
 
   build-docker:
     strategy:
       matrix:
-        os: [ubuntu-latest, ubuntu-24.04-arm]
+        os: [ubuntu-24.04, ubuntu-24.04-arm]
 
     runs-on: ${{ matrix.os }}
 

.github/workflows/release.yml

@@ -15,36 +15,33 @@ jobs:
       matrix:
         include:
           - name: Linux-x86_64
-            os: ubuntu-latest
+            os: ubuntu-24.04
             container: rockylinux:8
             ocaml_version: 5.2.1
-            opam_arch: i686
-            opam_cache_key: rocky8-5.2.1
+            tarball_filename: sail-Linux-x86_64.tar.gz
           - name: Linux-aarch64
             os: ubuntu-24.04-arm
             container: rockylinux:8
             ocaml_version: 5.2.1
-            opam_arch: arm64
-            opam_cache_key: rocky8-5.2.1-arm
+            tarball_filename: sail-Linux-aarch64.tar.gz
           # MacOS disabled for now due to code signing and notarisation requirements
-          # - name: mac-arm64 */
-          #   os: macos-latest */
-          #   container: "" */
-          #   ocaml_version: 5.2.1 */
-          #   opam_cache_key: macos-latest-5.2.1 */
+          # - name: mac-arm64
+          #   os: macos-26
+          #   container: ""
+          #   ocaml_version: 5.2.1
+          #   tarball_filename: sail-Mac-arm64.tar.gz
+          - name: Windows-x86_64
+            os: windows-2025
+            container: ""
+            ocaml_version: 5.2.1
+            tarball_filename: sail-Windows-AMD64.zip
 
     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 (Linux)
-      if: startsWith(matrix.os, 'ubuntu')
+      if: runner.os == 'Linux'
       run: |
         dnf install --assumeyes \
           gmp-devel \
@@ -64,15 +61,20 @@ jobs:
           diffutils \
           rsync \
           which \
-          cargo
-        curl -L -o /usr/local/bin/opam https://github.com/ocaml/opam/releases/download/2.1.5/opam-2.1.5-${{ matrix.opam_arch }}-linux
-        chmod +x /usr/local/bin/opam
+          cargo \
+          bubblewrap
 
-    - name: System dependencies (Mac)
-      if: startsWith(matrix.os, 'macos')
+    - name: System dependencies (macOS)
+      if: runner.os == 'macOS'
       run: |
-        brew install --force --overwrite gpatch gmp z3 pkgconf opam git rust
+        brew install --force --overwrite gpatch gmp pkgconf git rust
+
+    - name: System dependencies (Windows)
+      if: runner.os == 'Windows'
+      run: vcpkg install gmp
 
+    # This must be after git has been installed otherwise Github will use a zip
+    # of the code instead of git clone.
     - uses: actions/checkout@v4
 
     # Retreive git history (but not files) so that `git describe` works. This is
@@ -89,39 +91,45 @@ jobs:
         git config --global --add safe.directory '*'
         git fetch --unshallow
 
-    - name: Restore cached ~/.opam
-      id: cache-opam-restore
-      uses: actions/cache/restore@v4
+    - name: Setup Z3
+      id: z3
+      uses: cda-tum/setup-z3@v1
       with:
-        path: ~/.opam
-        key: ${{ matrix.opam_cache_key }}
+        version: 4.15.3
 
-    - 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
+    # Note this must be after checkout otherwise it doesn't pin local packages
+    # and create the default switch or something.
+    - name: Set-up OCaml
+      uses: ocaml/setup-ocaml@v3
       with:
-        path: ~/.opam
-        key: ${{ steps.cache-opam-restore.outputs.cache-primary-key }}
+        ocaml-compiler: ${{ matrix.ocaml_version }}
+
+    - name: Set LEMLIB env var
+      if: runner.os == 'Windows'
+      # Note we can't use `opam var lem:share` because lem hasn't been installed yet.
+      run: echo "LEMLIB=$(opam var share)\lem\library" >> $env:GITHUB_ENV
+
+    # This contains a fix for paths on Windows but hasn't been released yet.
+    - name: Pin latest linksem
+      if: runner.os == 'Windows'
+      run: opam pin add linksem https://github.com/rems-project/linksem.git
+
+    # Workaround for https://github.com/rems-project/lem/issues/38
+    - name: Install and fix lem
+      if: runner.os == 'Windows'
+      run: |
+        opam install lem
+        Rename-Item -Path "$(opam var lem:bin)\lem" -NewName "lem.exe"
 
     - 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
-      if: startsWith(matrix.os, 'ubuntu')
+      if: runner.os == 'Linux'
       run: |
         git clone --depth 1 --branch z3-4.13.0 https://github.com/Z3Prover/z3.git
         mkdir z3/build
@@ -130,17 +138,22 @@ jobs:
         make -j4
         make install
 
-    - name: Make release tarball
+    - name: Make release tarball (Linux)
+      if: runner.os == 'Linux'
+      run: |
+        opam exec -- make tarball Z3_EXE=z3/build/z3
+
+    - name: Make release tarball (Windows)
+      if: runner.os == 'Windows'
       run: |
-        eval $(opam env)
-        make tarball TARBALL_EXTRA_BIN=z3/build/z3
+        opam exec -- make tarball "Z3_EXE=$($(Get-Command z3).Source)" "GMP_DLL=$($(Get-Command libgmp-10.dll).Source)"
 
     - uses: actions/attest-build-provenance@v1
       with:
-        subject-path: _build/sail-${{ matrix.name }}.tar.gz
+        subject-path: _build/${{ matrix.tarball_filename }}
 
     - name: Upload tarball
       uses: actions/upload-artifact@v4
       with:
         name: sail-${{ matrix.name }}
-        path: _build/sail-${{ matrix.name }}.tar.gz
+        path: _build/${{ matrix.tarball_filename }}

.github/workflows/test-matrix.yml

@@ -105,7 +105,7 @@ jobs:
         name: test-results-${{ matrix.suite }}
         path: |
           test/**/tests.xml
-          test/suite-${{ matrix.suite }}.coverage 
+          test/suite-${{ matrix.suite }}.coverage
 
     # Only do this for one job in the test matrix
     - name: Upload event payload

.gitignore

@@ -50,7 +50,6 @@ lib/hol/sail-heap
 # Sail coverage
 /lib/coverage/Cargo.lock
 /lib/coverage/target
-/lib/coverage/libsail_coverage.a
 /sailcov/sailcov
 
 # location specific things

Makefile

@@ -13,24 +13,23 @@ install: sail
 libsail_coverage:
 	$(MAKE) -C lib/coverage
 
+# TODO: Make this work on Windows.
 extraction:
 	$(MAKE) -C src/lib/rocq
 	mv src/lib/rocq/*.mli src/lib/extraction
 	mv src/lib/rocq/*.ml src/lib/extraction
 
 # 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.
+# for running the compiler. Z3_EXE can be used to bundle a z3 binary.
+# GMP_DLL can be used to bundle a libgmp DLL (this is only used on Windows currently).
 tarball: sail libsail_coverage
 	dune install --relocatable --prefix=_build/tarball/sail
-	rm -rf _build/tarball/sail/lib
-	cp LICENSE _build/tarball/sail
-	cp THIRD_PARTY_FILES.md _build/tarball/sail
-	cp -a etc/tarball_extra/. _build/tarball/sail
-ifdef TARBALL_EXTRA_BIN
-	cp $(TARBALL_EXTRA_BIN) _build/tarball/sail/bin/
-endif
-	cp lib/coverage/libsail_coverage.a _build/tarball/sail/share/sail/lib/coverage/
+	dune exec -- sail_maker tarball --prefix=_build/tarball/sail --z3=$(Z3_EXE) --gmp=$(GMP_DLL)
+ifeq ($(OS),Windows_NT)
+	powershell Compress-Archive -Path "_build/tarball/sail" -DestinationPath "_build/sail-Windows-$(PROCESSOR_ARCHITECTURE).zip" -Force
+else
 	tar czvf _build/sail-$(shell uname -s)-$(shell uname -m).tar.gz -C _build/tarball sail
+endif
 
 coverage:
 	dune build --release --instrument-with bisect_ppx

dune-project

@@ -31,7 +31,7 @@
 
 (package
   (synopsis "Helper tool for compiling Sail")
-  (name sail_manifest)
+  (name sail_maker)
   (depends
     (ocaml (>= 4.08.1))))
 
@@ -139,7 +139,7 @@ http://www.cl.cam.ac.uk/~pes20/sail/.
 ")
   (depends
     (libsail (= :version))
-    (sail_manifest (and (= :version) :build))
+    (sail_maker (and (= :version) :build))
     (sail_ocaml_backend (and (= :version) :post))
     (sail_c_backend (and (= :version) :post))
     (sail_smt_backend (and (= :version) :post))
@@ -150,4 +150,7 @@ http://www.cl.cam.ac.uk/~pes20/sail/.
     (sail_latex_backend (and (= :version) :post))
     (sail_doc_backend (and (= :version) :post))
     (sail_output (and (= :version) :post))
-    (linenoise (>= 1.1.0))))
+    ; linenoise needs termios.h and some other headers that are not available
+    ; on windows (at least without installing extra cygwin packages which
+    ; is tricky).
+    (linenoise (and (>= 1.1.0) (<> :os "win32")))))

lib/coverage/Makefile

@@ -1,3 +1,8 @@
-libsail_coverage.a: src/*.rs Cargo.toml Makefile
+ifeq ($(OS),Windows_NT)
+    LIB_NAME = sail_coverage.lib
+else
+    LIB_NAME = libsail_coverage.a
+endif
+
+target/release/$(LIB_NAME): src/*.rs Cargo.toml Makefile
 	cargo build --release
-	cp target/release/libsail_coverage.a .

sail.opam

@@ -32,7 +32,7 @@ bug-reports: "https://github.com/rems-project/sail/issues"
 depends: [
   "dune" {>= "3.11"}
   "libsail" {= version}
-  "sail_manifest" {= version & build}
+  "sail_maker" {= version & build}
   "sail_ocaml_backend" {= version & post}
   "sail_c_backend" {= version & post}
   "sail_smt_backend" {= version & post}
@@ -43,7 +43,7 @@ depends: [
   "sail_latex_backend" {= version & post}
   "sail_doc_backend" {= version & post}
   "sail_output" {= version & post}
-  "linenoise" {>= "1.1.0"}
+  "linenoise" {>= "1.1.0" & os != "win32"}
   "odoc" {with-doc}
 ]
 build: [