Skip to content
Merged
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
39 changes: 37 additions & 2 deletions doc/ADR/release_process.md
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
\page release-process Release Process

**Date**: 2020-10-08
**Updated**: 2022-06-23
**Updated**: 2023-03-29
**Author**: Fotis Koutoulakis, fotis.koutoulakis@diffblue.com
**Domain**: Release & Packaging

Expand All @@ -10,7 +10,11 @@
The current process we follow through to make a new release is the following:

1. At the point in time we want to make the release, we make a change to
`src/config.inc`, and update the configuration variable `CBMC_VERSION`.
two files: `src/config.inc`, wherein we update the configuration variable
`CBMC_VERSION`, and `src/libcprover-rust/Cargo.toml`, wherein we update
the `version` variable to be the same as `CBMC_VERSION` (e.g. set both
to `5.80.0`).

This is important as it informs the various tools of the current version
of CBMC.

Expand All @@ -22,6 +26,19 @@ The current process we follow through to make a new release is the following:
denoting the minor version, and `z` identifying the patch version (useful
for a hotfix or patch.)

3. Pushing the Rust crate, which is documented [here](https://doc.rust-lang.org/cargo/commands/cargo-publish.html)
but effectively entails logging in with an API token generated from
https://crates.io with `cargo login`, and then issuing `cargo publish`.

The usual environment variables are required (part of the `publish`
step is that the crate can be built) - these are documented in the
`readme.md` file at the root of the `src/libcprover-rust/` directory,
and online at [libcprover_rust](https://crates.io/crates/libcprover_rust).

For the crate to be pushed successfully, the user performing the `cargo
publish` step needs to be a member of the [diffblue/diffblue-opensource](https://github.com/orgs/diffblue/teams/diffblue-opensource)
team.

At this point, the rest of the process is automated, so we don't need to do
anything more, but the process is described below for reference:

Expand Down Expand Up @@ -63,6 +80,24 @@ detectable change including bugfixes can do that. Instead, major version
increments should signal that we expect many users will have to review their
workflows for potential breakages, not just any.

### Rust API versioning

Following discussions during the development of `libcprover_rust`, it was decided
that it would be easiest if the Rust API version was following the same scheme
that CBMC does, so that it's clear which version of the Rust API corresponds to
which version of CBMC.

This means that the Rust API has two "versions" it can report.

1. The library version, as reported in `Cargo.toml`, and
2. The (C++) API version, which is coming from CBMC and aligns with the version
number in `config.inc` (reported via the `get_api_version()` API call).

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`).
Comment on lines +96 to +99
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.


## Constraints

Initial design of the release process suggested that the release cadence
Expand Down