Skip to content
Test documentation

Let Std. example code, and user code using Std., depend on target agnostic interfaces instead of target specific ones #7479

Sign in to view logs

Let Std. example code, and user code using Std., depend on target agnostic interfaces instead of target specific ones

Let Std. example code, and user code using Std., depend on target agnostic interfaces instead of target specific ones #7479

Workflow file for this run

.github/workflows/doc-tests.yml at 2ecab81
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-* ]
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