.github/with-docker: make compatible with podman

.github/actions/with-docker/action.yml

@@ -41,8 +41,8 @@ runs:
     run: |
       set -euxo pipefail
 
-      USER=github-user
-      GROUP=${USER}
+      IMAGE_USER=github-user
+      IMAGE_GROUP=${IMAGE_USER}
       Z3_VERSION=$(cat deps/z3)
       K_VERSION=$(cat deps/k_release)
       UV_VERSION=$(cat deps/uv_release)
@@ -53,22 +53,23 @@ runs:
         --tag "${TAG_NAME}"                         \
         --build-arg USER_ID="${USER_ID}"            \
         --build-arg GROUP_ID="${GROUP_ID}"          \
-        --build-arg USER="${USER}"                  \
-        --build-arg GROUP="${GROUP}"                \
+        --build-arg IMAGE_USER="${IMAGE_USER}"      \
+        --build-arg IMAGE_GROUP="${IMAGE_GROUP}"    \
         --build-arg K_VERSION="${K_VERSION}"        \
         --build-arg Z3_VERSION="${Z3_VERSION}"      \
         --build-arg LLVM_VERSION="${LLVM_VERSION}"  \
         --build-arg UV_VERSION="${UV_VERSION}"
 
-      docker run                            \
-        --name "${CONTAINER_NAME}"          \
-        --rm                                \
-        --interactive                       \
-        --tty                               \
-        --detach                            \
-        --user root                         \
-        --workdir "/home/${USER}/workspace" \
+      docker rm --force "${CONTAINER_NAME}" || true
+
+      docker run                                  \
+        --name "${CONTAINER_NAME}"                \
+        --interactive                             \
+        --tty                                     \
+        --detach                                  \
+        --user root                               \
+        --workdir "/home/${IMAGE_USER}/workspace" \
         "${TAG_NAME}"
 
-      docker cp . "${CONTAINER_NAME}":"/home/${USER}/workspace"
-      docker exec "${CONTAINER_NAME}" chown -R "${USER}:${GROUP}" "/home/${USER}"
+      docker cp ./. "${CONTAINER_NAME}":"/home/${IMAGE_USER}/workspace"
+      docker exec "${CONTAINER_NAME}" chown -R "${IMAGE_USER}:${IMAGE_GROUP}" "/home/${IMAGE_USER}"

.github/workflows/Dockerfile

@@ -2,19 +2,19 @@ ARG Z3_VERSION
 ARG K_VERSION
 ARG LLVM_VERSION
 
-FROM ghcr.io/foundry-rs/foundry:rc-1 as FOUNDRY
+FROM ghcr.io/foundry-rs/foundry:rc-1 AS foundry
 
 ARG Z3_VERSION
-FROM runtimeverificationinc/z3:ubuntu-jammy-${Z3_VERSION} as Z3
+FROM runtimeverificationinc/z3:ubuntu-jammy-${Z3_VERSION} AS z3
 
 ARG K_VERSION
 FROM runtimeverificationinc/kframework-k:ubuntu-jammy-${K_VERSION}
 
-COPY --from=FOUNDRY /usr/local/bin/forge /usr/local/bin/forge
-COPY --from=FOUNDRY /usr/local/bin/anvil /usr/local/bin/anvil
-COPY --from=FOUNDRY /usr/local/bin/cast /usr/local/bin/cast
+COPY --from=foundry /usr/local/bin/forge /usr/local/bin/forge
+COPY --from=foundry /usr/local/bin/anvil /usr/local/bin/anvil
+COPY --from=foundry /usr/local/bin/cast /usr/local/bin/cast
 
-COPY --from=Z3 /usr/bin/z3 /usr/bin/z3
+COPY --from=z3 /usr/bin/z3 /usr/bin/z3
 
 ARG LLVM_VERSION
 
@@ -37,17 +37,17 @@ RUN    apt-get update                  \
             python3                    \
             python3-pip
 
-ARG USER=user
-ARG GROUP
+ARG IMAGE_USER=user
+ARG IMAGE_GROUP
 ARG USER_ID
 ARG GROUP_ID
-RUN groupadd -g ${GROUP_ID} ${GROUP} && useradd -m -u ${USER_ID} -s /bin/sh -g ${GROUP} ${USER}
+RUN groupadd -g ${GROUP_ID} ${IMAGE_GROUP} && useradd -m -u ${USER_ID} -s /bin/sh -g ${IMAGE_GROUP} ${IMAGE_USER}
 
-USER ${USER}:${GROUP}
-RUN mkdir /home/${USER}/workspace
-WORKDIR /home/${USER}/workspace
+USER ${IMAGE_USER}:${IMAGE_GROUP}
+RUN mkdir /home/${IMAGE_USER}/workspace
+WORKDIR /home/${IMAGE_USER}/workspace
 
-ENV PATH=/home/${USER}/.cargo/bin:/home/${USER}/.local/bin:/usr/local/bin/:${PATH}
+ENV PATH=/home/${IMAGE_USER}/.cargo/bin:/home/${IMAGE_USER}/.local/bin:/usr/local/bin/:${PATH}
 
 ARG UV_VERSION
 RUN curl -LsSf https://astral.sh/uv/$UV_VERSION/install.sh | sh && uv --version

.github/workflows/test-pr.yml

@@ -86,7 +86,7 @@ jobs:
         run: |
           # Best effort: the container does not exist if 'Set up Docker' failed, and a
           # non-zero exit here would mask the step that actually failed.
-          docker stop --timeout=0 "kontrol-ci-profile-${GITHUB_SHA}" || true
+          docker rm --force "kontrol-ci-profile-${GITHUB_SHA}" || true
 
   integration-tests:
     needs: code-quality-checks
@@ -118,7 +118,7 @@ jobs:
         run: |
           # Best effort: the container does not exist if 'Set up Docker' failed, and a
           # non-zero exit here would mask the step that actually failed.
-          docker stop --timeout=0 "kontrol-ci-integration-${GITHUB_SHA}" || true
+          docker rm --force "kontrol-ci-integration-${GITHUB_SHA}" || true
 
   cse-tests:
     needs: code-quality-checks
@@ -137,20 +137,20 @@ jobs:
       - name: 'Set up Docker'
         uses: ./.github/actions/with-docker
         with:
-          container-name: kontrol-ci-integration-${{ github.sha }}
+          container-name: kontrol-ci-cse-${{ github.sha }}
       - name: 'Build Kontrol'
         run: |
-            docker exec -u github-user "kontrol-ci-integration-${GITHUB_SHA}" /bin/bash -c 'CXX=clang++-14 uv run kdist --verbose build -j`nproc` kontrol.*'
+            docker exec -u github-user "kontrol-ci-cse-${GITHUB_SHA}" /bin/bash -c 'CXX=clang++-14 uv run kdist --verbose build -j`nproc` kontrol.*'
       - name: 'Run CSE and Minimize tests'
         run: |
           TEST_ARGS='--numprocesses=5 --force-sequential -vv -k "test_kontrol_cse or test_foundry_minimize_proof"'
-          docker exec --user github-user "kontrol-ci-integration-${GITHUB_SHA}" make cov-integration TEST_ARGS="${TEST_ARGS}"
+          docker exec --user github-user "kontrol-ci-cse-${GITHUB_SHA}" make cov-integration TEST_ARGS="${TEST_ARGS}"
       - name: 'Tear down Docker'
         if: always()
         run: |
           # Best effort: the container does not exist if 'Set up Docker' failed, and a
           # non-zero exit here would mask the step that actually failed.
-          docker stop --timeout=0 "kontrol-ci-integration-${GITHUB_SHA}" || true
+          docker rm --force "kontrol-ci-cse-${GITHUB_SHA}" || true
 
   end-to-end-tests:
     needs: code-quality-checks
@@ -169,20 +169,20 @@ jobs:
       - name: 'Set up Docker'
         uses: ./.github/actions/with-docker
         with:
-          container-name: kontrol-ci-integration-${{ github.sha }}
+          container-name: kontrol-ci-e2e-${{ github.sha }}
       - name: 'Build Kontrol'
         run: |
-            docker exec -u github-user "kontrol-ci-integration-${GITHUB_SHA}" /bin/bash -c 'CXX=clang++-14 uv run kdist --verbose build -j`nproc` kontrol.*'
+            docker exec -u github-user "kontrol-ci-e2e-${GITHUB_SHA}" /bin/bash -c 'CXX=clang++-14 uv run kdist --verbose build -j`nproc` kontrol.*'
       - name: 'Run end-to-end tests'
         run: |
           TEST_ARGS='--numprocesses=6 -vv --force-sequential -k "test_kontrol_end_to_end or test_kontrol_setup_storage or test_kontrol_counterexample_generation"'
-          docker exec --user github-user "kontrol-ci-integration-${GITHUB_SHA}" make cov-integration TEST_ARGS="${TEST_ARGS}"
+          docker exec --user github-user "kontrol-ci-e2e-${GITHUB_SHA}" make cov-integration TEST_ARGS="${TEST_ARGS}"
       - name: 'Tear down Docker'
         if: always()
         run: |
           # Best effort: the container does not exist if 'Set up Docker' failed, and a
           # non-zero exit here would mask the step that actually failed.
-          docker stop --timeout=0 "kontrol-ci-integration-${GITHUB_SHA}" || true
+          docker rm --force "kontrol-ci-e2e-${GITHUB_SHA}" || true
 
   docker:
     needs: code-quality-checks
@@ -209,12 +209,15 @@ jobs:
         run: |
           K_VERSION=$(cat deps/k_release)
           Z3_VERSION=$(cat deps/z3)
-          docker build . --tag "${IMAGE_TAG}" --build-arg K_VERSION="${K_VERSION}" --build-arg Z3_VERSION="${Z3_VERSION}"
+          docker build . --ulimit nofile=65536:65536 --tag "${IMAGE_TAG}" --build-arg K_VERSION="${K_VERSION}" --build-arg Z3_VERSION="${Z3_VERSION}"
       - name: 'Start Docker container'
         run: |
+          # A container left behind by a canceled run keeps the name taken on the
+          # podman runners, so make starting one idempotent.
+          docker rm --force "${CONTAINER_NAME}" || true
+
           docker run                            \
             --name "${CONTAINER_NAME}"          \
-            --rm                                \
             --interactive                       \
             --tty                               \
             --detach                            \
@@ -239,7 +242,7 @@ jobs:
         run: |
           # Best effort: the container does not exist if 'Start Docker container' failed,
           # and a non-zero exit here would mask the step that actually failed.
-          docker stop --timeout=0 "${CONTAINER_NAME}" || true
+          docker rm --force "${CONTAINER_NAME}" || true
 
   nix:
     needs: code-quality-checks

.github/workflows/update-expected-output.yml

@@ -27,19 +27,19 @@ jobs:
       - name: 'Set up Docker'
         uses: ./.github/actions/with-docker
         with:
-          container-name: kontrol-ci-integration-${{ github.sha }}
+          container-name: kontrol-ci-expected-output-${{ github.sha }}
       - name: 'Build Kontrol'
         run: |
-            docker exec -u github-user "kontrol-ci-integration-${GITHUB_SHA}" /bin/bash -c 'CXX=clang++-14 uv run kdist --verbose build -j`nproc` kontrol.*'
+            docker exec -u github-user "kontrol-ci-expected-output-${GITHUB_SHA}" /bin/bash -c 'CXX=clang++-14 uv run kdist --verbose build -j`nproc` kontrol.*'
       - name: 'Run integration tests'
         run: |
           TEST_ARGS="--maxfail=1000 --numprocesses=2 --update-expected-output --force-sequential -vv"
-          docker exec --user github-user "kontrol-ci-integration-${GITHUB_SHA}" bash -c "make cov-integration TEST_ARGS='${TEST_ARGS} -k \"not (test_kontrol_cse or test_foundry_minimize_proof or test_kontrol_end_to_end or test_kontrol_setup_storage or test_kontrol_counterexample_generation)\"' || true"
-          docker exec --user github-user "kontrol-ci-integration-${GITHUB_SHA}" bash -c "make cov-integration TEST_ARGS='${TEST_ARGS} -k \"test_kontrol_cse or test_foundry_minimize_proof\"' || true"
-          docker exec --user github-user "kontrol-ci-integration-${GITHUB_SHA}" bash -c "make cov-integration TEST_ARGS='${TEST_ARGS} -k \"test_kontrol_end_to_end or test_kontrol_setup_storage or test_kontrol_counterexample_generation\"' || true"
+          docker exec --user github-user "kontrol-ci-expected-output-${GITHUB_SHA}" bash -c "make cov-integration TEST_ARGS='${TEST_ARGS} -k \"not (test_kontrol_cse or test_foundry_minimize_proof or test_kontrol_end_to_end or test_kontrol_setup_storage or test_kontrol_counterexample_generation)\"' || true"
+          docker exec --user github-user "kontrol-ci-expected-output-${GITHUB_SHA}" bash -c "make cov-integration TEST_ARGS='${TEST_ARGS} -k \"test_kontrol_cse or test_foundry_minimize_proof\"' || true"
+          docker exec --user github-user "kontrol-ci-expected-output-${GITHUB_SHA}" bash -c "make cov-integration TEST_ARGS='${TEST_ARGS} -k \"test_kontrol_end_to_end or test_kontrol_setup_storage or test_kontrol_counterexample_generation\"' || true"
       - name: 'Copy updated files to host'
         run: |
-          docker cp "kontrol-ci-integration-${GITHUB_SHA}":/home/github-user/workspace/src/tests/integration/test-data/show ./src/tests/integration/test-data/
+          docker cp "kontrol-ci-expected-output-${GITHUB_SHA}":/home/github-user/workspace/src/tests/integration/test-data/show ./src/tests/integration/test-data/
       # The regenerated files are published as an artifact rather than pushed back to
       # the branch, so this workflow needs no write credential. Download it and commit
       # the contents over src/tests/integration/test-data/show; see the README.
@@ -58,4 +58,4 @@ jobs:
         run: |
           # Best effort: the container does not exist if 'Set up Docker' failed, and a
           # non-zero exit here would mask the step that actually failed.
-          docker stop --timeout=0 "kontrol-ci-integration-${GITHUB_SHA}" || true
+          docker rm --force "kontrol-ci-expected-output-${GITHUB_SHA}" || true