You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
The Dafny runtime libraries are used as dependencies for target language projects with Dafny-generated code. Because the version resolution of these dependencies are handled by target language tooling, we can't ensure that each such project can depend on the exact version of the runtime library matching the Dafny version it used to generate code. For example, if A and B are both Dafny generated libraries, and A depends on B, when B upgrades its dependency on the Dafny runtime to a new version but A hasn't yet, A will have to be able to run with a newer runtime version than it was built with.
It should not be hard for us to guarantee that code generated by one version of Dafny can use a newer version of the runtime within the same major version. This only means we have to make sure we don't change or delete entry points in the runtimes, and we generally haven't needed to do that. But we need to back up that claim with explicit mechanisms in our CI and/or release process.
This is in some ways a more specific version of #5349, but given the runtime libraries are a bit special, in that only Dafny-generated code is intended to refer to them, this may be worth addressing first before the more general problem of compatibility within and between Dafny and the target languages.
The text was updated successfully, but these errors were encountered:
The Dafny runtime libraries are used as dependencies for target language projects with Dafny-generated code. Because the version resolution of these dependencies are handled by target language tooling, we can't ensure that each such project can depend on the exact version of the runtime library matching the Dafny version it used to generate code. For example, if A and B are both Dafny generated libraries, and A depends on B, when B upgrades its dependency on the Dafny runtime to a new version but A hasn't yet, A will have to be able to run with a newer runtime version than it was built with.
It should not be hard for us to guarantee that code generated by one version of Dafny can use a newer version of the runtime within the same major version. This only means we have to make sure we don't change or delete entry points in the runtimes, and we generally haven't needed to do that. But we need to back up that claim with explicit mechanisms in our CI and/or release process.
This is in some ways a more specific version of #5349, but given the runtime libraries are a bit special, in that only Dafny-generated code is intended to refer to them, this may be worth addressing first before the more general problem of compatibility within and between Dafny and the target languages.
The text was updated successfully, but these errors were encountered: