-
Notifications
You must be signed in to change notification settings - Fork 33
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
feat: Statically linked binary releases
This patch modifies the Docker workflow to build a statically linked portable binary of Alt-Ergo, following [1]. The workflow also now builds statically linked macOS binaries for x86-64 and arm64 platforms. Building the Linux binaries is fairly quick and hence performed on push/pull_request. On the other hand, the macOS build is fairly slow, and only performed when manually requested. [1] : https://ocamlpro.com/blog/2021_09_02_generating_static_and_portable_executables_with_ocaml/
- Loading branch information
1 parent
8c188f1
commit d3ed734
Showing
5 changed files
with
152 additions
and
51 deletions.
There are no files selected for viewing
This file was deleted.
Oops, something went wrong.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,94 @@ | ||
name: Build statically linked binaries | ||
|
||
on: | ||
workflow_dispatch: | ||
pull_request: | ||
push: | ||
branches: | ||
- next | ||
- main | ||
|
||
jobs: | ||
macos-static: | ||
name: Build statically linked macOS binaries | ||
# Only do this when explicitly requested since it takes a long time to | ||
# build on macOS; no need to waste resources | ||
if: ${{ github.event_name == 'workflow_dispatch' }} | ||
strategy: | ||
matrix: | ||
include: | ||
- arch: x86_64 | ||
os: macos-12 | ||
- arch: aarch64 | ||
os: macos-14 | ||
|
||
runs-on: ${{ matrix.os }} | ||
|
||
steps: | ||
- uses: actions/checkout@v4 | ||
with: | ||
persist-credentials: false | ||
|
||
- uses: ocaml/setup-ocaml@v2 | ||
with: | ||
allow-prerelease-opam: true | ||
ocaml-compiler: 4.14.1 | ||
dune-cache: true | ||
|
||
- run: opam install . --locked --deps-only --ignore-constraints-on alt-ergo-lib,alt-ergo-parsers | ||
|
||
- run: opam exec -- dune subst | ||
|
||
- run: LINK_MODE=mixed opam exec -- dune build --release src/bin/text/Main_text.exe | ||
|
||
- run: cp src/bin/text/Main_text.exe src/bin/text/alt-ergo | ||
|
||
- uses: actions/upload-artifact@v4 | ||
with: | ||
name: alt-ergo-${{ matrix.arch }}-macos | ||
path: src/bin/text/alt-ergo | ||
|
||
musl: | ||
name: Build statically linked binary with musl | ||
|
||
runs-on: ubuntu-latest | ||
|
||
# Retrieve and use a light docker container on which ocaml 4.10 is installed | ||
# as a system compiler. This container also contains opam 2.1. | ||
container: | ||
image: ocamlpro/ocaml:4.14 | ||
options: --user root | ||
|
||
steps: | ||
|
||
- name: Checkout code | ||
uses: actions/checkout@v4 | ||
|
||
- name: Switch to ocaml user | ||
run: su ocaml | ||
|
||
# This line is needed to acces and use opam. We are unable to set the user | ||
# to `ocaml` with the container parameters | ||
- run: sudo chmod a+wx . | ||
|
||
# This line is needed to allow the working directory to be used even | ||
# the ocaml user do not have rights on it. | ||
- run: CURRENTDIR=$(basename $(pwd)); git config --global --add safe.directory /__w/$CURRENTDIR/$CURRENTDIR | ||
|
||
- name: Install static dependencies | ||
run: sudo apk add zlib-static | ||
|
||
# Create a switch with the system compiler (no compilation needed). | ||
# This installs external (no need for depext with opam 2.1) and libs deps. | ||
- run: opam switch create . ocaml-system --locked --deps-only --ignore-constraints-on alt-ergo-lib,alt-ergo-parsers | ||
|
||
- run: opam exec -- dune subst | ||
- name: Build statically linked binary | ||
run: LINK_MODE=static opam exec -- dune build --release src/bin/text/Main_text.exe | ||
|
||
- run: cp src/bin/text/Main_text.exe src/bin/text/alt-ergo | ||
|
||
- uses: actions/upload-artifact@v4 | ||
with: | ||
name: alt-ergo-x86_64-linux-musl | ||
path: src/bin/text/alt-ergo |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file was deleted.
Oops, something went wrong.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,53 @@ | ||
#!/bin/sh | ||
|
||
set -ue | ||
|
||
LINK_MODE="$1" | ||
OS="$2" | ||
FLAGS= | ||
CCLIB= | ||
|
||
case "$LINK_MODE" in | ||
dynamic) | ||
;; # No extra flags needed | ||
static) | ||
case "$OS" in | ||
linux) | ||
CCLIB="-static -no-pie";; | ||
*) | ||
echo "No known static compilation flags for '$OS'" >&2 | ||
exit 1 | ||
esac;; | ||
mixed) | ||
FLAGS="-noautolink" | ||
CCLIB="-lstdcompat_stubs -lcamlzip -lnums -lzarith -lcamlstr -lunix -lz" | ||
LIBS="gmp" | ||
case "$OS" in | ||
linux) | ||
for lib in $LIBS; do | ||
CCLIB="$CCLIB -l$lib" | ||
done;; | ||
macosx) | ||
for lib in $LIBS; do | ||
if [[ $lib == lib* ]]; then | ||
archive="$lib.a" | ||
else | ||
archive="lib$lib.a" | ||
fi | ||
CCLIB="$CCLIB $(pkg-config $lib --variable libdir)/$archive" | ||
done;; | ||
*) | ||
echo "No known mixed compilation flags for '$OS'" >&2 | ||
exit 1 | ||
esac;; | ||
|
||
*) | ||
echo "Invalid link mode '$LINK_MODE'" >&2 | ||
exit 2 | ||
esac | ||
|
||
echo '(' | ||
echo ' -linkall' | ||
for f in $FLAGS; do echo " $f"; done | ||
for f in $CCLIB; do echo " -cclib $f"; done | ||
echo ')' |