Skip to content

Dafny Interoperability Test #1

Dafny Interoperability Test

Dafny Interoperability Test #1

Workflow file for this run

# This workflow is for testing backwards compatibility of a dafny version
# and tests if a project that consumes the mpl will be backwards compatible with
# a newer version of Dafny
name: Dafny Interoperability Test
on:
workflow_dispatch:
inputs:
mpl-dafny:
description: "The Dafny version to compile the MPL with (4.2.0, dafny-nightly, etc..)"
required: true
type: string
mpl-commit:
description: "The MPL commit to use"
required: false
default: "HEAD"
type: string
dbesdk-dafny:
description: "The Dafny version to compile the DBESDK with (4.2.0, dafny-nightly, etc..)"
required: true
type: string
jobs:
dafny-interop-java:
uses: ./.github/workflows/dafny_interop_java.yml
with:
mpl-dafny: ${{inputs.mpl-dafny}}
mpl-commit: ${{inputs.mpl-commit}}
dbesdk-dafny: ${{inputs.dbesdk-dafny}}
# dafny-interop-java-test-vectors:
# uses: ./.github/workflows/ci_test_vector_java.yml
# with:
# mpl-dafny: ${{inputs.mpl-dafny}}
# mpl-commit: ${{inputs.mpl-commit}}
# dbsesdk-dafny: ${{inputs.dbesdk-dafny}}
# dafny-interop-java-examples:
# uses: ./.github/workflows/ci_examples_java.yml
# with:
# mpl-dafny: ${{inputs.mpl-dafny}}
# mpl-commit: ${{inputs.mpl-commit}}
# dbsesdk-dafny: ${{inputs.dbesdk-dafny}}
# dafny-interop-net:
# uses: ./.github/workflows/ci_test_net.yml
# with:
# mpl-dafny: ${{inputs.mpl-dafny}}
# mpl-commit: ${{inputs.mpl-commit}}
# dbsesdk-dafny: ${{inputs.dbesdk-dafny}}
# dafny-interop-net-test-vectors:
# uses: ./.github/workflows/ci_test_vector_net.yml
# with:
# mpl-dafny: ${{inputs.mpl-dafny}}
# mpl-commit: ${{inputs.mpl-commit}}
# dbsesdk-dafny: ${{inputs.dbesdk-dafny}}
# dafny-interop-net-examples:
# uses: ./.github/workflows/ci_examples_net.yml
# with:
# mpl-dafny: ${{inputs.mpl-dafny}}
# mpl-commit: ${{inputs.mpl-commit}}
# dbsesdk-dafny: ${{inputs.dbesdk-dafny}}