Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Ensure Dafny runtime libraries are backwards compatible within major versions #5352

Open
robin-aws opened this issue Apr 23, 2024 · 0 comments

Comments

@robin-aws
Copy link
Member

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant