diff --git a/.github/actions/with-docker/action.yml b/.github/actions/with-docker/action.yml index 286091200..85bbefc26 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,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}" 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..7a14045db 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 @@ -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 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