Skip to content

Conversation

@NlightNFotis
Copy link
Contributor

Update the release process ADR with information on the
Rust crate publishing, along with some information on its
versioning schema and choices.

  • Each commit message has a non-empty body, explaining why the change was made.
  • Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
  • The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
  • Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
  • My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • White-space or formatting changes outside the feature-related changed lines are in commits of their own.

@NlightNFotis NlightNFotis added documentation Rust API Issues pertaining to the CBCM Rust API labels Mar 30, 2023
@NlightNFotis NlightNFotis requested a review from jimgrundy as a code owner March 30, 2023 11:05
@NlightNFotis NlightNFotis self-assigned this Mar 30, 2023
Comment on lines +96 to +99
Most of the time, these two numbers will be the same - but there can be scenarios
where they can diverge: if the user for example uses a later version of the
Rust API (say, `5.80.0`) to link against a static library representing an older
version of CBMC (say `5.79.0`).
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Outside the scope of this PR, but should this be allowed or prevented? Are there times when this is safe and times when it could yield problematic outcomes?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The Rust API needs to link against libcprover.x.y.z.a to use the functions exposed by the C++ API.

If the C++ API functions haven't been subjected to an interface change for the existing functions, then this should be safe.

Of course, there cannot be too wide a divergence between versions of the Rust and C++ API it depends on.

In my personal experiments, I have linked the Rust API version 5.80.0 against libcprover.5.78.0.a and libcprover.5.79.0.a and everything worked fine. But of course, there's no guarantee that even a weekly release change is going to work.

I can try linking it against an even earlier version to see what happens, but based on behaviour I have observed before, if this is not possible, the most likely outcome is a linking error.

@NlightNFotis NlightNFotis merged commit 417d362 into diffblue:develop Mar 31, 2023
@NlightNFotis NlightNFotis deleted the document_rust_crate_release branch March 31, 2023 09:19
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

documentation Rust API Issues pertaining to the CBCM Rust API

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants