Install why3 and why3find in local switch #4736
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 | |
| - uses: actions/cache@v4 | |
| with: | |
| path: | | |
| ~/.cargo/registry | |
| ~/.cargo/git | |
| target | |
| key: ${{ runner.os }}-contracts-${{ hashFiles('creusot-contracts/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 | |
| - uses: actions/cache@v4 | |
| with: | |
| path: | | |
| ~/.cargo/registry | |
| ~/.cargo/git | |
| target | |
| key: ${{ runner.os }}-contracts-stable-${{ hashFiles('creusot-contracts/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 | |
| - uses: actions/cache@v4 | |
| with: | |
| path: | | |
| ~/.cargo/registry | |
| ~/.cargo/git | |
| target | |
| key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }} | |
| - 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-deps: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - uses: actions/cache@v4 | |
| id: cache-opam | |
| with: | |
| path: ~/.local/share/creusot/_opam | |
| key: ${{ runner.os }}-opam-${{ hashFiles('creusot-deps.opam') }} | |
| - uses: ocaml/setup-ocaml@v3 | |
| if: steps.cache-opam.outputs.cache-hit != 'true' | |
| with: | |
| ocaml-compiler: 5.3.0 | |
| - name: Setup environment | |
| if: steps.cache-opam.outputs.cache-hit != 'true' | |
| run: | | |
| sudo apt update | |
| opam --cli=2.1 var --global in-creusot-ci=true | |
| - name: Install Opam dependencies and tools | |
| if: steps.cache-opam.outputs.cache-hit != 'true' | |
| run: ./INSTALL --skip-cargo-creusot --skip-creusot-rustc --skip-extra-tools | |
| - name: Minimize Opam cache | |
| run: rm -rf ~/.local/share/creusot/_opam/.opam-switch/{build,sources} | |
| why3: | |
| needs: why3-deps | |
| 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}} | |
| - uses: actions/cache@v4 | |
| with: | |
| path: | | |
| ~/.cargo/registry | |
| ~/.cargo/git | |
| target | |
| key: ${{ runner.os }}-cargo-creusot-${{ hashFiles('prelude/**', '**/Cargo.lock') }} | |
| - uses: actions/cache@v4 | |
| id: cache-creusot-setup | |
| with: | |
| path: | | |
| ~/.config/creusot | |
| ~/.local/share/creusot | |
| _opam/lib/why3find/packages | |
| key: ${{ runner.os }}-cargo-creusot-setup-${{ hashFiles('prelude/**', 'creusot-deps.opam', 'creusot-setup/src/tools_versions_urls.rs', 'creusot-setup/src/config.rs') }} | |
| - uses: actions/cache/restore@v4 | |
| with: | |
| path: ~./local/share/creusot/_opam | |
| key: ${{ runner.os }}-opam-${{ hashFiles('creusot-deps.opam') }} | |
| fail-on-cache-miss: true | |
| - name: Install solvers | |
| if: steps.cache-creusot-setup.outputs.cache-hit != 'true' | |
| # 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: | |
| needs: why3-deps | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - uses: actions/cache@v4 | |
| with: | |
| path: | | |
| ~/.cargo/registry | |
| ~/.cargo/git | |
| target | |
| key: ${{ runner.os }}-cargo-install-${{ hashFiles('**/Cargo.lock') }} | |
| - uses: actions/cache/restore@v4 | |
| with: | |
| path: ~./local/share/creusot/_opam | |
| key: ${{ runner.os }}-opam-${{ hashFiles('creusot-deps.opam') }} | |
| fail-on-cache-miss: 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 |