Fix a soundness issue that could be triggered by calling ensures fres… #16725
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 DafnyRef.pdf | |
| 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 | |
| build-refman: | |
| 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: ${{ matrix.os }} | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| os: [ ubuntu-22.04 ] | |
| steps: | |
| - name: OS | |
| run: echo ${{ runner.os }} ${{ matrix.os }} | |
| - 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: Build Dafny | |
| run: dotnet build dafny/Source/Dafny.sln | |
| - name: Install pandoc - Linux | |
| if: runner.os == 'Linux' | |
| run: | | |
| wget https://github.com/jgm/pandoc/releases/download/3.1.7/pandoc-3.1.7-1-amd64.deb | |
| sudo dpkg -i *.deb | |
| rm -rf *.deb | |
| pandoc -v | |
| sudo gem install rouge | |
| - name: Install pandoc - MacOS | |
| if: runner.os == 'MacOS' | |
| run: | | |
| unset HOMEBREW_NO_INSTALL_FROM_API | |
| brew untap Homebrew/core | |
| brew update-reset && brew update | |
| brew install pandoc | |
| pandoc -v | |
| sudo gem install rouge -v 3.30.0 | |
| - name: Install Tectonic | |
| uses: wtfjoke/setup-tectonic@v3 | |
| with: | |
| github-token: ${{ secrets.GITHUB_TOKEN }} | |
| tectonic-version: 0.15 | |
| - name: Build reference manual | |
| run: | | |
| eval "$(/usr/libexec/path_helper)" | |
| rm -f dafny/docs/DafnyRef/DafnyRef.pdf | |
| make -C dafny/docs/DafnyRef | |
| - name: Check | |
| run: ls -la dafny/docs/DafnyRef/DafnyRef.pdf | |
| - uses: actions/upload-artifact@v4 | |
| if: always() | |
| with: | |
| name: DafnyRef | |
| path: dafny/docs/DafnyRef/DafnyRef.pdf | |
| # Building the reference manual may update files, | |
| # such as renumbering sections or updating Options.txt. | |
| # These changes should have been checked in earlier, | |
| # so fail the build if anything changed. | |
| - name: Check for modifications | |
| run: 'git diff --exit-code || (echo "ERROR: Source changes detected (see above). Build the reference manual locally and commit these changes." && exit 1)' | |
| working-directory: dafny |