Skip to content

chore(deps): migrate z3 bundled feature to vendored #3558

Description

@purp

Description

z3 0.21 deprecates the bundled feature in favor of vendored. z3-sys
0.13's build script emits cargo:warning=The 'bundled' feature is deprecated. Please use the 'vendored' feature. on every build that enables it.

OpenShell wires the deprecated name through its own feature aliases:

  • crates/openshell-prover/Cargo.toml:14 — bundled-z3 = ["z3/bundled"]
  • crates/openshell-prover-cli/Cargo.toml:18, crates/openshell-server/Cargo.toml:123,
    crates/openshell-gateway/Cargo.toml:75 forward bundled-z3 onward

The work is to decide whether to repoint the bundled-z3 alias at
z3/vendored, and whether the public-facing alias name should change with it.

Context

Both features currently resolve to the same z3-sys code path, so nothing is
broken today and there is no user-visible behavior change. This is
forward-maintenance: the deprecated name will eventually be removed upstream.

This path is not incidental — it is the release build path. tasks/ci.toml:34
and tasks/scripts/stage-prebuilt-binaries.sh:172-173 force bundled-z3 for
the gateway, so tagged releases compile Z3 from vendored source through it.
That makes the change low-urgency but not zero-risk, which is why it was kept
out of the z3 0.21 upgrade (#3552) and its documentation follow-up.

bundled-z3 also appears in contributor-facing docs (README.md:362,
CONTRIBUTING.md:312-363) and in .agents/skills/build-openshell-mxc-windows/SKILL.md,
so a rename would need those updated in the same branch.

Not required for 0.1.0.

Definition of Done

  • A decision is recorded on whether to repoint bundled-z3 at z3/vendored
    and whether to rename the alias
  • If repointed, the gateway release build and the prover test suite are
    verified against the vendored path
  • Contributor docs and the Windows build skill match the resulting feature
    names
  • No deprecation warning is emitted for the Z3 source-build path

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

Labels

No labels
No labels

Type

No type

Projects

No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions