Improve error messages using annotate-snippets #6763
Workflow file for this run
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: Rust | |
| on: | |
| push: | |
| branches: [ master ] | |
| pull_request: | |
| branches: [ master ] | |
| concurrency: | |
| group: ${{ github.workflow }}-${{ github.ref }} | |
| cancel-in-progress: true | |
| 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 | |
| creusot-std-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 }}-creusot-std-${{ hashFiles('**/Cargo.lock') }} | |
| - name: Build creusot-std with nightly rustc | |
| run: cargo build -p creusot-std -F nightly | |
| env: | |
| RUSTFLAGS: -D warnings | |
| creusot-std-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 }}-creusot-std-stable-${{ hashFiles('Cargo.lock') }} | |
| - name: Build creusot-std with stable rustc | |
| run: cargo +stable build -p creusot-std | |
| env: | |
| RUSTFLAGS: -D warnings | |
| 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', 'prelude-generator/**') }} | |
| - name: Build | |
| run: cargo build | |
| - name: Run tests | |
| run: cargo test | |
| - run: cargo test --test why3 dummy-dummy-dummy # make sure its deps are in the cargo cache | |
| build-nix: | |
| runs-on: ubuntu-latest | |
| env: | |
| NIXPKGS_ALLOW_UNFREE: 1 # Allow the use of unfree software (Alt-Ergo) | |
| permissions: | |
| actions: write # Allow to purge the cache | |
| steps: | |
| - uses: actions/checkout@v5 | |
| - uses: nixbuild/nix-quick-install-action@v34 | |
| - uses: nix-community/cache-nix-action@v6 | |
| with: | |
| primary-key: nix-${{ runner.os }}-${{ hashFiles('**/flake.lock') }} | |
| gc-max-store-size: 10G | |
| purge: true | |
| - name: Check framework versions | |
| run: | | |
| cargo_version () { grep "$1_VERSION" creusot-setup/src/tools_versions_urls.rs | cut -d '"' -f2; } | |
| opam_version () { cat creusot-deps.opam | grep -m 1 $1 | cut -d '"' -f 4 | cut -c5-; } | |
| nix_version () { nix eval --json --impure .#why3Framework.passthru."$1".version | cut -d '"' -f2; } | |
| [[ $(nix_version why3) == "$(opam_version why3)"* ]] | |
| [[ $(nix_version why3find) == "$(opam_version why3find)"* ]] | |
| [[ $(nix_version alt-ergo) == $(cargo_version ALTERGO) ]] | |
| [[ $(nix_version cvc4) == $(cargo_version CVC4) ]] | |
| [[ $(nix_version cvc5) == $(cargo_version CVC5) ]] | |
| [[ $(nix_version z3) == $(cargo_version Z3) ]] | |
| - name: Build | |
| run: nix build --impure . --print-build-logs | |
| - name: Run tests | |
| run: nix shell --impure --command bash -c "cd .. && cargo creusot new test-project && cd test-project && cargo creusot prove" | |
| erasure-check: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - name: Cache Cargo build | |
| uses: actions/cache/restore@v4 | |
| with: | |
| path: | | |
| ~/.cargo/registry | |
| ~/.cargo/git | |
| target | |
| key: ${{ runner.os }}-cargo-${{ hashFiles('Cargo.lock', 'prelude-generator/**') }} | |
| - name: Build | |
| run: cargo build | |
| - name: Run tests | |
| run: ./t erasure-check | |
| 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/restore@v4 | |
| with: | |
| path: | | |
| ~/.cargo/registry | |
| ~/.cargo/git | |
| target | |
| key: ${{ runner.os }}-cargo-${{ hashFiles('Cargo.lock', 'prelude-generator/**') }} | |
| restore-keys: ${{ runner.os }}-cargo- | |
| - 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: Get current date | |
| run: echo "TODAY=$(date +'%Y-%m-%d')" >> $GITHUB_ENV | |
| - name: Restore Why3find cache | |
| uses: actions/cache/restore@v4 | |
| with: | |
| path: target/.why3find | |
| key: ${{ runner.os }}-why3find-${{ env.TODAY }}- | |
| - name: Setup environment | |
| run: | | |
| sudo apt update && sudo apt install opam libzmq3-dev | |
| opam init --bare | |
| 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/why3.conf:\n" | |
| cat ~/.config/creusot/why3.conf | |
| - run: ./t why3 --why3-all | |
| - name: Save Why3find cache | |
| uses: actions/cache/save@v4 | |
| with: | |
| path: target/.why3find | |
| key: ${{ runner.os }}-why3find-${{ env.TODAY }}-${{ hashFiles('target/.why3find/**') }} | |
| install: | |
| strategy: | |
| matrix: | |
| os: [ubuntu-latest, macos-latest] | |
| runs-on: ${{ matrix.os }} | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - run: rustup update | |
| if: matrix.os == 'macos-latest' | |
| - name: Cache Cargo build | |
| if: matrix.os == 'ubuntu-latest' | |
| uses: actions/cache/restore@v4 | |
| with: | |
| path: | | |
| ~/.cargo/registry | |
| ~/.cargo/git | |
| target | |
| key: ${{ runner.os }}-cargo-${{ hashFiles('Cargo.lock', 'prelude-generator/**') }} | |
| restore-keys: ${{ runner.os }}-cargo- | |
| - name: Cache Cargo build | |
| if: matrix.os == 'macos-latest' | |
| uses: actions/cache@v4 | |
| with: | |
| path: | | |
| ~/.cargo/registry | |
| ~/.cargo/git | |
| target | |
| key: ${{ runner.os }}-cargo-${{ hashFiles('Cargo.lock', 'prelude-generator/**') }} | |
| restore-keys: ${{ runner.os }}-cargo- | |
| - 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- | |
| - run: sudo apt update && sudo apt install opam libzmq3-dev | |
| if: matrix.os == 'ubuntu-latest' | |
| - run: brew update && brew install opam autoconf zeromq zlib | |
| if: matrix.os == 'macos-latest' | |
| - name: setup opam | |
| run: | | |
| opam init --bare | |
| opam --cli=2.1 var --global in-creusot-ci=true | |
| - run: ./INSTALL | |
| - name: Build doc of creusot-std | |
| run: cargo creusot doc | |
| env: | |
| RUSTDOCFLAGS: -D warnings | |
| - name: test cargo creusot new | |
| run: ./t build-new | |
| - name: test no_std build | |
| run: ./t build-no-std | |
| - name: Minimize Opam cache | |
| run: opam clean --all-switches --download-cache --logs --repo-cache |