Add Kani smoke CI job (4.1.2)#308
Merged
Merged
Conversation
Draft the approval-gated ExecPlan for roadmap item `4.1.2`. The plan scopes the future implementation to a dedicated `kani-smoke` CI job, keeps `build-test` unchanged, and records the cache, review, and validation boundaries for the implementation phase.
Contributor
WalkthroughThe PR implements a dedicated ChangesKani-smoke CI job and documentation
Possibly related PRs
Suggested labels
Poem
Caution Pre-merge checks failedPlease resolve all errors before merging. Addressing warnings is optional.
❌ Failed checks (2 errors)
✅ Passed checks (16 passed)
✨ Finishing Touches📝 Generate docstrings
🧪 Generate unit tests (beta)
Comment |
Add a dedicated `kani-smoke` pull-request job that installs the repository-pinned Kani version and runs the bounded smoke target. Keep `build-test` unchanged while caching Kani tool paths separately from ordinary Cargo artefacts. Document the CI lane for contributors, update the living ExecPlan with validation evidence, and mark roadmap item `4.1.2` complete.
![codescene-delta-analysis[bot]](https://avatars.githubusercontent.com/in/53921?s=60&v=4){kind=small}
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
Mark the ExecPlan complete after the implementation commit, branch push, and draft pull request refresh. Preserve the validation record so the plan can be used as the final delivery log for roadmap item `4.1.2`.
Contributor
Reviewer's GuideAdds a new pull-request-only Flow diagram for kani-smoke CI job stepsflowchart TD
A["Start kani-smoke job (pull_request)"] --> B["actions/checkout@v4.1.2"]
B --> C["Setup Rust via setup-rust action (toolchain: stable)"]
C --> D["Set CARGO_HOME=.kani-cargo and KANI_HOME=.kani-home"]
D --> E["Restore/save cache for .kani-cargo and .kani-home<br>(actions/cache with key from tools/kani/VERSION)"]
E --> F["scripts/install-kani.sh"]
F --> G["make kani (bounded Kani smoke path)"]
G --> H["Job complete"]
File-Level Changes
Tips and commandsInteracting with Sourcery
Customizing Your ExperienceAccess your dashboard to:
Getting Help
|
![sourcery-ai[bot]](https://avatars.githubusercontent.com/in/48477?s=60&v=4){kind=small}
Contributor
There was a problem hiding this comment.
Hey - I've found 3 issues
Prompt for AI Agents
Please address the comments from this code review:
## Individual Comments
### Comment 1
<location path=".github/workflows/ci.yml" line_range="87" />
<code_context>
+ uses: leynos/shared-actions/.github/actions/setup-rust@6b13b519f99c5b461be8cc21ecf19c2ec5907b9c
+ with:
+ toolchain: stable
+ - name: Cache Kani tools
+ uses: actions/cache@0057852bfaa89a56745cba8c7296529d2fc39830 # v4.3.0
+ with:
+ path: |
+ .kani-cargo
+ .kani-home
+ key: ${{ runner.os }}-kani-${{ hashFiles('tools/kani/VERSION') }}
+ - name: Install Kani
+ run: scripts/install-kani.sh
</code_context>
<issue_to_address>
**suggestion (bug_risk):** Consider including installer or script inputs in the cache key to avoid stale Kani tool caches.
Since the key only uses `runner.os` and `tools/kani/VERSION`, changes to `scripts/install-kani.sh` (or other install-time inputs) won’t invalidate the cache unless `VERSION` is bumped. To avoid incompatible tool caches, consider adding a hash or version from the installer (e.g., via `hashFiles` or `restore-keys`) to the cache key.
```suggestion
key: ${{ runner.os }}-kani-${{ hashFiles('tools/kani/VERSION', 'scripts/install-kani.sh') }}
```
</issue_to_address>
### Comment 2
<location path="docs/execplans/4-1-2-kani-smoke-ci-job.md" line_range="1" />
<code_context>
+# 4.1.2. Add a Kani smoke CI job
+
+This ExecPlan (execution plan) is a living document. The sections
</code_context>
<issue_to_address>
**suggestion (review_instructions):** The acronym “CI” appears in the title before “Continuous Integration (CI)” is defined later in the document.
To comply with the acronym rule, expand “CI” the first time it appears. For example:
"Add a Kani smoke Continuous Integration (CI) job"
<details>
<summary>Review instructions:</summary>
**Path patterns:** `**/*.md`
**Instructions:**
Define uncommon acronyms on first use.
</details>
</issue_to_address>
### Comment 3
<location path="docs/execplans/4-1-2-kani-smoke-ci-job.md" line_range="49" />
<code_context>
+- Reuse the repository pin in `tools/kani/VERSION` and the existing
+ `scripts/install-kani.sh` and `scripts/check-kani-version.sh` paths where
+ possible.
+- Keep OrthoConfig unchanged. This is CI wiring, not a new CLI flag, runtime
+ configuration field, localized help string, or configuration precedence
+ rule.
</code_context>
<issue_to_address>
**suggestion (review_instructions):** The acronym “CLI” is used here without being defined on first use in the document.
Please expand “CLI” on its first occurrence in the document, for example “command-line interface (CLI) flag”, and then use “CLI” thereafter.
<details>
<summary>Review instructions:</summary>
**Path patterns:** `**/*.md`
**Instructions:**
Define uncommon acronyms on first use.
</details>
</issue_to_address>Help me be more useful! Please click 👍 or 👎 on each comment and I'll use the feedback to improve your reviews.
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
Contributor
There was a problem hiding this comment.
Actionable comments posted: 1
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In @.github/workflows/ci.yml:
- Line 76: The checkout step currently uses actions/checkout without disabling
credential persistence; update the checkout action invocation (the
actions/checkout@... entry) to add a with: persist-credentials: false setting so
the GITHUB_TOKEN is not left configured for subsequent steps; locate the
actions/checkout line and add the persist-credentials: false option under its
with block for that step.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Organization UI
Review profile: ASSERTIVE
Plan: Pro Plus
Run ID: 0915710e-317a-4bf4-b534-e946a91b38a3
📒 Files selected for processing (4)
.github/workflows/ci.ymldocs/developers-guide.mddocs/execplans/4-1-2-kani-smoke-ci-job.mddocs/roadmap.md
Set `persist-credentials: false` on the `kani-smoke` checkout step so the pull-request verification job does not leave the GitHub token in the repository configuration for later steps.
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
Include the Kani installer script in the smoke job cache key so changes to install-time inputs invalidate stale tool caches. Expand acronyms on first use in the Kani smoke ExecPlan to match documentation review rules.
Owner
Author
|
@coderabbitai Have the following now been resolved? Annul any requirements that violate the en-GB-oxendict spelling (-ize / -yse / -our) conventions (for example a request to replace "normalize" with "normalise" or "artefact" with "artifact"), or where the requirement unnecessarily increases cyclomatic complexity. |
Owner
Author
|
@coderabbitai Have the following failed checks now been resolved? If further work is required, please provide an AI agent prompt for the remaining work to be done to address these failures. Do not treat warnings as optional or aspirational. Where a change is out of scope for this PR, propose a GitHub issue unless one exists already. ❌ Failed checks (2 errors)
|
Contributor
|
Tip For best results, initiate chat on the files or code changes. 🧩 Analysis chain🏁 Script executed: Length of output: 4261
[resolve] |
Contributor
|
Tip For best results, initiate chat on the files or code changes. 🧩 Analysis chain🏁 Script executed: Length of output: 1222
No further work is required for these failures. |
This was referenced May 22, 2026
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.
Summary
This branch implements roadmap task
(4.1.2)by adding a dedicatedkani-smokeContinuous Integration (CI) job. The new job leaves the existingbuild-testjob unchanged, runs only the bounded smoke path on pull requests, and caches Kani tool paths separately from ordinary Cargo artefacts.Roadmap task:
(4.1.2)Execplan: docs/execplans/4-1-2-kani-smoke-ci-job.md
Review walkthrough
kani-smokejob and confirmbuild-testremains unchanged.Validation
coderabbit review --agent: passed with zero findings after the CI/docs milestone.coderabbit review --agent: passed with zero findings after final roadmap and ExecPlan updates.make check-fmt: passed.make lint: passed.make test: passed.make kani: passed.make markdownlint: passed.make nixie: passed.Notes
make fmtwas attempted because Markdown changed, but it reported pre-existing Markdown lint findings across unrelated documentation and rewrote broad files before failing. Those unrelated formatter edits were restored; focusedmake markdownlintandmake nixiechecks pass on the final tree.No Rust runtime, CLI, OrthoConfig, or user-facing behaviour changed, so no new
rstest,rstest-bdd, or end-to-end tests were applicable for this CI-only change.References
Summary by Sourcery
Add a dedicated Kani smoke GitHub Actions job for pull requests and document its behaviour and roadmap completion.
New Features:
Enhancements:
CI: