Make checker trace more JSON-ish (#911) #1196
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: ci | |
| on: | |
| workflow_dispatch: | |
| push: | |
| branches: [main] | |
| pull_request: | |
| branches: [main] | |
| jobs: | |
| fixpoint: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Clone fixpoint | |
| run: | | |
| git clone https://github.com/ucsd-progsys/liquid-fixpoint | |
| echo "fixpoint_hash=$(git -C liquid-fixpoint/ rev-parse HEAD)" >> $GITHUB_ENV | |
| echo "local_binaries_path=$(pwd)/local-binaries" >> $GITHUB_ENV | |
| - name: Cache fixpoint | |
| uses: actions/cache@v4 | |
| id: cache-fixpoint | |
| with: | |
| path: local-binaries | |
| key: fixpoint-bin-${{ runner.os }}-${{ env.fixpoint_hash }} | |
| - name: Install Haskell | |
| if: steps.cache-fixpoint.outputs.cache-hit != 'true' | |
| uses: haskell-actions/setup@v2.7.0 | |
| with: | |
| enable-stack: true | |
| stack-version: "latest" | |
| - name: Compile fixpoint | |
| if: steps.cache-fixpoint.outputs.cache-hit != 'true' | |
| run: | | |
| cd liquid-fixpoint | |
| stack install --fast --local-bin-path "$local_binaries_path" --flag liquid-fixpoint:-link-z3-as-a-library | |
| - name: Upload Fixpoint | |
| uses: actions/upload-artifact@v4.4.3 | |
| with: | |
| name: fixpoint | |
| path: ${{ env.local_binaries_path }}/fixpoint | |
| tests: | |
| runs-on: ubuntu-latest | |
| needs: fixpoint | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - name: Download Fixpoint | |
| uses: actions/download-artifact@v4.1.8 | |
| with: | |
| name: fixpoint | |
| path: ~/.local/bin/ | |
| - name: Add fixpoint to PATH | |
| run: chmod 755 ~/.local/bin/fixpoint && echo ~/.local/bin >> $GITHUB_PATH | |
| - run: which fixpoint | |
| - name: Install Z3 | |
| uses: cda-tum/setup-z3@v1.6.1 | |
| with: | |
| version: 4.12.1 | |
| platform: linux | |
| env: | |
| GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| - name: Rust Cache | |
| uses: Swatinem/rust-cache@v2.7.5 | |
| - name: Build | |
| run: | | |
| cargo build | |
| - name: Run tests | |
| run: | | |
| which fixpoint && cargo xtask test | |
| vtock: | |
| runs-on: ubuntu-latest | |
| needs: fixpoint | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - name: Download Fixpoint | |
| uses: actions/download-artifact@v4.1.8 | |
| with: | |
| name: fixpoint | |
| path: ~/.local/bin/ | |
| - name: Add fixpoint to PATH | |
| run: chmod 755 ~/.local/bin/fixpoint && echo ~/.local/bin >> $GITHUB_PATH | |
| - name: Install Z3 | |
| uses: cda-tum/setup-z3@v1.6.1 | |
| with: | |
| version: 4.12.1 | |
| platform: linux | |
| env: | |
| GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| - name: Rust Cache | |
| uses: Swatinem/rust-cache@v2.7.5 | |
| - name: Install Flux | |
| run: | | |
| cargo x install | |
| echo ~/.cargo/bin >> $GITHUB_PATH | |
| - name: Clone vtock | |
| run: | | |
| git clone https://github.com/PLSysSec/tock | |
| cp rust-toolchain tock/rust-toolchain.toml | |
| - name: Patch flux-rs dependency if in pull request | |
| if: github.event_name == 'pull_request' | |
| run: | | |
| echo '[patch."https://github.com/flux-rs/flux.git"]' >> tock/Cargo.toml | |
| echo 'flux-rs = { path = "../lib/flux-rs" }' >> tock/Cargo.toml | |
| - name: Check tock/kernel | |
| run: | | |
| cd tock | |
| cargo flux -p kernel | |
| rustfmt: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - name: Rust Cache | |
| uses: Swatinem/rust-cache@v2.7.5 | |
| - name: Rust rustfmt | |
| run: cargo fmt --check | |
| clippy: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - name: Add clippy | |
| run: rustup component add clippy | |
| - name: Rust Cache | |
| uses: Swatinem/rust-cache@v2.7.5 | |
| - name: Run check | |
| run: RUSTFLAGS="-Dwarnings" cargo check | |
| - name: Run clippy | |
| uses: actions-rs/clippy-check@v1.0.7 | |
| with: | |
| token: ${{ secrets.GITHUB_TOKEN }} |