Install dependencies, build SMACK, and format once in CI - #845
Open
shaobo-he wants to merge 7 commits into
Open
Conversation
The regression matrix has 28 entries, and every one of them re-ran the identical clang-format/flake8 pass and installed the dev dependencies from scratch to do it. Each job also invoked bin/build.sh twice, the second call re-running the whole apt phase for nothing, and installed a Rust nightly toolchain even for the 17 pure C/LLVM folders. Workflow changes: * Hoist formatting into a single `check-format` job. bin/build.sh stays the single source of truth for how the tools are installed -- it pins clang-format to LLVM_SHORT_VERSION from bin/versions -- but every phase except INSTALL_DEV_DEPENDENCIES is switched off, so the job installs no LLVM/dotnet/Boost packages, downloads no solvers and compiles nothing. It is deliberately not a `needs:` of check-regressions: a skipped job reports as success to branch protection, so gating the matrix on it would turn a formatting error into 28 green-looking skipped checks. * Collapse each matrix job's two bin/build.sh calls into one. * Derive INSTALL_RUST from the matrix entry, so only the folders that actually reach rustc install the nightly toolchain (10 of 28). * Cache smack-deps on bin/versions + bin/build.sh, so Z3, Boogie and Corral are downloaded once per version bump instead of 28 times per run. restore/save are split rather than using actions/cache so that only a job which ran green can publish an entry: bin/build.sh guards its installs with `[ ! -d ]`, so a job that died on a failed download would otherwise cache an empty tree that every later job would accept as a complete install. No restore-keys, for the same reason. * Restrict `push` to the branches that publish an image and add a concurrency group. A push to a branch with an open pull request used to fire the entire workflow a second time. Push runs key the group on github.run_id so two merges landing close together on develop both run and both publish. * Docker job: replace the disabled ::set-output syntax with $GITHUB_OUTPUT, and gate the job on a push to this repository -- Docker Hub secrets are not available to forks, so a fork PR used to earn a guaranteed red X after ~25 minutes of green regressions. Map main to :stable; master no longer exists after the rename, which is why :stable stopped being published even though docs/installation.md advertises it. * Add job timeouts and a read-only default permissions block. bin/build.sh changes: * Make DEPS_DIR overridable, so CI can place smack-deps inside GITHUB_WORKSPACE for actions/cache. Identical to today's value when unset. * Remove the hardcoded `GITHUB_ACTIONS = true -> exit 0` escape hatch. It existed only so the old workflow could lint between two build.sh calls, and it is a trap: any future job setting INSTALL_DEV_DEPENDENCIES=1 alongside BUILD_SMACK/TEST_SMACK would exit before the tests and report green. * Drop `cargo install rustfilt`. rustfilt appears exactly once in the whole repository, on the line being removed; nothing invokes it. It is also a from-source compile and the only unpinned item in the Rust install. * Give the exit status a defined value when TEST_SMACK=0. With `set -e` active, `res=$?` was only ever reached with $? == 0, and with TEST_SMACK=0 `res` was unset entirely. The 28 matrix strings are byte-identical, so every existing status check name is preserved. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
shaobo-he
changed the title
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
The regression matrix has 28 entries, but dependency installation, source
compilation, and formatting are properties of the revision rather than of an
individual test folder. This PR moves each of those operations out of the
matrix so the shards run only their assigned regression tests.
Workflow
prepare CI dependency imagecomputes an exact recipe hash over.github/ci/Dockerfile,bin/build.sh, andbin/versions.LLVM, .NET, Boost, Python, Rust, Z3, Boogie, and Corral and publishes the
image only after a successful build.
silently select stale tools.
build SMACKchecks out the requested revision in that image, compiles itonce, and uploads a one-day tar artifact of its install tree. The tar archive
preserves executable permissions.
set
BUILD_SMACK=0, and run only their selected tests.Fork pull requests can reuse an existing exact dependency image. If a fork
changes the image recipe, CI fails with an explicit request for a maintainer to
publish that trusted image; untrusted pull-request code is never given package
write access.
Per workflow run
The GitHub-hosted runner stops and deletes every job container during cleanup,
then decommissions the VM and its local image layers. The content-addressed GHCR
dependency image is retained deliberately: deleting that registry version after
each run would force a rebuild on every run and would prevent fork PRs from
reusing the trusted image.
Other CI corrections retained
pushevents after formatting,build, and regressions pass.
mainasstableanddevelopaslatest.pushandpull_requestruns.DEPS_DIRoverridable so the container can keep solver tools under/opt/smack-depswithout changing local defaults.Verification