From ac6a0bb4632e48510147f3f9f566758d03d842a6 Mon Sep 17 00:00:00 2001 From: Andrei <16517508+anvacaru@users.noreply.github.com> Date: Mon, 21 Sep 2026 15:27:40 +0300 Subject: [PATCH 1/3] podman compatibility updates --- .github/actions/with-docker/action.yml | 30 +++++++++++--------- .github/workflows/Dockerfile | 26 ++++++++--------- .github/workflows/test-pr.yml | 26 ++++++++++------- .github/workflows/update-expected-output.yml | 14 ++++----- 4 files changed, 51 insertions(+), 45 deletions(-) diff --git a/.github/actions/with-docker/action.yml b/.github/actions/with-docker/action.yml index 286091200..f0e4bdbb6 100644 --- a/.github/actions/with-docker/action.yml +++ b/.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,24 @@ 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}" \ + --rm \ + --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}" diff --git a/.github/workflows/Dockerfile b/.github/workflows/Dockerfile index 375ffb314..510a3de84 100644 --- a/.github/workflows/Dockerfile +++ b/.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 diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml index a19e14fe2..cc8c84308 100644 --- a/.github/workflows/test-pr.yml +++ b/.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 @@ -212,6 +212,10 @@ jobs: docker build . --tag "${IMAGE_TAG}" --build-arg K_VERSION="${K_VERSION}" --build-arg Z3_VERSION="${Z3_VERSION}" - name: 'Start Docker container' run: | + # See .github/actions/with-docker: a container left behind by a canceled + # run keeps the name taken on the podman runners. + docker rm --force "${CONTAINER_NAME}" || true + docker run \ --name "${CONTAINER_NAME}" \ --rm \ @@ -239,7 +243,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 diff --git a/.github/workflows/update-expected-output.yml b/.github/workflows/update-expected-output.yml index 7a558c8e4..4490fca7b 100644 --- a/.github/workflows/update-expected-output.yml +++ b/.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 From 1cb73b116364a3955b9ce3dfb6add4da3d94edeb Mon Sep 17 00:00:00 2001 From: Andrei <16517508+anvacaru@users.noreply.github.com> Date: Mon, 21 Sep 2026 15:54:40 +0300 Subject: [PATCH 2/3] remove rm from docker run invocations --- .github/actions/with-docker/action.yml | 1 - .github/workflows/test-pr.yml | 5 ++--- 2 files changed, 2 insertions(+), 4 deletions(-) diff --git a/.github/actions/with-docker/action.yml b/.github/actions/with-docker/action.yml index f0e4bdbb6..85bbefc26 100644 --- a/.github/actions/with-docker/action.yml +++ b/.github/actions/with-docker/action.yml @@ -64,7 +64,6 @@ runs: docker run \ --name "${CONTAINER_NAME}" \ - --rm \ --interactive \ --tty \ --detach \ diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml index cc8c84308..bd6afc535 100644 --- a/.github/workflows/test-pr.yml +++ b/.github/workflows/test-pr.yml @@ -212,13 +212,12 @@ jobs: docker build . --tag "${IMAGE_TAG}" --build-arg K_VERSION="${K_VERSION}" --build-arg Z3_VERSION="${Z3_VERSION}" - name: 'Start Docker container' run: | - # See .github/actions/with-docker: a container left behind by a canceled - # run keeps the name taken on the podman runners. + # 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 \ From 34fd91c908707b92fc4f9a2fbeab334934497384 Mon Sep 17 00:00:00 2001 From: Andrei <16517508+anvacaru@users.noreply.github.com> Date: Tue, 22 Sep 2026 09:11:51 +0300 Subject: [PATCH 3/3] add nofile ulimit flag --- .github/workflows/test-pr.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml index bd6afc535..7a14045db 100644 --- a/.github/workflows/test-pr.yml +++ b/.github/workflows/test-pr.yml @@ -209,7 +209,7 @@ 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