Skip to content

Commit 611ccd5

Browse files
TimmmmTimmmm
committed
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.
1 parent 91dc2b3 commit 611ccd5

File tree

18 files changed

+389
-131
lines changed

18 files changed

+389
-131
lines changed

‎.github/workflows/build.yml‎

Lines changed: 51 additions & 31 deletions
Original file line numberDiff line numberDiff line change
@@ -2,69 +2,89 @@ name: Build matrix
22

33
on: [push, workflow_dispatch]
44

5+
# Required for vcpkg binary caching. See
6+
# https://learn.microsoft.com/en-us/vcpkg/github-integration
7+
permissions:
8+
contents: write
9+
510
env:
11+
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
12+
VCPKG_FEATURE_FLAGS: dependencygraph
613
OPAMVERBOSE: 1
714

815
jobs:
916
build:
1017
strategy:
1118
matrix:
12-
version: [4.08.1, 5.2.1]
13-
os: [ubuntu-latest, ubuntu-24.04-arm, macos-latest]
19+
ocaml_version: [4.08.1, 5.2.1]
20+
os: [ubuntu-24.04, ubuntu-24.04-arm, macos-26, windows-2025]
1421
exclude:
15-
- os: macos-latest
16-
version: 4.08.1
22+
- os: macos-26
23+
ocaml_version: 4.08.1
24+
# Windows is only supported by OCaml 5 or later.
25+
- os: windows-2025
26+
ocaml_version: 4.08.1
1727

1828
runs-on: ${{ matrix.os }}
1929

2030
steps:
2131
- uses: actions/checkout@v4
2232

23-
- name: System dependencies (ubuntu)
24-
if: startsWith(matrix.os, 'ubuntu')
25-
run: |
26-
sudo apt install build-essential libgmp-dev z3 cvc4 opam
33+
- name: System dependencies (Linux)
34+
if: runner.os == 'Linux'
35+
run: sudo apt install build-essential libgmp-dev cvc4
2736

2837
- name: System dependencies (macOS)
29-
if: startsWith(matrix.os, 'macos')
30-
run: |
31-
brew install --force --overwrite gpatch gmp z3 pkgconf opam
38+
if: runner.os == 'macOS'
39+
run: brew install --force --overwrite gpatch gmp pkgconf
3240

33-
- name: Restore cached opam
34-
id: cache-opam-restore
35-
uses: actions/cache/restore@v4
36-
with:
37-
path: ~/.opam
38-
key: ${{ matrix.os }}-${{ matrix.version }}
41+
- name: System dependencies (Windows)
42+
if: runner.os == 'Windows'
43+
run: vcpkg install gmp
3944

40-
- name: Setup opam
41-
if: steps.cache-opam-restore.outputs.cache-hit != 'true'
42-
run: |
43-
opam init --yes --no-setup --shell=sh --compiler=${{ matrix.version }}
45+
- name: Setup Z3
46+
id: z3
47+
uses: cda-tum/setup-z3@v1
48+
with:
49+
version: 4.15.3
4450

45-
- name: Save cached opam
46-
if: steps.cache-opam-restore.outputs.cache-hit != 'true'
47-
id: cache-opam-save
48-
uses: actions/cache/save@v4
51+
- name: Set-up OCaml
52+
uses: ocaml/setup-ocaml@v3
4953
with:
50-
path: ~/.opam
51-
key: ${{ steps.cache-opam-restore.outputs.cache-primary-key }}
54+
ocaml-compiler: ${{ matrix.ocaml_version }}
55+
56+
- name: Set LEMLIB env var
57+
if: runner.os == 'Windows'
58+
# Note we can't use `opam var lem:share` because lem hasn't been installed yet.
59+
run: echo "LEMLIB=$(opam var share)\lem\library" >> $env:GITHUB_ENV
60+
61+
# This contains a fix for paths on Windows but hasn't been released yet.
62+
- name: Pin latest linksem
63+
if: runner.os == 'Windows'
64+
run: opam pin add linksem https://github.com/rems-project/linksem.git
65+
66+
# Workaround for https://github.com/rems-project/lem/issues/38
67+
- name: Install and fix lem
68+
if: runner.os == 'Windows'
69+
run: |
70+
opam install lem
71+
Rename-Item -Path "$(opam var lem:bin)\lem" -NewName "lem.exe"
5272
5373
- name: Install Sail
5474
run: |
55-
eval $(opam env)
5675
opam pin --yes --no-action add .
5776
opam install sail --yes
5877
5978
- name: Test Sail
79+
# Tests use lots of unix-isms currently (fork, mkdir -p, etc).
80+
if: runner.os != 'Windows'
6081
run: |
61-
eval $(opam env)
62-
etc/ci_core_tests.sh
82+
opam exec -- bash etc/ci_core_tests.sh
6383
6484
build-docker:
6585
strategy:
6686
matrix:
67-
os: [ubuntu-latest, ubuntu-24.04-arm]
87+
os: [ubuntu-24.04, ubuntu-24.04-arm]
6888

6989
runs-on: ${{ matrix.os }}
7090

‎.github/workflows/release.yml‎

Lines changed: 62 additions & 49 deletions
Original file line numberDiff line numberDiff line change
@@ -15,36 +15,33 @@ jobs:
1515
matrix:
1616
include:
1717
- name: Linux-x86_64
18-
os: ubuntu-latest
18+
os: ubuntu-24.04
1919
container: rockylinux:8
2020
ocaml_version: 5.2.1
21-
opam_arch: i686
22-
opam_cache_key: rocky8-5.2.1
21+
tarball_filename: sail-Linux-x86_64.tar.gz
2322
- name: Linux-aarch64
2423
os: ubuntu-24.04-arm
2524
container: rockylinux:8
2625
ocaml_version: 5.2.1
27-
opam_arch: arm64
28-
opam_cache_key: rocky8-5.2.1-arm
26+
tarball_filename: sail-Linux-aarch64.tar.gz
2927
# MacOS disabled for now due to code signing and notarisation requirements
30-
# - name: mac-arm64 */
31-
# os: macos-latest */
32-
# container: "" */
33-
# ocaml_version: 5.2.1 */
34-
# opam_cache_key: macos-latest-5.2.1 */
28+
# - name: mac-arm64
29+
# os: macos-26
30+
# container: ""
31+
# ocaml_version: 5.2.1
32+
# tarball_filename: sail-Mac-arm64.tar.gz
33+
- name: Windows-x86_64
34+
os: windows-2025
35+
container: ""
36+
ocaml_version: 5.2.1
37+
tarball_filename: sail-Windows-AMD64.zip
3538

3639
runs-on: ${{ matrix.os }}
3740
container: ${{ matrix.container }}
3841

39-
env:
40-
# Disable opam warning about running as root.
41-
OPAMROOTISOK: 1
42-
4342
steps:
44-
# This must be before checkout otherwise Github will use a zip of the
45-
# code instead of git clone.
4643
- name: System dependencies (Linux)
47-
if: startsWith(matrix.os, 'ubuntu')
44+
if: runner.os == 'Linux'
4845
run: |
4946
dnf install --assumeyes \
5047
gmp-devel \
@@ -64,15 +61,20 @@ jobs:
6461
diffutils \
6562
rsync \
6663
which \
67-
cargo
68-
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
69-
chmod +x /usr/local/bin/opam
64+
cargo \
65+
bubblewrap
7066
71-
- name: System dependencies (Mac)
72-
if: startsWith(matrix.os, 'macos')
67+
- name: System dependencies (macOS)
68+
if: runner.os == 'macOS'
7369
run: |
74-
brew install --force --overwrite gpatch gmp z3 pkgconf opam git rust
70+
brew install --force --overwrite gpatch gmp pkgconf git rust
71+
72+
- name: System dependencies (Windows)
73+
if: runner.os == 'Windows'
74+
run: vcpkg install gmp
7575

76+
# This must be after git has been installed otherwise Github will use a zip
77+
# of the code instead of git clone.
7678
- uses: actions/checkout@v4
7779

7880
# Retreive git history (but not files) so that `git describe` works. This is
@@ -89,39 +91,45 @@ jobs:
8991
git config --global --add safe.directory '*'
9092
git fetch --unshallow
9193
92-
- name: Restore cached ~/.opam
93-
id: cache-opam-restore
94-
uses: actions/cache/restore@v4
94+
- name: Setup Z3
95+
id: z3
96+
uses: cda-tum/setup-z3@v1
9597
with:
96-
path: ~/.opam
97-
key: ${{ matrix.opam_cache_key }}
98+
version: 4.15.3
9899

99-
- name: Init opam
100-
if: steps.cache-opam-restore.outputs.cache-hit != 'true'
101-
run: |
102-
# Sandboxing doesn't work in Docker.
103-
opam init --disable-sandboxing --yes --no-setup --shell=sh --compiler=${{ matrix.ocaml_version }} && \
104-
eval "$(opam env)" && \
105-
ocaml --version
106-
107-
- name: Save cached opam
108-
if: steps.cache-opam-restore.outputs.cache-hit != 'true'
109-
id: cache-opam-save
110-
uses: actions/cache/save@v4
100+
# Note this must be after checkout otherwise it doesn't pin local packages
101+
# and create the default switch or something.
102+
- name: Set-up OCaml
103+
uses: ocaml/setup-ocaml@v3
111104
with:
112-
path: ~/.opam
113-
key: ${{ steps.cache-opam-restore.outputs.cache-primary-key }}
105+
ocaml-compiler: ${{ matrix.ocaml_version }}
106+
107+
- name: Set LEMLIB env var
108+
if: runner.os == 'Windows'
109+
# Note we can't use `opam var lem:share` because lem hasn't been installed yet.
110+
run: echo "LEMLIB=$(opam var share)\lem\library" >> $env:GITHUB_ENV
111+
112+
# This contains a fix for paths on Windows but hasn't been released yet.
113+
- name: Pin latest linksem
114+
if: runner.os == 'Windows'
115+
run: opam pin add linksem https://github.com/rems-project/linksem.git
116+
117+
# Workaround for https://github.com/rems-project/lem/issues/38
118+
- name: Install and fix lem
119+
if: runner.os == 'Windows'
120+
run: |
121+
opam install lem
122+
Rename-Item -Path "$(opam var lem:bin)\lem" -NewName "lem.exe"
114123
115124
- name: Install Sail
116125
run: |
117-
eval $(opam env)
118126
opam pin --yes --no-action add .
119127
opam install sail --yes
120128
121129
# Build Z3 from source since the binary releases only support glibc 2.31
122130
# and old distros like RHEL 8 have 2.28.
123131
- name: Build Z3
124-
if: startsWith(matrix.os, 'ubuntu')
132+
if: runner.os == 'Linux'
125133
run: |
126134
git clone --depth 1 --branch z3-4.13.0 https://github.com/Z3Prover/z3.git
127135
mkdir z3/build
@@ -130,17 +138,22 @@ jobs:
130138
make -j4
131139
make install
132140
133-
- name: Make release tarball
141+
- name: Make release tarball (Linux)
142+
if: runner.os == 'Linux'
143+
run: |
144+
opam exec -- make tarball Z3_EXE=z3/build/z3
145+
146+
- name: Make release tarball (Windows)
147+
if: runner.os == 'Windows'
134148
run: |
135-
eval $(opam env)
136-
make tarball TARBALL_EXTRA_BIN=z3/build/z3
149+
opam exec -- make tarball "Z3_EXE=$($(Get-Command z3).Source)" "GMP_DLL=$($(Get-Command libgmp-10.dll).Source)"
137150
138151
- uses: actions/attest-build-provenance@v1
139152
with:
140-
subject-path: _build/sail-${{ matrix.name }}.tar.gz
153+
subject-path: _build/${{ matrix.tarball_filename }}
141154

142155
- name: Upload tarball
143156
uses: actions/upload-artifact@v4
144157
with:
145158
name: sail-${{ matrix.name }}
146-
path: _build/sail-${{ matrix.name }}.tar.gz
159+
path: _build/${{ matrix.tarball_filename }}

‎.github/workflows/test-matrix.yml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -105,7 +105,7 @@ jobs:
105105
name: test-results-${{ matrix.suite }}
106106
path: |
107107
test/**/tests.xml
108-
test/suite-${{ matrix.suite }}.coverage
108+
test/suite-${{ matrix.suite }}.coverage
109109
110110
# Only do this for one job in the test matrix
111111
- name: Upload event payload

‎Makefile‎

Lines changed: 8 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -13,24 +13,23 @@ install: sail
1313
libsail_coverage:
1414
$(MAKE) -C lib/coverage
1515

16+
# TODO: Make this work on Windows.
1617
extraction:
1718
$(MAKE) -C src/lib/rocq
1819
mv src/lib/rocq/*.mli src/lib/extraction
1920
mv src/lib/rocq/*.ml src/lib/extraction
2021

2122
# Build binary tarball. The lib directory is very large and not needed
22-
# for running the compiler. TARBALL_EXTRA_BIN can be used to bundle z3.
23+
# for running the compiler. Z3_EXE can be used to bundle a z3 binary.
24+
# GMP_DLL can be used to bundle a libgmp DLL (this is only used on Windows currently).
2325
tarball: sail libsail_coverage
2426
dune install --relocatable --prefix=_build/tarball/sail
25-
rm -rf _build/tarball/sail/lib
26-
cp LICENSE _build/tarball/sail
27-
cp THIRD_PARTY_FILES.md _build/tarball/sail
28-
cp -a etc/tarball_extra/. _build/tarball/sail
29-
ifdef TARBALL_EXTRA_BIN
30-
cp $(TARBALL_EXTRA_BIN) _build/tarball/sail/bin/
31-
endif
32-
cp lib/coverage/libsail_coverage.a _build/tarball/sail/share/sail/lib/coverage/
27+
dune exec -- sail_maker tarball --prefix=_build/tarball/sail --z3=$(Z3_EXE) --gmp=$(GMP_DLL)
28+
ifeq ($(OS),Windows_NT)
29+
powershell Compress-Archive -Path "_build/tarball/sail" -DestinationPath "_build/sail-Windows-$(PROCESSOR_ARCHITECTURE).zip" -Force
30+
else
3331
tar czvf _build/sail-$(shell uname -s)-$(shell uname -m).tar.gz -C _build/tarball sail
32+
endif
3433

3534
coverage:
3635
dune build --release --instrument-with bisect_ppx

‎dune-project‎

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -31,7 +31,7 @@
3131

3232
(package
3333
(synopsis "Helper tool for compiling Sail")
34-
(name sail_manifest)
34+
(name sail_maker)
3535
(depends
3636
(ocaml (>= 4.08.1))))
3737

@@ -139,7 +139,7 @@ http://www.cl.cam.ac.uk/~pes20/sail/.
139139
")
140140
(depends
141141
(libsail (= :version))
142-
(sail_manifest (and (= :version) :build))
142+
(sail_maker (and (= :version) :build))
143143
(sail_ocaml_backend (and (= :version) :post))
144144
(sail_c_backend (and (= :version) :post))
145145
(sail_smt_backend (and (= :version) :post))
@@ -150,4 +150,7 @@ http://www.cl.cam.ac.uk/~pes20/sail/.
150150
(sail_latex_backend (and (= :version) :post))
151151
(sail_doc_backend (and (= :version) :post))
152152
(sail_output (and (= :version) :post))
153-
(linenoise (>= 1.1.0))))
153+
; linenoise needs termios.h and some other headers that are not available
154+
; on windows (at least without installing extra cygwin packages which
155+
; is tricky).
156+
(linenoise (and (>= 1.1.0) (<> :os "win32")))))

‎lib/coverage/Makefile‎

Lines changed: 7 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,8 @@
1-
libsail_coverage.a: src/*.rs Cargo.toml Makefile
1+
ifeq ($(OS),Windows_NT)
2+
LIB_NAME = sail_coverage.lib
3+
else
4+
LIB_NAME = libsail_coverage.a
5+
endif
6+
7+
target/release/$(LIB_NAME): src/*.rs Cargo.toml Makefile
28
cargo build --release
3-
cp target/release/libsail_coverage.a .

‎sail.opam‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -32,7 +32,7 @@ bug-reports: "https://github.com/rems-project/sail/issues"
3232
depends: [
3333
"dune" {>= "3.11"}
3434
"libsail" {= version}
35-
"sail_manifest" {= version & build}
35+
"sail_maker" {= version & build}
3636
"sail_ocaml_backend" {= version & post}
3737
"sail_c_backend" {= version & post}
3838
"sail_smt_backend" {= version & post}
@@ -43,7 +43,7 @@ depends: [
4343
"sail_latex_backend" {= version & post}
4444
"sail_doc_backend" {= version & post}
4545
"sail_output" {= version & post}
46-
"linenoise" {>= "1.1.0"}
46+
"linenoise" {>= "1.1.0" & os != "win32"}
4747
"odoc" {with-doc}
4848
]
4949
build: [

‎sail_manifest.opam‎ renamed to ‎sail_maker.opam‎

File renamed without changes.

0 commit comments

Comments
 (0)