Skip to content

Commit

Permalink
Remove unnecessary build step for some workflows (#3124)
Browse files Browse the repository at this point in the history
Workflows that run the perf regressions (`scripts/kani-perf.sh`) do not
need to build Kani, as the perf script itself builds Kani in release
mode:


https://github.com/model-checking/kani/blob/dc0978043c52492112e4ad37a617fd3c8100ef1f/scripts/kani-perf.sh#L12

The extra build step was causing Kani to be built two extra times for
the `benchcomp` flow because the workflow was building it in debug mode,
so the script will end up rebuilding it in release mode. This should
save about 3 minutes for the `benchcomp` flow.
  • Loading branch information
zhassan-aws authored Apr 5, 2024
1 parent a589e57 commit 5131258
Show file tree
Hide file tree
Showing 4 changed files with 0 additions and 19 deletions.
6 changes: 0 additions & 6 deletions .github/workflows/bench.yml
Original file line number Diff line number Diff line change
Expand Up @@ -55,12 +55,6 @@ jobs:
os: ubuntu-20.04
kani_dir: new

- name: Build Kani (new variant)
run: pushd new && cargo build-dev

- name: Build Kani (old variant)
run: pushd old && cargo build-dev

- name: Copy benchmarks from new to old
run: rm -rf ./old/tests/perf ; cp -r ./new/tests/perf ./old/tests/

Expand Down
4 changes: 0 additions & 4 deletions .github/workflows/cbmc-latest.yml
Original file line number Diff line number Diff line change
Expand Up @@ -32,10 +32,6 @@ jobs:
os: ${{ matrix.os }}
kani_dir: 'kani'

- name: Build Kani
working-directory: ./kani
run: cargo build-dev

- name: Checkout CBMC under "cbmc"
uses: actions/checkout@v4
with:
Expand Down
3 changes: 0 additions & 3 deletions .github/workflows/kani-m1.yml
Original file line number Diff line number Diff line change
Expand Up @@ -23,8 +23,5 @@ jobs:
with:
os: macos-13-xlarge

- name: Build Kani
run: cargo build-dev

- name: Execute Kani regression
run: ./scripts/kani-regression.sh
6 changes: 0 additions & 6 deletions .github/workflows/kani.yml
Original file line number Diff line number Diff line change
Expand Up @@ -27,9 +27,6 @@ jobs:
with:
os: ${{ matrix.os }}

- name: Build Kani
run: cargo build-dev

- name: Execute Kani regression
run: ./scripts/kani-regression.sh

Expand Down Expand Up @@ -88,9 +85,6 @@ jobs:
with:
os: ubuntu-20.04

- name: Build Kani using release mode
run: cargo build-dev -- --release

- name: Execute Kani performance tests
run: ./scripts/kani-perf.sh
env:
Expand Down

0 comments on commit 5131258

Please sign in to comment.