Clean up benchmark directories after building #2583
Conversation
This commit makes benchcomp delete fresh copies of benchmark directories after running the benchmark suite, by default. This is to save disk space, especially on CI machines which do not have enough disk space to run the perf suite. The new behavior can be turned off with the new --no-cleanup-run-dirs flag.
There was a problem hiding this comment.
Sorry, it's not clear to me what this is actually cleaning and when. Can you please clarify?
In order to test this, I think we need to compare two versions of Kani that use a different toolchain. I think that is the main problem, probably because each toolchain takes around 2GB of disk.
If you have a benchmark directory So for the kani-perf suite, in the CI machine, kani gets cloned, and then benchcomp makes two more copies of it to run with the old and new toolchain... and each of those copies of kani contain the whole git history and object files etc. (I had previously considered making benchcomp ignore |
Description of changes:
This commit makes benchcomp delete fresh copies of benchmark directories after running the benchmark suite, by default. This is to save disk space, especially on CI machines which do not have enough disk space to run the perf suite. The new behavior can be turned off with the new --no-cleanup-run-dirs flag.
Resolved issues:
N/A
Related RFC:
N/A
Call-outs:
Here is a run where the benchcomp job succeeds after deleting the stale benchmark repos.
Testing:
Ran in CI
no
Checklist
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.