From aa09d3de2dfc585410dd8486cc17d87587cc0381 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= Date: Thu, 22 Feb 2024 09:25:59 +0100 Subject: [PATCH 01/10] 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/ --- .github/workflows/build_docker.yml | 49 ---------------- .github/workflows/build_static.yml | 90 ++++++++++++++++++++++++++++++ src/bin/text/dune | 6 +- src/bin/text/flags.dune | 1 - src/bin/text/gen-link-flags.sh | 53 ++++++++++++++++++ 5 files changed, 148 insertions(+), 51 deletions(-) delete mode 100644 .github/workflows/build_docker.yml create mode 100644 .github/workflows/build_static.yml delete mode 100644 src/bin/text/flags.dune create mode 100755 src/bin/text/gen-link-flags.sh diff --git a/.github/workflows/build_docker.yml b/.github/workflows/build_docker.yml deleted file mode 100644 index 14b7d596a..000000000 --- a/.github/workflows/build_docker.yml +++ /dev/null @@ -1,49 +0,0 @@ -name: Build with ocp Docker container - -# The goal of this workflow is to test the installation of the project with opam -# on a specific light docker container instead of using default GH-actions one. -on: - push: - branches: - - fix-ci - - next - - main - -jobs: - install_docker: - name: opam install on a specific docker container - - 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.10 - options: --user root - - steps: - - # Checkout the code of the current branch - - name: Checkout code - uses: actions/checkout@v4 - - # 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: Update opam repository - run: opam update - - # Create a switch with the system compiler (no compilation needed). - # And then, install 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 - - # Install the project packages - - run: opam install . --locked diff --git a/.github/workflows/build_static.yml b/.github/workflows/build_static.yml new file mode 100644 index 000000000..21de66762 --- /dev/null +++ b/.github/workflows/build_static.yml @@ -0,0 +1,90 @@ +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 + + - 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 diff --git a/src/bin/text/dune b/src/bin/text/dune index 861dafd17..793e68dc2 100644 --- a/src/bin/text/dune +++ b/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))) diff --git a/src/bin/text/flags.dune b/src/bin/text/flags.dune deleted file mode 100644 index 4c6083a40..000000000 --- a/src/bin/text/flags.dune +++ /dev/null @@ -1 +0,0 @@ -(-linkall) diff --git a/src/bin/text/gen-link-flags.sh b/src/bin/text/gen-link-flags.sh new file mode 100755 index 000000000..1e23263fd --- /dev/null +++ b/src/bin/text/gen-link-flags.sh @@ -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 ')' From ee897a3144286925c86487255696af9a16087b61 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= Date: Fri, 23 Feb 2024 11:51:42 +0100 Subject: [PATCH 02/10] WIP: Docker --- Dockerfile | 15 +++++++++++++++ 1 file changed, 15 insertions(+) create mode 100644 Dockerfile diff --git a/Dockerfile b/Dockerfile new file mode 100644 index 000000000..04fddba9d --- /dev/null +++ b/Dockerfile @@ -0,0 +1,15 @@ +FROM ocamlpro/ocaml:4.14 + +USER ocaml + +RUN sudo apk add zlib-static + +COPY . . + +RUN sudo chmod a+wx . + +RUN opam switch create . ocaml-system --locked --deps-only --ignore-constraints-on alt-ergo-lib,alt-ergo-parsers + +RUN opam exec -- dune subst + +RUN LINK_MODE=static opam exec -- dune build --release src/bin/text/Main_text.exe From 1e599bc7b2f7670a088930b858fa03b0b56c134a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= Date: Mon, 4 Mar 2024 10:57:43 +0100 Subject: [PATCH 03/10] WIP WIP --- .dockerignore | 1 + Dockerfile | 47 +++++++++++++++++++++++++++++----- src/bin/text/gen-link-flags.sh | 3 ++- 3 files changed, 43 insertions(+), 8 deletions(-) create mode 100644 .dockerignore diff --git a/.dockerignore b/.dockerignore new file mode 100644 index 000000000..e660fd93d --- /dev/null +++ b/.dockerignore @@ -0,0 +1 @@ +bin/ diff --git a/Dockerfile b/Dockerfile index 04fddba9d..ab0881f79 100644 --- a/Dockerfile +++ b/Dockerfile @@ -1,15 +1,48 @@ -FROM ocamlpro/ocaml:4.14 +FROM quay.io/pypa/manylinux_2_28_aarch64 AS compilation -USER ocaml +ADD https://github.com/ocaml/opam/releases/download/2.2.0-beta1/opam-2.2.0-beta1-arm64-linux /bin/opam -RUN sudo apk add zlib-static +RUN chmod +x /bin/opam -COPY . . +RUN opam init -a --bare --disable-sandboxing -RUN sudo chmod a+wx . +COPY . /src/alt-ergo -RUN opam switch create . ocaml-system --locked --deps-only --ignore-constraints-on alt-ergo-lib,alt-ergo-parsers +WORKDIR /src/alt-ergo + +ENV OPAMYES 1 +ENV OPAMDEPEXTYES 1 +ENV OPAMCONFIRMLEVEL unsafe-yes +ENV OPAMERRLOGLEN 0 + +RUN yum -y install gmp-static zlib-static + +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=static opam exec -- dune build --release src/bin/text/Main_text.exe +RUN LINK_MODE=mixed opam exec -- dune build --release src/bin/text/Main_text.exe + +FROM scratch AS alt-ergo +COPY --from=compilation /src/alt-ergo/src/bin/text/Main_text.exe /bin/alt-ergo +ENTRYPOINT [ "/bin/alt-ergo" ] + +# FROM ocamlpro/ocaml:4.14 AS compilation +# +# USER ocaml +# +# RUN sudo apk add zlib-static +# +# COPY --chown=ocaml:ocaml . /src/alt-ergo +# +# WORKDIR /src/alt-ergo +# +# RUN opam switch create . ocaml-system --locked --deps-only --ignore-constraints-on alt-ergo-lib,alt-ergo-parsers +# +# RUN opam exec -- dune subst +# +# RUN LINK_MODE=static opam exec -- dune build --release src/bin/text/Main_text.exe +# +# FROM scratch AS alt-ergo +# COPY --from=compilation /src/alt-ergo/src/bin/text/Main_text.exe /bin/alt-ergo +# ENTRYPOINT [ "/bin/alt-ergo" ] diff --git a/src/bin/text/gen-link-flags.sh b/src/bin/text/gen-link-flags.sh index 1e23263fd..340818d88 100755 --- a/src/bin/text/gen-link-flags.sh +++ b/src/bin/text/gen-link-flags.sh @@ -26,7 +26,8 @@ case "$LINK_MODE" in linux) for lib in $LIBS; do CCLIB="$CCLIB -l$lib" - done;; + done + CCLIB="-Wl,-Bstatic $CCLIB -Wl,-Bdynamic";; macosx) for lib in $LIBS; do if [[ $lib == lib* ]]; then From 09993d29651cc7e92a8eb57d95d6594aafeac189 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= Date: Wed, 20 Mar 2024 13:57:32 +0100 Subject: [PATCH 04/10] WIPPITY --- Dockerfile | 17 +++++++++++++---- 1 file changed, 13 insertions(+), 4 deletions(-) diff --git a/Dockerfile b/Dockerfile index ab0881f79..123b06274 100644 --- a/Dockerfile +++ b/Dockerfile @@ -1,6 +1,17 @@ -FROM quay.io/pypa/manylinux_2_28_aarch64 AS compilation +FROM quay.io/pypa/manylinux_2_28_x86_64 AS compilation -ADD https://github.com/ocaml/opam/releases/download/2.2.0-beta1/opam-2.2.0-beta1-arm64-linux /bin/opam +# 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 @@ -15,8 +26,6 @@ ENV OPAMDEPEXTYES 1 ENV OPAMCONFIRMLEVEL unsafe-yes ENV OPAMERRLOGLEN 0 -RUN yum -y install gmp-static zlib-static - RUN opam switch create . 4.14.1 --locked --deps-only --ignore-constraints-on alt-ergo-lib,alt-ergo-parsers RUN opam exec -- dune subst From bf4fcd5e1a27f5f25d8cb7a1de892be415f5047c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= Date: Wed, 20 Mar 2024 14:03:15 +0100 Subject: [PATCH 05/10] WIP --- .github/workflows/build_static.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/build_static.yml b/.github/workflows/build_static.yml index 21de66762..5aab6ed72 100644 --- a/.github/workflows/build_static.yml +++ b/.github/workflows/build_static.yml @@ -35,7 +35,7 @@ jobs: 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 switch create . ocaml-system --locked --deps-only --ignore-constraints-on alt-ergo-lib,alt-ergo-parsers - run: opam exec -- dune subst From 1229dcb9c85555332328a532c3b7671cf692e3e5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= Date: Wed, 20 Mar 2024 15:00:31 +0100 Subject: [PATCH 06/10] WIP --- .github/workflows/build_static.yml | 3 +++ Dockerfile | 8 +++++--- 2 files changed, 8 insertions(+), 3 deletions(-) diff --git a/.github/workflows/build_static.yml b/.github/workflows/build_static.yml index 5aab6ed72..0c4684ce3 100644 --- a/.github/workflows/build_static.yml +++ b/.github/workflows/build_static.yml @@ -78,7 +78,10 @@ jobs: - 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: LINK_MODE=static opam exec -- dune build --release src/bin/text/Main_text.exe diff --git a/Dockerfile b/Dockerfile index 123b06274..3681e4f65 100644 --- a/Dockerfile +++ b/Dockerfile @@ -30,11 +30,13 @@ RUN opam switch create . 4.14.1 --locked --deps-only --ignore-constraints-on alt RUN opam exec -- dune subst -RUN LINK_MODE=mixed opam exec -- dune build --release src/bin/text/Main_text.exe +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 /src/alt-ergo/src/bin/text/Main_text.exe /bin/alt-ergo -ENTRYPOINT [ "/bin/alt-ergo" ] +COPY --from=compilation /opt/alt-ergo/ /opt/alt-ergo/ +ENTRYPOINT [ "/opt/alt-ergo/bin/alt-ergo" ] # FROM ocamlpro/ocaml:4.14 AS compilation # From 33f2a4ec8c66b88edb83c8e1c7a252e4124365a4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= Date: Wed, 20 Mar 2024 15:18:22 +0100 Subject: [PATCH 07/10] WIP --- .github/workflows/build_static.yml | 4 ++-- Dockerfile | 20 -------------------- 2 files changed, 2 insertions(+), 22 deletions(-) diff --git a/.github/workflows/build_static.yml b/.github/workflows/build_static.yml index 0c4684ce3..0c0b8b3fa 100644 --- a/.github/workflows/build_static.yml +++ b/.github/workflows/build_static.yml @@ -53,10 +53,10 @@ jobs: runs-on: ubuntu-latest - # Retrieve and use a light docker container on which ocaml 4.10 is installed + # 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 + image: ocamlpro/ocaml:4.14-flambda options: --user root steps: diff --git a/Dockerfile b/Dockerfile index 3681e4f65..e4ec8dbee 100644 --- a/Dockerfile +++ b/Dockerfile @@ -37,23 +37,3 @@ 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" ] - -# FROM ocamlpro/ocaml:4.14 AS compilation -# -# USER ocaml -# -# RUN sudo apk add zlib-static -# -# COPY --chown=ocaml:ocaml . /src/alt-ergo -# -# WORKDIR /src/alt-ergo -# -# RUN opam switch create . ocaml-system --locked --deps-only --ignore-constraints-on alt-ergo-lib,alt-ergo-parsers -# -# RUN opam exec -- dune subst -# -# RUN LINK_MODE=static opam exec -- dune build --release src/bin/text/Main_text.exe -# -# FROM scratch AS alt-ergo -# COPY --from=compilation /src/alt-ergo/src/bin/text/Main_text.exe /bin/alt-ergo -# ENTRYPOINT [ "/bin/alt-ergo" ] From 14f35ae61bb043376eed8b80fe9b85df8a4edad2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= Date: Thu, 21 Mar 2024 15:55:41 +0100 Subject: [PATCH 08/10] macOS --- .github/workflows/build_static.yml | 18 +++++++++++------- src/bin/text/gen-link-flags.sh | 2 ++ 2 files changed, 13 insertions(+), 7 deletions(-) diff --git a/.github/workflows/build_static.yml b/.github/workflows/build_static.yml index 0c0b8b3fa..c03d5e0f6 100644 --- a/.github/workflows/build_static.yml +++ b/.github/workflows/build_static.yml @@ -13,7 +13,7 @@ jobs: 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' }} + #if: ${{ github.event_name == 'workflow_dispatch' }} strategy: matrix: include: @@ -39,14 +39,16 @@ jobs: - run: opam exec -- dune subst - - run: LINK_MODE=mixed opam exec -- dune build --release src/bin/text/Main_text.exe + - run: opam exec -- dune build --release @install --promote-install-files false + env: + LINK_MODE: mixed - - run: cp src/bin/text/Main_text.exe src/bin/text/alt-ergo + - 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: src/bin/text/alt-ergo + path: _destdir/opt/alt-ergo/bin/alt-ergo musl: name: Build statically linked binary with musl @@ -83,11 +85,13 @@ jobs: - 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: opam exec -- dune build --release @install --promote-install-files false + env: + LINK_MODE: static - - run: cp src/bin/text/Main_text.exe src/bin/text/alt-ergo + - 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: src/bin/text/alt-ergo + path: _destdir/opt/alt-ergo/bin/alt-ergo diff --git a/src/bin/text/gen-link-flags.sh b/src/bin/text/gen-link-flags.sh index 340818d88..097b67d76 100755 --- a/src/bin/text/gen-link-flags.sh +++ b/src/bin/text/gen-link-flags.sh @@ -20,6 +20,8 @@ case "$LINK_MODE" in 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 From 40bba3ff983b980802942a840814a31b8d990788 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= Date: Thu, 21 Mar 2024 16:05:06 +0100 Subject: [PATCH 09/10] There is already a switch --- .github/workflows/build_static.yml | 2 -- 1 file changed, 2 deletions(-) diff --git a/.github/workflows/build_static.yml b/.github/workflows/build_static.yml index c03d5e0f6..198ebb70a 100644 --- a/.github/workflows/build_static.yml +++ b/.github/workflows/build_static.yml @@ -35,8 +35,6 @@ jobs: ocaml-compiler: 4.14.1 dune-cache: true - - run: opam switch create . ocaml-system --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 From db42948360c31b3f782023ae7e84fcaf005dca58 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= Date: Thu, 21 Mar 2024 16:10:26 +0100 Subject: [PATCH 10/10] still need to install deps...... --- .github/workflows/build_static.yml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/.github/workflows/build_static.yml b/.github/workflows/build_static.yml index 198ebb70a..7976357ac 100644 --- a/.github/workflows/build_static.yml +++ b/.github/workflows/build_static.yml @@ -35,6 +35,8 @@ jobs: 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