8000 ci: cap scheduled Kani proof concurrency (#693) by adityamukho · Pull Request #783 · project-minigraf/minigraf · GitHub
[go: up one dir, main page]
Skip to content

ci: cap scheduled Kani proof concurrency (#693) #783

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
adityamukho merged 1 commit into from
Oct 29, 2026
Merged

ci: cap scheduled Kani proof concurrency (#693) #783

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 8 additions & 6 deletions .github/workflows/kani.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,10 +10,12 @@ run-name: >-
|| github.event_name == 'workflow_dispatch' && inputs.ref
|| (github.event.schedule == '0 18 * * *' && 'v3' || 'main') }})

# #627: proves the byte encoders that order index keys (src/storage/keys/
# verification.rs, src/storage/index/verification.rs). The whole set takes
# about 30 seconds of proof time and ~1 GB of memory. Kani upgrades are
# deliberate PRs that re-run the set.
# #627/#693: main proves the value encoder (5 harnesses); v3 also proves
# key encoders and pure scalar decoders (29 harnesses after #693).
# The v3 set passed on the bench machine in about 2 minutes warm with
# 7.6 GiB aggregate CBMC peak RSS at -j 4. Keep concurrency capped at
# that measured value for the 16 GiB runner. Kani upgrades are deliberate
# PRs that re-run both branches' proof sets.

on:
pull_request:
Expand Down Expand Up @@ -61,7 +63,7 @@ jobs:
uses: model-checking/kani-github-action@v1.1
with:
kani-version: 0.68.0
args: --lib -j --output-format terse -Z unstable-options --harness-timeout 10m
args: --lib -j 4 --output-format terse -Z unstable-options --harness-timeout 10m

- name: Record Kani failure
if: ${{ failure() && github.event_name == 'schedule' }}
Expand All @@ -76,7 +78,7 @@ jobs:
echo
echo "- Run: $GITHUB_SERVER_URL/$GITHUB_REPOSITORY/actions/runs/$GITHUB_RUN_ID"
echo "- Commit: $(git rev-parse HEAD)"
echo "- Reproduce: \`cargo kani --lib -j --output-format terse -Z unstable-options --harness-timeout 10m\` (Kani 0.68.0)"
echo "- Reproduce: \`cargo kani --lib -j 4 --output-format terse -Z unstable-options --harness-timeout 10m\` (Kani 0.68.0)"
echo
echo "The failing harness and its counterexample are in the run log."
} > "$report_file"
Expand Down
Loading
0