Release 0.4 #4787
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@v4 | |
| - name: Rust fmt | |
| run: | | |
| shopt -s globstar | |
| rustfmt **/*.rs --check | |
| contracts-build: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - name: Cache Cargo build | |
| uses: actions/cache@v4 | |
| with: | |
| path: | | |
| ~/.cargo/registry | |
| ~/.cargo/git | |
| target | |
| key: ${{ runner.os }}-contracts-${{ hashFiles('**/Cargo.lock') }} | |
| - name: Build creusot-contracts with nightly rustc | |
| run: cargo build -p creusot-contracts -F nightly | |
| contracts-build-stable: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - name: Cache Cargo build | |
| uses: actions/cache@v4 | |
| with: | |
| path: | | |
| ~/.cargo/registry | |
| ~/.cargo/git | |
| target | |
| key: ${{ runner.os }}-contracts-stable-${{ hashFiles('**/Cargo.lock') }} | |
| - name: Build creusot-contracts with stable rustc | |
| run: cargo +stable build -p creusot-contracts | |
| build: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - name: Cache Cargo build | |
| uses: actions/cache@v4 | |
| with: | |
| path: | | |
| ~/.cargo/registry | |
| ~/.cargo/git | |
| target | |
| key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }} | |
| restore-keys: ${{ runner.os }}-cargo- | |
| - name: Build | |
| run: cargo build | |
| - name: dummy creusot setup | |
| run: | | |
| mkdir -p ~/.config/creusot | |
| cp ci/creusot-config-dummy.toml ~/.config/creusot/Config.toml | |
| - name: Run tests | |
| run: cargo test | |
| why3: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v4 | |
| 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}} | |
| - name: Cache Cargo build | |
| uses: actions/cache@v4 | |
| with: | |
| path: | | |
| ~/.cargo/registry | |
| ~/.cargo/git | |
| target | |
| key: ${{ runner.os }}-cargo-creusot-${{ hashFiles('prelude/**', '**/Cargo.lock') }} | |
| restore-keys: ${{ runner.os }}-cargo-creusot- | |
| - name: Cache Opam switch | |
| uses: actions/cache/restore@v4 # This cache is saved by the install job | |
| with: | |
| path: ~/.local/share/creusot/_opam | |
| key: ${{ runner.os }}-opam-${{ hashFiles('creusot-deps.opam') }} | |
| restore-keys: ${{ runner.os }}-opam- | |
| - name: Install Opam | |
| uses: ocaml/setup-ocaml@v3 | |
| with: | |
| ocaml-compiler: 5.3.0 | |
| opam-pin: false | |
| - name: Setup environment | |
| run: | | |
| sudo apt update | |
| opam --cli=2.1 var --global in-creusot-ci=true | |
| - name: Install solvers | |
| # Use only 2 parallel provers, because more provers (4) makes replaying proofs unstable | |
| run: | | |
| ./INSTALL --skip-cargo-creusot --skip-creusot-rustc --provers-parallelism 2 | |
| 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 | |
| install: | |
| strategy: | |
| matrix: | |
| os: [ubuntu-latest, macos-latest] | |
| runs-on: ${{ matrix.os }} | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - name: Cache Cargo build | |
| if: matrix.os == 'ubuntu-latest' | |
| uses: actions/cache@v4 | |
| with: | |
| path: | | |
| ~/.cargo/registry | |
| ~/.cargo/git | |
| target | |
| key: ${{ runner.os }}-cargo-install-${{ hashFiles('**/Cargo.lock') }} | |
| - name: Cache Opam switch | |
| if: matrix.os == 'ubuntu-latest' | |
| uses: actions/cache@v4 | |
| with: | |
| path: ~/.local/share/creusot/_opam | |
| key: ${{ runner.os }}-opam-${{ hashFiles('creusot-deps.opam') }} | |
| restore-keys: ${{ runner.os }}-opam- | |
| - name: Cache Opam switch (MacOS) | |
| if: matrix.os == 'macos-latest' | |
| uses: actions/cache@v4 | |
| with: | |
| path: ~/.creusot/_opam | |
| key: ${{ runner.os }}-opam-${{ hashFiles('creusot-deps.opam') }} | |
| restore-keys: ${{ runner.os }}-opam- | |
| - name: Install Opam | |
| uses: ocaml/setup-ocaml@v3 | |
| with: | |
| ocaml-compiler: 5.3.0 | |
| opam-pin: false | |
| - run: sudo apt update | |
| if: matrix.os == 'ubuntu-latest' | |
| - run: opam --cli=2.1 var --global in-creusot-ci=true | |
| - run: ./INSTALL | |
| - name: test cargo creusot new | |
| run: | | |
| set -x | |
| cd .. | |
| cargo creusot new test-project --main --creusot-contracts ../creusot/creusot-contracts | |
| cd test-project | |
| cargo fmt --check | |
| cargo build | |
| cargo creusot | |
| cargo creusot prove | |
| - name: Minimize Opam cache | |
| run: rm -rf ~/.local/share/creusot/_opam/.opam-switch/{build,sources} |