Skip to content

feat: make all type conversions public #1164

feat: make all type conversions public

feat: make all type conversions public #1164

# This workflow formally verifies the generated Dafny.
name: Library Dafny verification
on:
pull_request:
push:
branches:
- main-1.x
workflow_dispatch:
# Manual trigger for this workflow, either the normal version
# or the nightly build that uses the latest Dafny prerelease
# (accordingly to the "nightly" parameter).
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 16 * * *"
jobs:
verification:
# Don't run the nightly build on forks
if: github.event_name != 'schedule' || github.repository_owner == 'smithy-lang'
strategy:
matrix:
library: [
TestModels/dafny-dependencies/StandardLibrary, # This stores current Polymorph dependencies that all TestModels depend on
TestModels/Aggregate,
TestModels/AggregateReferences,
TestModels/Constraints,
TestModels/Constructor,
TestModels/Dependencies,
TestModels/Errors,
TestModels/Extendable,
TestModels/Extern,
TestModels/LocalService,
TestModels/Refinement,
TestModels/Resource,
# TestModels/SimpleTypes/BigDecimal,
# TestModels/SimpleTypes/BigInteger,
TestModels/SimpleTypes/SimpleBlob,
TestModels/SimpleTypes/SimpleBoolean,
# TestModels/SimpleTypes/SimpleByte,
TestModels/SimpleTypes/SimpleDouble,
TestModels/SimpleTypes/SimpleEnum,
# TestModels/SimpleTypes/SimpleEnumV2,
# TestModels/SimpleTypes/SimpleFloat,
TestModels/SimpleTypes/SimpleInteger,
TestModels/SimpleTypes/SimpleLong,
# TestModels/SimpleTypes/SimpleShort,
TestModels/SimpleTypes/SimpleString,
# TestModels/SimpleTypes/SimpleTimestamp,
TestModels/Union,
TestModels/aws-sdks/ddb,
TestModels/aws-sdks/kms,
TestModels/aws-sdks/sqs-via-cli,
]
os: [ ubuntu-latest ]
runs-on: ${{ matrix.os }}
env:
DOTNET_CLI_TELEMETRY_OPTOUT: 1
DOTNET_NOLOGO: 1
steps:
- name: Support longpaths
run: |
git config --global core.longpaths true
- uses: actions/checkout@v2
- name: Setup Dafny
uses: dafny-lang/[email protected]
with:
# A && B || C is the closest thing to an if .. then ... else ... or ?: expression the GitHub Actions syntax supports.
dafny-version: ${{ (github.event_name == 'schedule' || inputs.nightly) && 'nightly-latest' || '4.1.0' }}
- name: Generate Polymorph Wrapper Dafny code
shell: bash
working-directory: ./${{ matrix.library }}
run: |
make polymorph_dafny
- name: Verify ${{ matrix.library }} Dafny code
shell: bash
working-directory: ./${{ matrix.library }}
run: |
# This works because `node` is installed by default on GHA runners
CORES=$(node -e 'console.log(os.cpus().length)')
make verify CORES=$CORES
- name: Check solver resource use
shell: bash
working-directory: ./${{ matrix.library }}
run: |
make dafny-reportgenerator