From 5a120df9440a64e41a38aadf8230a613784c880e Mon Sep 17 00:00:00 2001 From: Jack Royer Date: Tue, 28 Jul 2026 14:56:45 +0200 Subject: [PATCH] Centralize dependencies and package metadata in the workspace Each member declared its own versions and its own ../ path dependencies, so a shared dependency had to be edited in several manifests to stay consistent. Move them to [workspace.dependencies] and [workspace.package]; members now carry only what is specific to them. z3 is the case that motivated this: it is a normal dependency of smt-server and a dev-dependency of qfbvsmtrs, both on 0.20.0 with gh-release. Nothing tied the two together, and letting them drift would build and link two different z3 versions. Member crates keep their own `description` and their own feature additions on top of the shared entry, so smt-server still gets qfbvsmtrs with "wire" and rumba-core with "parse", and qfbvsmtrs still takes smt-wire as optional. crates/qfbvsmtrs/fuzz declares its own [workspace] and is therefore outside this one; its path dependency stays as it is, and it is still checked with --manifest-path as CI does. Pure refactor: Cargo.lock is byte-identical, and `cargo tree --workspace --all-features --edges all` is unchanged modulo path prefixes. --- Cargo.toml | 25 +++++++++++++++++++++++++ crates/qfbvsmtrs/Cargo.toml | 16 ++++++++-------- crates/smt-qfbv-smtlib/Cargo.toml | 10 +++++----- crates/smt-server/Cargo.toml | 24 ++++++++++++------------ crates/smt-wire/Cargo.toml | 6 +++--- 5 files changed, 53 insertions(+), 28 deletions(-) diff --git a/Cargo.toml b/Cargo.toml index 90b12dd..2fbdaf0 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -6,3 +6,28 @@ members = [ "crates/smt-qfbv-smtlib", ] resolver = "2" + +[workspace.package] +version = "0.1.0" +edition = "2021" +license = "MIT OR Apache-2.0" + +[workspace.dependencies] +# Workspace members. `crates/qfbvsmtrs/fuzz` declares its own `[workspace]` and so +# sits outside this one; it keeps a plain path dependency on qfbvsmtrs. +qfbvsmtrs = { path = "crates/qfbvsmtrs" } +smt-qfbv-smtlib = { path = "crates/smt-qfbv-smtlib" } +smt-wire = { path = "crates/smt-wire" } + +# External. z3 has to stay on a single version across the workspace: it is a +# normal dependency of smt-server and a dev-dependency of qfbvsmtrs, and the +# gh-release feature downloads a matching prebuilt solver for each. +binbit = { git = "https://github.com/bint-disasm/binbit", rev = "b4996145c06f39ce5bbc79a959975d7d20b6cf5e" } +blake3 = "1" +dashu = { version = "0.4.2", features = ["num-traits"] } +rumba-core = "1.0.0" +rusqlite = { version = "0.32", features = ["bundled"] } +splr = "0.17.2" +varisat = "0.2.2" +yaspar = "2.7.0" +z3 = { version = "0.20.0", features = ["gh-release"] } diff --git a/crates/qfbvsmtrs/Cargo.toml b/crates/qfbvsmtrs/Cargo.toml index 5729af9..6412a34 100644 --- a/crates/qfbvsmtrs/Cargo.toml +++ b/crates/qfbvsmtrs/Cargo.toml @@ -1,19 +1,19 @@ [package] name = "qfbvsmtrs" -version = "0.1.0" -edition = "2021" +version.workspace = true +edition.workspace = true description = "Standalone pure-Rust QF_BV SMT solver via bit-blasting" -license = "MIT OR Apache-2.0" +license.workspace = true [features] default = [] wire = ["dep:smt-wire"] [dependencies] -smt-qfbv-smtlib = { path = "../smt-qfbv-smtlib" } -smt-wire = { path = "../smt-wire", optional = true } -varisat = "0.2.2" -splr = "0.17.2" +smt-qfbv-smtlib.workspace = true +smt-wire = { workspace = true, optional = true } +varisat.workspace = true +splr.workspace = true [dev-dependencies] -z3 = { version = "0.20.0", features = ["gh-release"] } +z3.workspace = true diff --git a/crates/smt-qfbv-smtlib/Cargo.toml b/crates/smt-qfbv-smtlib/Cargo.toml index 0408438..c0e0550 100644 --- a/crates/smt-qfbv-smtlib/Cargo.toml +++ b/crates/smt-qfbv-smtlib/Cargo.toml @@ -1,10 +1,10 @@ [package] name = "smt-qfbv-smtlib" -version = "0.1.0" -edition = "2021" +version.workspace = true +edition.workspace = true description = "Shared sink-oriented QF_BV SMT-LIB frontend utilities" -license = "MIT OR Apache-2.0" +license.workspace = true [dependencies] -dashu = { version = "0.4.2", features = ["num-traits"] } -yaspar = "2.7.0" +dashu.workspace = true +yaspar.workspace = true diff --git a/crates/smt-server/Cargo.toml b/crates/smt-server/Cargo.toml index 6614cfb..ad9b377 100644 --- a/crates/smt-server/Cargo.toml +++ b/crates/smt-server/Cargo.toml @@ -1,19 +1,19 @@ [package] name = "smt-server" -version = "0.1.0" -edition = "2021" +version.workspace = true +edition.workspace = true description = "Reference SMT wire-format server and backends" -license = "MIT OR Apache-2.0" +license.workspace = true [dependencies] -binbit = { git = "https://github.com/bint-disasm/binbit", rev = "b4996145c06f39ce5bbc79a959975d7d20b6cf5e" } -qfbvsmtrs = { path = "../qfbvsmtrs", features = ["wire"] } -rumba-core = "1.0.0" -smt-qfbv-smtlib = { path = "../smt-qfbv-smtlib" } -smt-wire = { path = "../smt-wire" } -blake3 = "1" -rusqlite = { version = "0.32", features = ["bundled"] } -z3 = { version = "0.20.0", features = ["gh-release"] } +binbit.workspace = true +qfbvsmtrs = { workspace = true, features = ["wire"] } +rumba-core.workspace = true +smt-qfbv-smtlib.workspace = true +smt-wire.workspace = true +blake3.workspace = true +rusqlite.workspace = true +z3.workspace = true [dev-dependencies] -rumba-core = { version = "1.0.0", features = ["parse"] } +rumba-core = { workspace = true, features = ["parse"] } diff --git a/crates/smt-wire/Cargo.toml b/crates/smt-wire/Cargo.toml index a50be91..f9add4e 100644 --- a/crates/smt-wire/Cargo.toml +++ b/crates/smt-wire/Cargo.toml @@ -1,9 +1,9 @@ [package] name = "smt-wire" -version = "0.1.0" -edition = "2021" +version.workspace = true +edition.workspace = true description = "Rust codecs, views, validation, and builders for the SMT v1 wire format" -license = "MIT OR Apache-2.0" +license.workspace = true [lib] name = "smt_wire"