Indexing of FMap in logic
#4288
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: | | |
| mkdir -p ~/.config/creusot | |
| cp ci/creusot-config-dummy.toml ~/.config/creusot/Config.toml | |
| - 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 | |
| target | |
| key: ${{ runner.os }}-cargo-creusot-${{ hashFiles('**/Cargo.lock') }} | |
| - uses: actions/cache@v2 | |
| id: cache-creusot-setup | |
| with: | |
| path: | | |
| ~/.config/creusot | |
| ~/.local/share/creusot | |
| key: ${{ runner.os }}-cargo-creusot-setup-${{ hashFiles('creusot-deps.opam', 'creusot-setup/src/tools_versions_urls.rs', 'creusot-setup/src/config.rs') }} | |
| - uses: actions/cache@v2 | |
| id: cache-opam | |
| with: | |
| path: | | |
| /home/runner/work/creusot/creusot/_opam | |
| key: ${{ runner.os }}-opam-${{ hashFiles('creusot-deps.opam') }} | |
| - uses: ocaml/setup-ocaml@v2 | |
| if: steps.cache-opam.outputs.cache-hit != 'true' | |
| with: | |
| ocaml-compiler: 4.14.1 | |
| - name: install opam dependencies | |
| if: steps.cache-opam.outputs.cache-hit != 'true' | |
| run: | | |
| opam switch | |
| opam --cli=2.1 var --global in-creusot-ci=true | |
| opam install . | |
| mkdir /tmp/to-delete | |
| opam info --list-files why3 > keep | |
| sed -i 's/^.*\/_opam\///' keep | |
| rsync -a -r --remove-source-files --exclude-from=keep _opam/ /tmp/to-delete | |
| - name: setup opam PATH | |
| run: | | |
| echo /home/runner/work/creusot/creusot/_opam/bin >> $GITHUB_PATH | |
| - name: run cargo creusot setup install | |
| if: steps.cache-creusot-setup.outputs.cache-hit != 'true' | |
| 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 |