WIP: macOS static binaries

.dockerignore

@@ -0,0 +1 @@
+bin/

.github/workflows/build_static.yml

@@ -0,0 +1,97 @@
+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: opam exec -- dune build --release @install --promote-install-files false
+        env:
+          LINK_MODE: mixed
+
+      - run: opam exec -- dune install -p alt-ergo --create-install-files --prefix opt/alt-ergo --relocatable
+
+      - uses: actions/upload-artifact@v4
+        with:
+          name: alt-ergo-${{ matrix.arch }}-macos
+          path: _destdir/opt/alt-ergo/bin/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.14 is installed
+    # as a system compiler. This container also contains opam 2.1.
+    container:
+      image: ocamlpro/ocaml:4.14-flambda
+      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
+
+      - 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: opam exec -- dune build --release @install --promote-install-files false
+        env:
+          LINK_MODE: static
+
+      - run: opam exec -- dune install -p alt-ergo --create-install-files --prefix opt/alt-ergo --relocatable
+
+      - uses: actions/upload-artifact@v4
+        with:
+          name: alt-ergo-x86_64-linux-musl
+          path: _destdir/opt/alt-ergo/bin/alt-ergo

Dockerfile

@@ -0,0 +1,39 @@
+FROM quay.io/pypa/manylinux_2_28_x86_64 AS compilation
+
+# Enable Devel repo (for gmp-static)
+RUN dnf -y install almalinux-release-devel
+
+# Install config-manager command (for enabling PowerTools repo)
+RUN dnf -y install 'dnf-command(config-manager)'
+
+# Enable PowerTools repo (for zlib-static)
+RUN dnf config-manager --set-enabled powertools
+
+RUN dnf -y install gmp-static zlib-static make patch unzip
+
+ADD https://github.com/ocaml/opam/releases/download/2.2.0-beta1/opam-2.2.0-beta1-x86_64-linux /bin/opam
+
+RUN chmod +x /bin/opam
+
+RUN opam init -a --bare --disable-sandboxing
+
+COPY . /src/alt-ergo
+
+WORKDIR /src/alt-ergo
+
+ENV OPAMYES 1
+ENV OPAMDEPEXTYES 1
+ENV OPAMCONFIRMLEVEL unsafe-yes
+ENV OPAMERRLOGLEN 0
+
+RUN opam switch create . 4.14.1 --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 @install
+
+RUN opam exec -- dune install --relocatable --prefix /opt/alt-ergo/
+
+FROM scratch AS alt-ergo
+COPY --from=compilation /opt/alt-ergo/ /opt/alt-ergo/
+ENTRYPOINT [ "/opt/alt-ergo/bin/alt-ergo" ]

src/bin/text/dune

@@ -1,12 +1,16 @@
 (documentation
   (package alt-ergo))
 
+(rule
+ (with-stdout-to link_flags.dune
+  (run ./gen-link-flags.sh %{env:LINK_MODE=dynamic} %{ocaml-config:system})))
+
 (executable
   (name Main_text)
   (public_name alt-ergo)
   (package alt-ergo)
   (libraries alt_ergo_common)
-  (link_flags (:include flags.dune))
+  (link_flags (:standard (:include link_flags.dune)))
   (modules Main_text)
   (promote (until-clean)))
 

src/bin/text/gen-link-flags.sh

@@ -0,0 +1,56 @@
+#!/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"
+    # Note: for OCaml 5, use -lcamlstrnat and -lunixnat and mind zlib
+    # https://github.com/ocaml/ocaml/issues/12562
+    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
+	CCLIB="-Wl,-Bstatic $CCLIB -Wl,-Bdynamic";;
+      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 ')'