Do not trigger queries during metadata encoding for (implicitly) igno… #2961
This file contains hidden or 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] | |
| types: [opened, synchronize, reopened, ready_for_review] | |
| jobs: | |
| tests: | |
| strategy: | |
| matrix: | |
| os: [ubuntu-latest, macos-latest, windows-latest] | |
| runs-on: ${{ matrix.os }} | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - name: Install fixpoint | |
| uses: ./.github/actions/install-fixpoint | |
| env: | |
| GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| - name: Install Z3 | |
| uses: cda-tum/setup-z3@v1.6.6 | |
| with: | |
| version: 4.12.1 | |
| - name: Rust Cache | |
| uses: Swatinem/rust-cache@v2.8.0 | |
| - name: Run tests | |
| run: | | |
| cargo xtask test | |
| vtock: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - name: Install fixpoint | |
| uses: ./.github/actions/install-fixpoint | |
| env: | |
| GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| # Older versions hang | |
| - name: Install Z3 | |
| uses: cda-tum/setup-z3@v1.6.6 | |
| with: | |
| version: 4.15.3 | |
| - name: Rust Cache | |
| uses: Swatinem/rust-cache@v2.8.0 | |
| - 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.toml 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 | |
| echo 'flux-core = { path = "../lib/flux-core" }' >> tock/Cargo.toml | |
| echo 'flux-alloc = { path = "../lib/flux-alloc" }' >> tock/Cargo.toml | |
| - name: Check tock/kernel | |
| run: | | |
| cd tock | |
| cargo flux -p cortexm -p rv32i | |
| lean-demo: | |
| strategy: | |
| matrix: | |
| os: [ubuntu-latest, macos-latest] | |
| runs-on: ${{ matrix.os }} | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - name: Install Lean via elan | |
| run: | | |
| curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y | |
| echo "$HOME/.elan/bin" >> $GITHUB_PATH | |
| - name: Install fixpoint | |
| uses: ./.github/actions/install-fixpoint | |
| env: | |
| GITHUB_TOKEN: | |
| ${{ secrets.GITHUB_TOKEN }} | |
| # Older versions hang | |
| - name: Install Z3 | |
| uses: cda-tum/setup-z3@v1.6.6 | |
| with: | |
| version: 4.15.3 | |
| - name: Rust Cache | |
| uses: Swatinem/rust-cache@v2.8.0 | |
| - name: Install Flux | |
| run: | | |
| cargo x install | |
| echo ~/.cargo/bin >> $GITHUB_PATH | |
| - name: Clone flux-to-lean-demo | |
| run: | | |
| git clone https://github.com/flux-rs/flux-to-lean-demo | |
| - name: Generate Lean Project | |
| continue-on-error: true | |
| working-directory: flux-to-lean-demo | |
| run: | | |
| cargo flux | |
| - name: Copy proofs | |
| working-directory: flux-to-lean-demo | |
| run: | | |
| cp -r LeanUserProofs/* lean_proofs/LeanProofs/User/ | |
| - name: Run lean | |
| working-directory: flux-to-lean-demo | |
| run: | | |
| cd lean_proofs && lake build | |
| - name: Check proofs in flux | |
| run: | | |
| cargo flux | |
| rustfmt: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - name: Rust Cache | |
| uses: Swatinem/rust-cache@v2.8.0 | |
| - name: Rust rustfmt | |
| run: cargo fmt --check | |
| clippy: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - name: Rust cache | |
| uses: Swatinem/rust-cache@v2.8.0 | |
| - name: Run cargo check | |
| run: RUSTFLAGS="-Dwarnings" cargo check | |
| - name: Run clippy | |
| run: cargo clippy |