diff --git a/.github/workflows/build_docker.yml b/.github/workflows/build_docker.yml deleted file mode 100644 index 14b7d596a4..0000000000 --- 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 0000000000..a9ac8e5284 --- /dev/null +++ b/.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 diff --git a/src/bin/text/dune b/src/bin/text/dune index 861dafd171..793e68dc25 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 4c6083a401..0000000000 --- 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 0000000000..097b67d76e --- /dev/null +++ b/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 ')'