Add the is operator to Dafny
#384
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: Build cedar-spec | |
| on: | |
| pull_request: | |
| env: | |
| dotnet-version: 6.0.x # SDK Version for building Dafny | |
| jobs: | |
| build_and_test_dafny: | |
| name: Build and Test Dafny | |
| runs-on: ubuntu-latest | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| toolchain: | |
| - stable | |
| steps: | |
| - name: Checkout cedar-spec | |
| uses: actions/checkout@v3 | |
| - name: Install Z3 | |
| shell: bash | |
| run: | | |
| wget -q --show-progress https://github.com/Z3Prover/z3/releases/download/z3-4.12.1/z3-4.12.1-x64-glibc-2.35.zip | |
| unzip z3-4.12.1-x64-glibc-2.35.zip | |
| echo "$(pwd)/z3-4.12.1-x64-glibc-2.35/bin" >> $GITHUB_PATH | |
| - name: Audit Dafny files | |
| shell: bash | |
| working-directory: ./cedar-dafny | |
| run : | | |
| dotnet tool restore | |
| sudo apt-get install ack | |
| find . -path test -prune -o -name '*.dfy' | xargs -I {} sh -c "printf '%s: ' {} && (dotnet tool run dafny audit {} | ack --passthru --nocolor '0 findings')" | |
| - name: verify dafny | |
| working-directory: ./cedar-dafny | |
| run: make GEN_STATS=1 verify | |
| - name: test dafny | |
| working-directory: ./cedar-dafny | |
| run: make test | |
| - name: log resource usage | |
| working-directory: ./cedar-dafny | |
| run: | | |
| dotnet tool restore | |
| dotnet tool run dafny-reportgenerator summarize-csv-results --max-resource-count 10000000 . || true | |
| build_and_test_drt: | |
| name: Build and Test DRT | |
| runs-on: ubuntu-latest | |
| strategy: | |
| matrix: | |
| toolchain: | |
| - stable | |
| steps: | |
| - name: Checkout cedar-spec | |
| uses: actions/checkout@v3 | |
| with: | |
| submodules: recursive | |
| - name: Get Java 17 | |
| uses: actions/setup-java@v3 | |
| with: | |
| distribution: 'corretto' | |
| java-version: '17' | |
| cache: 'gradle' | |
| - name: Build Dafny def engine | |
| working-directory: ./cedar-dafny | |
| shell: bash | |
| run: make compile-difftest | |
| - name: Build cedar-dafny-java-wrapper | |
| working-directory: ./cedar-dafny-java-wrapper | |
| shell: bash | |
| run: ./gradlew build dumpClasspath | |
| - name: rustup | |
| run: rustup update ${{ matrix.toolchain }} && rustup default ${{ matrix.toolchain }} | |
| - name: cargo fmt (cedar-policy-generators) | |
| working-directory: ./cedar-policy-generators | |
| run: cargo fmt --all --check | |
| - name: cargo fmt (cedar-drt) | |
| working-directory: ./cedar-drt | |
| run: cargo fmt --all --check | |
| - name: cargo fmt (cedar-drt/fuzz/) | |
| working-directory: ./cedar-drt/fuzz | |
| run: cargo fmt --all --check | |
| - name: cargo rustc (cedar-policy-generators) | |
| working-directory: ./cedar-policy-generators | |
| run: RUSTFLAGS="-D warnings -F unsafe-code" cargo build --verbose | |
| - name: cargo rustc (cedar-drt) | |
| working-directory: ./cedar-drt | |
| run: RUSTFLAGS="-D warnings -F unsafe-code" cargo build --verbose | |
| - name: cargo rustc (cedar-drt/fuzz/) | |
| working-directory: ./cedar-drt/fuzz | |
| run: RUSTFLAGS="-D warnings -F unsafe-code" cargo build --verbose | |
| - name: cargo test (cedar-policy-generators) | |
| working-directory: ./cedar-policy-generators | |
| run: cargo test --verbose | |
| - name: cargo test (cedar-drt) | |
| working-directory: ./cedar-drt | |
| shell: bash | |
| run: | | |
| source ./set_env_vars.sh | |
| export LD_LIBRARY_PATH=${LD_LIBRARY_PATH+$LD_LIBRARY_PATH:}$JAVA_HOME/lib/server | |
| cargo test --verbose | |
| build_cedar_lean: | |
| name: Build cedar-lean | |
| runs-on: ubuntu-latest | |
| strategy: | |
| matrix: | |
| toolchain: | |
| - stable | |
| steps: | |
| - name: Checkout cedar-spec | |
| uses: actions/checkout@v3 | |
| with: | |
| submodules: recursive | |
| - name: Install Lean | |
| shell: bash | |
| run: | | |
| wget https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | |
| bash elan-init.sh -y | |
| - name: Build | |
| working-directory: ./cedar-lean | |
| shell: bash | |
| run: source ~/.profile && lake build Cedar | |
| - name: Test | |
| working-directory: ./cedar-lean | |
| shell: bash | |
| run: source ~/.profile && lake exe CedarUnitTests |