Split analysis makefile and GitHub Actions workflow - #294
Merged
Conversation
mk/analysis.mk held three unrelated things in 595 lines: the clang-format and shellcheck file lists, the clang-tidy, scan-build and Infer entry points, and the Frama-C proof targets with the WP machinery that turns them into rules. Branches touching different halves of it still conflict. mk/verify.mk keeps the proofs, mk/lint.mk and mk/format.mk take the rest. The proof target table stays with the machinery rather than becoming a fourth file. VERIFY_TARGETS reads $(.VARIABLES) with :=, so it sees only what make has parsed so far, and check-proof-targets.py catches a VERIFY_<T>_SRC block written below that line by comparing the table against "make print-verify-targets". A table in its own file is always parsed first, which makes that comparison unfalsifiable: the check would report success for the one mistake it was written to catch. scripts/analysis-mk.py becomes scripts/verify-mk.py and gains joined_text(), so check-mutants.py and check-char-signedness.py drop the private copies of that reader they each carried and the makefile is named in one place. check-mutants.py's HARNESS_FILES lists mk/verify.mk in place of mk/analysis.mk; mk/format.mk and mk/lint.mk are left out because neither can change a proof verdict, which is what that set selects for. Targets, recipes and variables are unchanged: "make -n verify" prints the same recipe for all seventeen proofs, and "make help" lists the same entries, with print-verify-targets now printing after analyze because the awk scans MAKEFILE_LIST in include order.
![cubic-dev-ai[bot]](https://avatars.githubusercontent.com/in/1082092?s=60&v=4){kind=small}
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
jserv
changed the title
Contributor
|
Use "GitHub Actions" instead of "Github CI" as the latter is confusing. |
.github/workflows/main.yml ran ten jobs in 869 lines, so a branch
touching the runtime matrix conflicted with one touching the proof
sharding. It splits along its needs edges, leaving no dependency to
cross a file boundary: lint.yml, build.yml (build-macos ->
runtime-macos), static-analysis.yml (tidy-macos, scan-macos,
infer-macos) and verify.yml (proof-targets -> verify-mutants -> verify
and verify-mutants-gate).
Job ids, job names, steps, env, matrices, caches and artifact names are
copied unchanged, so every required status check keeps the name branch
protection requires. That is also why the jobs are not routed through a
reusable workflow: one called with workflow_call reports as "<caller> /
<callee>", which renames the check and unrequires it silently.
check-proof-targets.py reads the verify-mutants matrix out of
verify.yml, and check-mutants.py's HARNESS_FILES names verify.yml alone,
since that is the file deciding which target a shard passes to --target
and the other three cannot reach the mutation run.
Each file carries its own copy of the on:, concurrency: and permissions:
blocks, so ${{ github.workflow }} now yields four cancellation groups
instead of one. A new push still cancels every in-flight job of a pull
request; cancelling one workflow by hand no longer cancels the rest, and
a manual run takes one workflow_dispatch per file.
runtime-macos was gated to push and pull_request, so "Run workflow" on Build ran build-macos alone and reported green with every HVF and sanitizer leg skipped. A skipped required check does not block a merge, as verify-mutants-gate's comment in verify.yml already records, so a manual run could stand in for testing that never happened. The gate predates the split: main.yml carried the same if: under an on: block that already listed workflow_dispatch. Adding the event rather than dropping the trigger keeps the manual re-run, which is what the self-hosted runners need after an outage. The repository guard is untouched, so a fork still cannot reach them. Only the PR-head guard step reads pull_request context and it carries its own if:.
On a tree without the generated headers, "make lint" fails: src/debug/syscall-hist.c:18:10: error: 'dispatch.h' file not found src/syscall/syscall.c:78:10: error: 'dispatch.h' file not found Found compiler error(s). make: *** [lint] Error 1 The target listed shim_blob.h and version.h only, while clang-tidy runs over $(SRCS), two of whose files include the dispatch.h that $(DISPATCH_HEADER) generates. mk/analysis.mk carried the same list, so the gap predates the split. tidy-macos hid it with a step that generated all three headers before calling make lint, which meant CI never exercised the target's own dependencies. That step goes with the fix.
Without shellcheck on PATH the loop read the shell's 127 as a warning like any other, so the target ended: /bin/sh: shellcheck: command not found ... 39 script(s) have warnings counting scripts none of which was checked. require-tool, which lint, analyze and infer-uninit already call, names the tool and the install and stops there. The command -v guards on shfmt and black in indent are deliberately the other shape: a formatter that skips itself changes nothing, while a checker that skips itself reports a pass it never earned. mk/analysis.mk carried the same loop, so this predates the split.
henrybear327
force-pushed
the
build/split-analysis-and-ci
branch
from
August 14, 2026 13:35
8966357 to
15996f3
Compare
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
2 participants
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.
It's been a recent trend that that we continue to have merge conflicts regarding the analysis makefile and Github Action main.yml files, and those 2 files have grown to a size that is not easily maintainable.
This PR splits the files by feature area. It's a pure refactoring PR, not intended to do any feature changes.
Summary by cubic
Split the analysis Makefile and CI workflow by concern to reduce conflicts and keep required checks stable. Manual Build dispatches now run HVF runtime tests; check-format fails if
shellcheckis missing, and lint depends on the generateddispatch.h.Review notes
mk/lint.mk,mk/verify.mk, andmk/format.mk; proof targets stay inmk/verify.mk. Targets and recipes are unchanged..github/workflows/main.ymlwithbuild.yml,lint.yml,static-analysis.yml, andverify.yml; job ids/names, matrices, caches, artifacts, and required status checks are preserved. Concurrency is per file. Build onworkflow_dispatchruns runtime tests.scripts/verify-mk.py;check-proof-targets.pyreads the verify matrix fromverify.yml. Stubs and scripts now referencemk/verify.mk.make lintadds$(DISPATCH_HEADER)as a prerequisite.check-formatrequiresshellcheckand fails fast if missing.Migration
shellcheckto runmake check-format. No changes needed for developers otherwise or for branch protection settings.Written for commit 15996f3. Summary will update on new commits.