Skip to content

Commit

Permalink
Add disk space output to debug occasional test failures (#2905)
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 5fc7172
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 5fc7172

Please sign in to comment.