Add check to ensure generics for sorts are correct #1032
Workflow file for this run
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/[email protected] | |
| 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/[email protected] | |
| 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/[email protected] | |
| with: | |
| name: fixpoint | |
| path: ${{ env.local_binaries_path }}/fixpoint | |
| tests: | |
| runs-on: ubuntu-latest | |
| needs: fixpoint | |
| steps: | |
| - uses: actions/checkout@v3 | |
| - name: Download Fixpoint | |
| uses: actions/[email protected] | |
| 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/[email protected] | |
| with: | |
| version: 4.12.1 | |
| platform: linux | |
| env: | |
| GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| - name: Rust Cache | |
| uses: Swatinem/[email protected] | |
| - 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@v3 | |
| - name: Download Fixpoint | |
| uses: actions/[email protected] | |
| 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/[email protected] | |
| with: | |
| version: 4.12.1 | |
| platform: linux | |
| env: | |
| GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| - name: Rust Cache | |
| uses: Swatinem/[email protected] | |
| - 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.crates-io]' >> 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@v3 | |
| - name: Rust Cache | |
| uses: Swatinem/[email protected] | |
| - name: Rust rustfmt | |
| run: cargo fmt --check | |
| clippy: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v3 | |
| - name: Add clippy | |
| run: rustup component add clippy | |
| - name: Rust Cache | |
| uses: Swatinem/[email protected] | |
| - name: Run clippy | |
| uses: actions-rs/[email protected] | |
| with: | |
| token: ${{ secrets.GITHUB_TOKEN }} |