Skip to content

Implement decreases to expressions #9357

Implement decreases to expressions

Implement decreases to expressions #9357

Workflow file for this run

name: Test documentation
## Tests various aspects of documentation
## -- Examples are well-formed and verify when expected
## (Building the pdf is separately tested, in refman.yml)
##
## The tests only need to run on one OS -- Linux is used because the test scripts are bash
on:
workflow_dispatch:
pull_request:
branches: [ master, main-* ]
merge_group:
concurrency:
group: ${{ github.workflow }}-${{ github.ref }}
cancel-in-progress: true
jobs:
check-deep-tests:
uses: ./.github/workflows/check-deep-tests-reusable.yml
doctests:
needs: check-deep-tests
if: always() && (( github.event_name == 'pull_request' && (needs.check-deep-tests.result == 'success' || contains(github.event.pull_request.labels.*.name, 'run-deep-tests'))) || ( github.event_name == 'push' && ( github.ref_name == 'master' || vars.TEST_ON_FORK == 'true' )))
runs-on: ubuntu-latest
steps:
- name: Setup dotnet
uses: actions/setup-dotnet@v4
with:
dotnet-version: 6.0.x
- name: Checkout Dafny
uses: actions/checkout@v4
with:
submodules: recursive
path: dafny
- name: Load Z3
run: |
sudo apt-get install -qq libarchive-tools
mkdir -p dafny/Binaries/z3/bin
wget -qO- https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02/z3-4.12.1-x64-ubuntu-20.04-bin.zip | bsdtar -xf -
mv z3-* dafny/Binaries/z3/bin/
chmod +x dafny/Binaries/z3/bin/z3-*
- name: Build Dafny
run: dotnet build dafny/Source/Dafny.sln
- name: Check generated error catalog
run: |
which java
chmod +x dafny/docs/HowToFAQ/make-error-catalog
./dafny/docs/HowToFAQ/make-error-catalog
- name: Check Error Catalog examples
run: |
cd dafny/docs
chmod +x ./check-examples
PATH=../bin:$PATH ./check-examples HowToFAQ/Errors-*.md || ( echo Tests Failed; exit 1 ) && echo Tests Succeeded
- name: Check OnlineTutorial examples
run: |
cd dafny/docs
chmod +x ./check-examples
PATH=../bin:$PATH ./check-examples OnlineTutorial/*.md || ( echo Tests Failed; exit 1 ) && echo Tests Succeeded
- name: Check Reference Manual examples
run: |
cd dafny/docs
chmod +x ./check-examples
PATH=../bin:$PATH ./check-examples DafnyRef/*.md || ( echo Tests Failed; exit 1 ) && echo Tests Succeeded
- name: Check ProofOptimization examples
run: |
cd dafny/docs
chmod +x ./check-examples
PATH=../bin:$PATH ./check-examples ProofOptimization/*.md || ( echo Tests Failed; exit 1 ) && echo Tests Succeeded