Skip to content

Remove the need to build Kani with --workspace #1580

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Merged
tedinski merged 1 commit into from
Aug 24, 2022
Merged

Remove the need to build Kani with --workspace #1580

tedinski merged 1 commit into from
Aug 24, 2022

Conversation

@tedinski
Copy link
Contributor

@tedinski tedinski commented Aug 23, 2022

Description of changes:

  1. This depends on a feature?/bug fix? that will land in stable Rust in 1.64 (released in a month on Sept 22). It works for us now because we're pinned against a nightly Rust that now includes the patch.
  2. This might slightly reduce the over all "load" in CI, but I doubt it will decrease CI times by very much. The current critical path is macos-11 regression, and I believe that there we only save the build time of "bookrunner" and "make-kani-release" and nothing else. Hmm, maybe saving a "rebuild" of library/kani as well maybe.

Resolved issues:

Call-outs:

Testing:

  • How is this change tested? ci

  • Is this a refactor change? sorta

Checklist

  • Each commit message has a non-empty body, explaining why the change was made
  • Methods or procedures are documented
  • Regression or unit tests are included, or existing tests cover the modified code
  • My PR is restricted to a single feature or bugfix

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

@tedinski tedinski requested a review from a team as a code owner August 23, 2022 22:02
zhassan-aws
zhassan-aws reviewed Aug 23, 2022
View reviewed changes
docs/src/cheat-sheets.md

```bash
# Build all packages in the repository
cargo build --workspace
Copy link
Contributor

@zhassan-aws zhassan-aws Aug 23, 2022

Choose a reason for hiding this comment

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

Should this be kept with --workspace removed?

Copy link
Contributor Author

@tedinski tedinski Aug 24, 2022

Choose a reason for hiding this comment

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

I'm open to other ideas but IMO it was only ever in there in the first place to note that --workspace was needed.

@YoshikiTakashima
Copy link
Contributor

YoshikiTakashima commented Aug 23, 2022

If that feature lands, shall we also deprecate --workspace from cargo kani?

@zhassan-aws
Copy link
Contributor

zhassan-aws commented Aug 23, 2022

If that feature lands, shall we also deprecate --workspace from cargo kani?

I don't think we should, because users may still want to compile their entire workspace (and not just the default members) with Kani. Note that this PR is only concerned with how Kani itself is built, and not how it is used to compile packages.

@tedinski tedinski merged commit 8e746ac into model-checking:main Aug 24, 2022
@tedinski tedinski deleted the ci-tweaks-3 branch August 24, 2022 16:20
@github-actions github-actions bot mentioned this pull request May 27, 2025
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@zhassan-aws zhassan-aws zhassan-aws approved these changes

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@tedinski @YoshikiTakashima @zhassan-aws