Skip to content

Fix reveal statement inside witness bug #3678

Fix reveal statement inside witness bug

Fix reveal statement inside witness bug #3678

name: Build and Test Dafny Standard Libraries
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
build:
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: macos-13
steps:
- name: Checkout Dafny
uses: actions/checkout@v4
with:
submodules: true
- name: Set up JDK 18
uses: actions/setup-java@v4
with:
java-version: 18
distribution: corretto
- name: Set up Go
uses: actions/setup-go@v5
with:
go-version: '1.21'
cache: false
- name: Set up goimports
env:
GO111MODULE: on
run: go install golang.org/x/tools/cmd/goimports@latest
- name: Build Dafny
run: dotnet build Source/Dafny.sln
- name: Get Z3
run: make z3-mac
- run: npm install bignumber.js
- name: Test DafnyStandardLibraries
run: make -C Source/DafnyStandardLibraries all