Document minimum requirements for compiled code in each language

[robin-aws]

Spin-off from #1951. For each target language, we should be very explicit about what minimum version of the language/runtime/etc. the compiled code needs, what third-party libraries are needed (e.g. the bignumber.js library), etc. We also need to back this up with CI to ensure we test on this minimal environment.

[davidcok]

Note that the CI process includes constructing a new working environment and running compilations in it for each language. This clearly needs maintenance as new languages are added. But it is a check on the dependencies.

[robin-aws]

Just to update, #2572 implements one approach that involves running the whole suite twice, once for the latest supported version of each language and once for the oldest supported version.

There are two issues with this:

1. Our CI resource constraints are already an issue, and even just doubling the nightly build cost could actually start to impact development further. Not to mention it is extremely wasteful to run tests that aren't even compiled twice for different compilation target runtimes (credit to @fabiomadge for pointing this out to me).
2. This approach only supports picking exactly two configurations, but .NET specifically needs at least two "oldest" configurations: netstandard2.0 and net472 IIRC.

I don't yet see a way to avoid significantly refactoring our test suite to address this.

[robin-aws]

With most compiled tests converted to use %testDafnyForEachCompiler now (#4115), I can see a clearer path forwards on this:

• We implement a way to only run the subset of integration tests that use that command, and restrict it to only run for a given target language.
• We split the integration tests into shards differently:
  • Define a "target-environment" GitHub actions matrix dimension
  • For each target language, add multiple target-environment values, trying to hit at least the oldest and newest supported versions (e.g. [java-8, java-17], [dotnet-netstandard2.0, dotnet-net452, dotnet-7.0], ...)
  • Execute the remaining tests (verification only, or NONUNIFORM compilation tests) on their own shard
• Individual shards could still be subdivided using XUNIT_SHARD and XUNIT_SHARD_COUNT as we do now, if they are disproportionately large

[texastony]

Is there any chance this can be prioritized?
For years, we have been asking for Dafny to advertise the details of the supported compiled languages:
i.e.: Dafny's compiled output uses features from JavaScript X, Java Y, Go Z, etc.

[atomb]

Is there any chance this can be prioritized? For years, we have been asking for Dafny to advertise the details of the supported compiled languages: i.e.: Dafny's compiled output uses features from JavaScript X, Java Y, Go Z, etc.

I'll start gathering some information on this. While I'm digging through it, I may start by leaving comments here with what I've found, so it'll be immediately available. Once we have a comprehensive set of details, we can consolidate them into a new document, and into CI checks that those documented dependencies are still correct.

[robin-aws]

CI checks that those documented dependencies are still correct.

See my comment above on this, and also note that #5081 will add support for a DAFNY_INTEGRATION_TESTS_ONLY_COMPILERS environment variable which helps us move towards that solution: https://github.com/dafny-lang/dafny/pull/5081/files#diff-1f04f8e2995d51289d432a867bd2393195de7abf5dcf8c62683870489a48c4d2R117

[atomb]

I'm sure various folks already know this information, but I don't think it's written down anywhere, so here's what I've uncovered so far for the widely-supported languages.

C#

• The runtime works with language versions at least as old as C# 7.3 (2018).
• The runtime works with target frameworks at least as old as netstandard2.0 (2017) and net452 (2014).
• Has no non-standard dependencies.

Go

• CI uses 1.15 (2020)
• Uses packages, not modules. Modules were introduced in 1.11.
• Suspect that this means it works with 1.10 (from 2018) because it was written when that, or a previous release, was current?

Java

• Uses lambdas, so 1.8 should be the minimum.
• Currently tested in CI with 1.8.
• Has no non-standard dependencies.

JavaScript

• Depends on bignumber.js, which is compatible with JavaScript 1.5 (ECMAScript 3).
  • Note that ECMAScript 2020 includes a BigInt type.
• Uses ... syntax, introduced in ECMAScript 2018 (9th Edition).
• I don't think it uses anything newer.

Python

• Generates import typing which was introduced in Python 3.5.
• Probably doesn't require anything newer?