Skip to content

Conversation

@tedinski
Copy link
Contributor

@tedinski tedinski commented Mar 8, 2022

Description of changes:

While bumbling around trying to find the name of "this crate" I basically implemented this, so I've cleaned this up to submit separately from anything else.

Resolved issues:

Resolves #717

Call-outs:

Contains a few extra cleanups and comments unrelated to headline feature.

Testing:

  • How is this change tested? existing suite. Notably not really feasible to add to our cargo-kani test suite since the way all those invocations work specifies the working directory. But it does work now to e.g. call cargo-kani from src

  • Is this a refactor change? basically yes

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 March 8, 2022 23:11
/// `cargo locate-project` produces a response like:
/// `{"root":"/full/path/to/src/cargo-kani/Cargo.toml"}`
fn cargo_locate_project() -> Result<PathBuf> {
let cmd = Command::new("cargo").arg("locate-project").output()?;
Copy link
Contributor

Choose a reason for hiding this comment

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

One option is to run cargo locate-project with --message-format plain to avoid parsing json.

$ pwd
/home/ubuntu/git/kani/tests/cargo-kani/config/src
$ cargo locate-project
{"root":"/home/ubuntu/git/kani/tests/cargo-kani/config/Cargo.toml"}
$ cargo locate-project --message-format plain
/home/ubuntu/git/kani/tests/cargo-kani/config/Cargo.toml

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Done, though while debugging why everything suddenly failed (there is a newline in the bytes, oh), I realized I should update a bit of the error handling here too.

Copy link
Contributor

Choose a reason for hiding this comment

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

Ouch!

@tedinski tedinski merged commit 6dc0eb3 into model-checking:main Mar 9, 2022
@tedinski tedinski deleted the locate-project branch March 9, 2022 16:58
tedinski added a commit to tedinski/rmc that referenced this pull request Apr 26, 2022
* use message-format plain, update error handling
tedinski added a commit that referenced this pull request Apr 27, 2022
* use message-format plain, update error handling
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Cargo-rmc cannot locate workspace Cargo.toml

2 participants