Fix workspace feature handling to filter features per-package#4545
Open
tautschnig wants to merge 2 commits intomodel-checking:mainfrom
Open
Fix workspace feature handling to filter features per-package#4545tautschnig wants to merge 2 commits intomodel-checking:mainfrom
tautschnig wants to merge 2 commits intomodel-checking:mainfrom
Conversation
The --features flag was being applied globally to all packages in a workspace, causing failures when packages don't all declare the same features. This change filters requested features for each package based on what that package actually defines in its features BTreeMap. Added regression test for --workspace --features with mixed features. Co-authored-by: Kiro autonomous agent Resolves: model-checking#4544
There was a problem hiding this comment.
Pull request overview
This PR fixes a bug where cargo kani --workspace --features <feature> would fail when workspace members don't all declare the requested features. The fix filters features per-package to match cargo's standard behavior, where features are only applied to packages that declare them.
Changes:
- Modified feature handling in
call_cargo.rsto filter features per-package instead of applying them globally - Added
filter_features_for_package()function to check which features each package declares - Added comprehensive regression test with a workspace containing packages with different feature sets
Reviewed changes
Copilot reviewed 9 out of 9 changed files in this pull request and generated no comments.
Show a summary per file
| File | Description |
|---|---|
| kani-driver/src/call_cargo.rs | Core fix: features are now filtered per-package and added to individual cargo commands instead of globally |
| tests/script-based-pre/workspace_features/workspace_features.sh | Test script verifying the fix works with various flag combinations |
| tests/script-based-pre/workspace_features/workspace_features.expected | Expected output for the test |
| tests/script-based-pre/workspace_features/mytests/src/lib.rs | Test crate with use_mylib feature defined |
| tests/script-based-pre/workspace_features/mytests/Cargo.toml | Test crate manifest defining the use_mylib feature |
| tests/script-based-pre/workspace_features/mylib/src/lib.rs | Test library with no features (to reproduce the issue) |
| tests/script-based-pre/workspace_features/mylib/Cargo.toml | Test library manifest with no features section |
| tests/script-based-pre/workspace_features/config.yml | Test configuration |
| tests/script-based-pre/workspace_features/Cargo.toml | Workspace manifest for the test |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
zhassan
reviewed
Feb 13, 2026
zhassan
approved these changes
Feb 13, 2026
zhassan
left a comment
There was a problem hiding this comment.
Looks good. Thanks for the quick fix!
Ensures feature propagation to packages and validates proof inclusion as requested by tautschnig.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
The --features flag was being applied globally to all packages in a workspace, causing failures when packages don't all declare the same features. This change filters requested features for each package based on what that package actually defines in its features BTreeMap.
Added regression test for --workspace --features with mixed features.
Co-authored-by: Kiro autonomous agent
Resolves #4544
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.