Resolution is differential-tested against cargo, but on the corpus: a crate list chosen for the mechanisms it breaks. That is the right shape for finding bugs and the wrong shape for claiming correctness, because the corpus is synthetic and its crates were picked by us.
What is missing
Pick real repositories, resolve each with cargo and with please_rust, and diff the resolved graphs: versions selected, features enabled per crate, which optional deps activated. A difference is either a bug here or a deliberate deviation, and both want recording.
Why it is different from what exists
scripts/differential.sh asks cargo whether a crate can be built at all, and is used to triage a failure. This asks whether we resolved the same graph, on code nobody here chose.
Where it lives
A separate corpus repo rather than here, since it needs to check out real projects.
How you would know
A set of real repositories whose resolution matches cargo's, with any deviation explained rather than merely observed. That is what would let the resolver claim correctness rather than the absence of known bugs.
Resolution is differential-tested against cargo, but on the corpus: a crate list chosen for the mechanisms it breaks. That is the right shape for finding bugs and the wrong shape for claiming correctness, because the corpus is synthetic and its crates were picked by us.
What is missing
Pick real repositories, resolve each with cargo and with
please_rust, and diff the resolved graphs: versions selected, features enabled per crate, which optional deps activated. A difference is either a bug here or a deliberate deviation, and both want recording.Why it is different from what exists
scripts/differential.shasks cargo whether a crate can be built at all, and is used to triage a failure. This asks whether we resolved the same graph, on code nobody here chose.Where it lives
A separate corpus repo rather than here, since it needs to check out real projects.
How you would know
A set of real repositories whose resolution matches cargo's, with any deviation explained rather than merely observed. That is what would let the resolver claim correctness rather than the absence of known bugs.