diff --git a/.github/workflows/docker-publish.yml b/.github/workflows/docker-publish.yml index e56584ae2..dd92f2a91 100644 --- a/.github/workflows/docker-publish.yml +++ b/.github/workflows/docker-publish.yml @@ -2,8 +2,17 @@ # Publish map2check-dev Docker image to GitHub Container Registry # # Triggers: -# - Push to develop (Dockerfile.dev changes) -# - Manual dispatch (workflow_dispatch) +# - Push to develop (Dockerfile.dev changes) -> build AND push +# - Pull request touching Dockerfile.dev -> build only, no push +# - Manual dispatch (workflow_dispatch) -> build AND push +# +# The pull_request trigger is not decoration. Until it existed, Dockerfile.dev +# was only ever built after a merge, so a recipe that cannot build reached +# develop and broke the image: the Clam section built with the default cc +# (GCC 11) instead of clang-16, and GCC rejects a construct in sea-dsa that +# clang only warns about. Nothing pre-merge could have caught that, because +# nothing pre-merge compiled the file. It is paths-filtered, so PRs that do not +# touch the Dockerfile pay nothing. # # Phase 1.5 — OpenSSF Best Practices Badge ############################################################ @@ -14,6 +23,10 @@ on: branches: [develop] paths: - 'Dockerfile.dev' + pull_request: + branches: [develop, main, master] + paths: + - 'Dockerfile.dev' workflow_dispatch: env: @@ -32,7 +45,10 @@ jobs: - name: Checkout uses: actions/checkout@v4 + # Skipped on pull_request: the run does not push, and a PR from a fork + # has no packages:write token to log in with anyway. - name: Log in to GHCR + if: github.event_name != 'pull_request' uses: docker/login-action@v3 with: registry: ${{ env.REGISTRY }} @@ -48,11 +64,13 @@ jobs: type=raw,value=latest type=sha,prefix= + # push is false on pull_request: the point there is to prove the recipe + # builds, not to publish an image from an unmerged branch over :latest. - name: Build and push uses: docker/build-push-action@v5 with: context: . file: ./Dockerfile.dev - push: true + push: ${{ github.event_name != 'pull_request' }} tags: ${{ steps.meta.outputs.tags }} labels: ${{ steps.meta.outputs.labels }} diff --git a/Dockerfile.dev b/Dockerfile.dev index c82691999..911010dc6 100644 --- a/Dockerfile.dev +++ b/Dockerfile.dev @@ -157,6 +157,15 @@ RUN apt-get update && apt-get install -y \ # CLAM_INCLUDE_TESTS=OFF: Clam's own lit suite needs `lit` from pip and adds # build time for tests of a dependency, not of Map2Check. # +# The compilers are named explicitly rather than left to the ENV CC/CXX set in +# section 11: those are declared 88 lines BELOW this RUN, and a Docker ENV only +# applies to later instructions, so Clam would silently build with the default +# cc/c++ (GCC 11). That is not a cosmetic difference -- sea-dsa defines +# seadsa::mkTLIGetter with a redundant namespace qualification inside its own +# namespace, which clang accepts as -Wextra-qualification but GCC rejects +# outright, and the image build dies at 34%. Upstream's own docker/clam.Dockerfile +# passes these same two flags; clang is the toolchain Clam is built against. +# # The crab / extra / build / install sequence is Clam's documented one. Each # target downloads and installs a dependency (Crab, then sea-dsa and # llvm-seahorn); the cmake re-run between them re-reads the cache so the next @@ -165,6 +174,8 @@ RUN git clone --depth 1 -b dev16 https://github.com/seahorn/clam.git /tmp/clam & cd /tmp/clam && mkdir build && cd build && \ CLAM_CFG="-DCMAKE_BUILD_TYPE=Release -DCLAM_LLVM_VERSION=16 \ -DCLAM_INCLUDE_TESTS=OFF \ + -DCMAKE_C_COMPILER=/usr/bin/clang-16 \ + -DCMAKE_CXX_COMPILER=/usr/bin/clang++-16 \ -DLLVM_DIR=/usr/lib/llvm-16/lib/cmake/llvm \ -DCMAKE_INSTALL_PREFIX=/opt/clam" && \ cmake .. $CLAM_CFG && \