New VCGen for logic functions #3298
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: Rust | |
| on: | |
| push: | |
| branches: [ master ] | |
| pull_request: | |
| branches: [ master ] | |
| env: | |
| CARGO_TERM_COLOR: always | |
| jobs: | |
| fmt: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v2 | |
| - name: Rust fmt | |
| run: | | |
| shopt -s globstar | |
| rustfmt **/*.rs --check | |
| contracts-build: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v2 | |
| - uses: actions/cache@v2 | |
| with: | |
| path: | | |
| ~/.cargo/registry | |
| ~/.cargo/git | |
| target | |
| key: ${{ runner.os }}-contracts-${{ hashFiles('creusot-contracts/Cargo.lock') }} | |
| - name: Build creusot-contracts with rustc | |
| run: cargo build -p creusot-contracts | |
| build: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v2 | |
| - uses: actions/cache@v2 | |
| with: | |
| path: | | |
| ~/.cargo/registry | |
| ~/.cargo/git | |
| target | |
| key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }} | |
| - name: Build | |
| run: cargo build | |
| - name: dummy creusot setup | |
| run: cp -r .creusot-config.sample .creusot-config | |
| - name: Run tests | |
| run: cargo test | |
| why3: | |
| runs-on: ubuntu-22.04 | |
| steps: | |
| - uses: actions/checkout@v2 | |
| with: | |
| fetch-depth: ${{ github.event.pull_request.commits }} | |
| - name: Fetch target branch | |
| if: github.base_ref | |
| run: git fetch --no-tags --prune --depth=1 origin +refs/heads/${{github.base_ref}}:refs/remotes/origin/${{github.base_ref}} | |
| - uses: actions/cache@v2 | |
| with: | |
| path: | | |
| ~/.cargo/registry | |
| ~/.cargo/git | |
| ~/.cache/creusot | |
| target | |
| key: ${{ runner.os }}-cargo-creusot-${{ hashFiles('**/Cargo.lock', 'creusot-setup/src/tools_versions_urls.rs') }} | |
| - uses: dawidd6/action-download-artifact@v2 | |
| with: | |
| workflow: why3.yml | |
| name: why3 | |
| path: /home/runner/work/creusot/why3 | |
| - name: setup paths for why3 and alt-ergo | |
| run: | | |
| chmod -R +x ~/work/creusot/why3/bin | |
| chmod -R +x ~/work/creusot/why3/lib/why3/why3server | |
| echo ~/work/creusot/why3/bin >> $GITHUB_PATH | |
| mv ~/work/creusot/why3/alt-ergo /usr/local/bin/alt-ergo | |
| chmod +x /usr/local/bin/alt-ergo | |
| echo $(/usr/local/bin/alt-ergo --version) | |
| - name: run cargo creusot setup install | |
| run: | | |
| cargo run --bin cargo-creusot creusot setup install | |
| echo -e "\n>> ~/.config/creusot/Config.toml:\n" | |
| cat ~/.config/creusot/Config.toml | |
| echo -e "\n>> ~/.config/creusot/.why3.conf:\n" | |
| cat ~/.config/creusot/.why3.conf | |
| - run: cargo test --test why3 "" -- --replay=none --diff-from=origin/master | |
| - run: cargo test --test why3 "" -- --skip-unstable |