Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
24 changes: 21 additions & 3 deletions .github/workflows/docker-publish.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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
############################################################
Expand All @@ -14,6 +23,10 @@ on:
branches: [develop]
paths:
- 'Dockerfile.dev'
pull_request:
branches: [develop, main, master]
paths:
- 'Dockerfile.dev'
workflow_dispatch:

env:
Expand All @@ -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 }}
Expand All @@ -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 }}
11 changes: 11 additions & 0 deletions Dockerfile.dev
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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 && \
Expand Down
Loading