feat: Statically linked binary releases (OCamlPro#1045)

This patch modifies the Docker workflow to build a statically linked
portable binary of Alt-Ergo, following [1]. This also adds static builds
for macOS on both x86-64 and arm64 platforms.

Building the Linux binaries is fairly quick and hence performed on
push/pull_request. It can also be manually requested. macOS static
builds are much slower and can only be manually requested.

[1] : https://ocamlpro.com/blog/2021_09_02_generating_static_and_portable_executables_with_ocaml/

.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

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 ')'