Support fully-qualified `--package` arguments

[joshlf]

We use Kani in zerocopy, and pass --package zerocopy in CI. However, on our 0.7 branch, we are encountering this failure:

error: There are multiple `zerocopy` packages in your project, and the specification `zerocopy` is ambiguous.
Please re-run this command with one of the following specifications:
  path+file:///home/runner/work/zerocopy/zerocopy#0.7.35
  registry+https://github.com/rust-lang/crates.io-index#zerocopy@0.7.35
error: Failed to execute cargo (exit status: 101). Found 0 compilation errors.

This seems to be due to Kani having a transitive dependency on zerocopy 0.7. However, Kani does not support passing either suggested syntax as an argument to the --package flag. If Kani supported --package path+file:///home/runner/work/zerocopy/zerocopy#0.7.35, it would allow us to fix this failure.

[feliperodri]

Thank you for reporting this bug. We are trying to reproduce and investigate on our side.

[celinval]

Hi @joshlf, I was able to reproduce the issue by cloning the version of the PR above, and this is indeed an issue with how we are handling the package argument.

FYI, the ambiguity seems to be coming from the rand package that is one of your dev-dependencies:

$ cargo tree | head -n 15
zerocopy v0.7.35 (/tmp/zerocopy)
└── byteorder v1.5.0
[dev-dependencies]
├── assert_matches v1.5.0
├── elain v0.3.0
├── itertools v0.11.0
│   └── either v1.13.0
├── rand v0.8.5
│   ├── libc v0.2.159
│   ├── rand_chacha v0.3.1
│   │   ├── ppv-lite86 v0.2.20
│   │   │   └── zerocopy v0.7.35  <------------------- Here!!

Running cargo build fails with the same issue:

$ cargo build --package zerocopy --features __internal_use_only_features_that_work_on_stable
error: There are multiple `zerocopy` packages in your project, and the specification `zerocopy` is ambiguous.
Please re-run this command with one of the following specifications:
  path+file:///tmp/zerocopy#0.7.35
  registry+https://github.com/rust-lang/crates.io-index#zerocopy@0.7.35

[joshlf]

Ah yeah I suppose it's not actually Kani itself that has the zerocopy dep, but it's just that we need to be able to pass an unambiguous package spec via Kani.

Thanks for looking into this!