Move runtimes into distinct project in the solution

[camrein]

This issue is related to #1529.
Until now, it was sufficient to have a recent .NET SDK installed to build Dafny. With the merge of #680, it became a bit more cumbersome. One now needs to install and configure Java 8, although Dafny is mostly C#. Since all projects of Dafny's solution depend somehow on DafnyRuntime, it makes the whole build fail if you do not have the correct Java version configured in the path.
I suggest moving the non C# runtimes into a distinct project to avoid failing the complete build of Dafny.

Alternatively, we can make at least the java runtime optional. For example like this:

<!-- Only copy the java runtime if it exists -->
<Content Include="DafnyRuntimeJava\build\libs\DafnyRuntime.jar" Link="DafnyRuntime.jar" CopyToOutputDirectory="PreserveNewest" Condition="Exists('DafnyRuntimeJava\build\libs\DafnyRuntime.jar')" />

<!-- Ignore the failing gradle build -->
<Exec WorkingDirectory="DafnyRuntimeJava" Command="./gradlew -q clean build" IgnoreExitCode="true" />

However, this might reduce the awareness that the build is incomplete.

[keyboardDrummer]

I think DafnyPipeline doesn't need to depend on DafnyRuntime, as it does now, but making fewer projects depend on DafnyRuntime doesn't seem like much of a solution to me since building the entire Dafny solution will still include building DafnyRuntime and thus require an installed Java SDK.

The cleanest solution I see it is to have the Dafny Java back-end be in a separate .NET solution. We could use this pattern for other languages as well. Running the Dafny test-suite for most languages requires installing some language specific components. The current wiki reads: "The tests in the Test/comp folder run the Dafny compiler to produce code for .NET, Java, JavaScript, and Go. If you don't have all the dependencies installed, many tests will fail."

Note that making the above change might be some work. Would it be okay to leave the requirement to have Java SDK installed exist for the time being, or do you think it complicates contributions too much?

[camrein]

I think DafnyPipeline doesn't need to depend on DafnyRuntime, as it does now, but making fewer projects depend on DafnyRuntime doesn't seem like much of a solution to me since building the entire Dafny solution will still include building DafnyRuntime and thus require an installed Java SDK.

Removing the unnecessary dependency would even be better in my opinion. The undesirable effect I've observed is that now all projects fail to build because they depend on DafnyRuntime. If it's solely the DafnyRuntime project whose build fails, that's perfectly fine (even if the solution as a whole fails). Removing this dependency allows building the Dafny compiler and language server without requiring Java.

The cleanest solution I see it is to have the Dafny Java back-end be in a separate .NET solution. We could use this pattern for other languages as well. Running the Dafny test-suite for most languages requires installing some language specific components. The current wiki reads: "The tests in the Test/comp folder run the Dafny compiler to produce code for .NET, Java, JavaScript, and Go. If you don't have all the dependencies installed, many tests will fail."

That makes sense. This would make it easier for people to understand the reason for the additional dependencies. Moreover, in the future, this would allow creating new projects to support other languages. It'll make it easier to distinguish which runtime fails to build and why.

Note that making the above change might be some work. Would it be okay to leave the requirement to have Java SDK installed exist for the time being, or do you think it complicates contributions too much?

For me it's fine. But having seen other projects I think it's a huge letdown if there are tons of prerequisites necessary to build a project on your own. Moreover, I think there are many people that compile Dafny from the source to have the most recent compiler features. Therefore, we should keep the entry barrier as low as possible. So if it's possible to build all projects except for DafnyRuntime, I think that'd be great.

[robin-aws]

I noticed while working on #680 that it was odd for DafnyPipeline to depend on DafnyRuntime, since you would think the compilers shouldn't depend on any runtime code, but instead only emit code that does. For the record, as they are currently constructed this dependency is not completely unnecessary, because the C# compiler depends on the textual content of DafnyRuntime.cs - unless /useRuntimeLib is provided, the compiler prepends DafnyRuntime.cs to the generated C# output.

Technically it is possible to remove this dependency, as long as the runtimes are build and included in any test packages that actually run compiled Dafny code (such as IntegrationTests) and the actual published zip files. I'll add that to my follow up PR (#1534) and verify it passes the CI.

[robin-aws]

Looks like I can't quite break the dependency entirely - trying to read the DafnySourceAttribute out of a dll built by Dafny using /useRuntimeLib forces the resolution of its dependencies, and without a dependency on DafnyRuntime.dll in the projects it fails to load. This is actually a regression, since it used to use Mono.Cecil to read the metadata out of the dll without loading it, but we lost that when we migrated to .NET Core: https://github.com/dafny-lang/dafny/pull/794/files?authenticity_token=cjKZTuCnPaMU5OXpxh5I4TewzebWGiW4PZ8pbHfpvsMuriUPTKp3gybdq50EXYlg8ZBRVgCD5DBfebkvNr%2Fa6g%3D%3D&file-filters%5B%5D=.cs&hide-deleted-files=true#diff-0ba2e4842e187b0efcf6a6b5fd6fca73b546ece27e54074265eab734f826240dL45-R48

I was able to move the dependency from DafnyPipeline to DafnyDriver instead in #1534, which is at least an improvement.

[camrein]

Looks like I can't quite break the dependency entirely - trying to read the DafnySourceAttribute out of a dll built by Dafny using /useRuntimeLib forces the resolution of its dependencies, and without a dependency on DafnyRuntime.dll in the projects it fails to load.

That's unfortunate. How about, as an intermediate solution/mitigation, moving the Java runtime into its own project file? It's solely the Gradle command that fails. By creating a separate project one sees that something's missing for the build but can still generate the binaries for all other projects.