Skip to content

Commit

Permalink
Add disk space output to debug occasional test failures
Browse files Browse the repository at this point in the history
Despite freeing up disk space early on, we saw occasional failures like
https://github.com/model-checking/kani/actions/runs/7030685174/job/19130721957
that look like running out of disk space.

This change should be reverted once we have diagnosed the problem.
  • Loading branch information
tautschnig committed Nov 30, 2023
1 parent 725bc77 commit b4387dd
Showing 1 changed file with 4 additions and 0 deletions.
4 changes: 4 additions & 0 deletions scripts/kani-regression.sh
Original file line number Diff line number Diff line change
Expand Up @@ -101,8 +101,12 @@ cargo kani --manifest-path "$FEATURES_MANIFEST_PATH" --harness trivial_success
cargo clean --manifest-path "$FEATURES_MANIFEST_PATH"

# Check that documentation compiles.
echo "Current disk usage:"
df -h
echo "Starting doc tests:"
cargo doc --workspace --no-deps --exclude std
echo "Disk usage after documentation build:"
df -h

echo
echo "All Kani regression tests completed successfully."
Expand Down

0 comments on commit b4387dd

Please sign in to comment.