Build and Test #192
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 and Test | |
| on: | |
| push: | |
| branches: [ main ] | |
| pull_request: | |
| branches: [ main ] | |
| workflow_dispatch: | |
| inputs: | |
| nightly: | |
| description: 'Run the nightly build' | |
| required: false | |
| type: boolean | |
| schedule: | |
| # Nightly build against Dafny's nightly prereleases, | |
| # for early warning of verification issues or regressions. | |
| # Timing chosen to be adequately after Dafny's own nightly build, | |
| # but this might need to be tweaked: | |
| # https://github.com/dafny-lang/dafny/blob/master/.github/workflows/deep-tests.yml#L16 | |
| - cron: "30 8 * * *" | |
| jobs: | |
| build: | |
| # Don't run the nightly build on forks | |
| if: github.event_name != 'schedule' || github.repository_owner == 'dafny-lang' | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v2 | |
| with: | |
| submodules: recursive | |
| - name: Set up .NET | |
| uses: actions/setup-dotnet@v1 | |
| with: | |
| dotnet-version: 6.0.x | |
| - name: Setup Dafny | |
| uses: dafny-lang/[email protected] | |
| with: | |
| dafny-version: ${{ (github.event_name == 'schedule' || inputs.nightly) && 'nightly-latest' || '3.7.1' }} | |
| - name: Verify Dafny code | |
| run: dotnet build -t:VerifyDafny -p:VerifyDafnyJobs=2 -p:TestVerifyOverride="verificationLogger:csv" | |
| - name: Run Tests | |
| run: | | |
| dotnet test --verbosity normal | |
| # Ensure failure on a concrete CSV with inconsistent outcomes | |
| ! dotnet run --project src -- summarize-csv-results test/diff-outcomes.csv | |
| # Ensure success on a concrete CSV with inconsistent outcomes if asked for | |
| dotnet run --project src -- summarize-csv-results --allow-different-outcomes test/diff-outcomes.csv | |
| - name: Self Report | |
| # Generates a report based on the logged data from verifying itself. | |
| # This is both a guard against unstable verification and a smoke test of the tool itself. | |
| run: dotnet run --project src -- summarize-csv-results --max-resource-count 900000 . | |
| - name: Stability Analysis | |
| # Analyzes the stability of verification by running it several | |
| # more times and calculating statistics | |
| # | |
| # Runs Dafny directly because it doesn't seem like we can pass | |
| # multiple arguments to it through MSBuild. | |
| run: | | |
| DFYS=`find src test -name "*.dfy"` | |
| dafny /compile:0 /timeLimit:30 /verificationLogger:csv /randomSeedIterations:5 ${DFYS} | |
| dotnet run --project src -- summarize-csv-results --max-resource-stddev 10000 . | |
| dotnet run --project src -- summarize-csv-results --max-resource-cv-pct 5 . |