Enable Dafny support in Gradle

[keyboardDrummer]

Summary

Gradle allows creating complicated build setups for multiple languages, which is great for Dafny since Dafny customers may often want to trigger builds in languages other than Dafny as well.

Background and Motivation

_

Proposed Feature

Create a Dafny plugin for Gradle that exposes various Dafny commands, such as verify and translate, inside Gradle. The plugin will use the Gradle specification to generate a Dafny project file, and invoke the Dafny CLI on that. This way, Dafny IDEs that depend on a Dafny project file can also make use of this Gradle plugin.

By using the generated sources as input sources for compiling Gradle tasks, users can setup Java or .NET builds that depend on Dafny sources.

Examples

The resulting build.gradle could look something like this:

apply plugin: 'dafny-gradle'

// Will call `dafny translate --library=libs/dependencyA --library=libs/dependencyB --language=java --output="<something>/generated-src" src/dafny/**`
dafny.sources = 'src/dafny'
dafny.libraries = ['libs/dependencyA','libs/dependencyB']
dafny.language = 'java'
dafny.output = 'generated-src'

// Configure the Java plugin to pick up the sources generated by the Dafny plugin
sourceSets.main.java.srcDirs = ['src/application', 'src/extern-implementations', 'generated-src']

dependencies {
    // Java dependencies, including the ones required by the extern implementations,
    // can be defined by deferring to existing Java dependency management systems
    implementation...
    ...
}

Alternatives

No response

[robin-aws]

I really like this approach. It's similar in spirit to the existing dafny.msbuild plugin, but it seems like we'll get more milage out of it given Gradle seems to support multiple languages, and multi-language projects, by design. I'm not a Gradle expert by any stretch so forgive some basic questions to help me understand better.

I assume that once we have support for remote Dafny dependencies (#3007) we'd want to specify Dafny dependencies in the dependencies section as well, instead of with the dafny.libraries option. Given that, would it make more sense to use the dependencies section right away? Gradle seems to have different flavors of dependencies we could use for the local use case, such as "file dependencies": https://docs.gradle.org/current/userguide/declaring_dependencies.html#sub:file_dependencies. Using /library to make that work would just be implementation details.

You've got dafny.language as a single value, but I suspect some Dafny projects will want to compile the same Dafny source to multiple target languages. Would that fit into the generic Gradle build steps well enough, even if the implementation would end up invoking dafny multiple times? A common pattern in our test suite is doing one call to verify, and then one call for each target language without verification to save time. It would be great to encapsulate that implementation behind a simple Gradle configuration, especially since then we could optimize later by having dafny itself support multiple target outputs at once.

We should be very clear on exactly how much this would overlap with the project file support (#2907). Some intentional overlap could be beneficial but we should probably minimize it.

[keyboardDrummer]

I assume that once we have support for remote Dafny dependencies (#3007) we'd want to specify Dafny dependencies in the dependencies section as well, instead of with the dafny.libraries option

It seems would be more idiomatic to Gradle, the C++ plugin also defines dependencies there (link), although I don't understand the semantics of that section.

You've got dafny.language as a single value, but I suspect some Dafny projects will want to compile the same Dafny source to multiple target languages. Would that fit into the generic Gradle build steps well enough, even if the implementation would end up invoking dafny multiple times?

It seems simpler to me to keep it like this for now. I don't think we're closing any doors by doing a single dafny call initially.

We should be very clear on exactly how much this would overlap with the project file support (#2907). Some intentional overlap could be beneficial but we should probably minimize it.

I think there should be a Gradle task defined by the Gradle Dafny plugin to generate a Dafny project file, so IDEs can use that.