doc-tests.yml

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 update && 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