-
Notifications
You must be signed in to change notification settings - Fork 13.3k
new solver proof tree generation #112351
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.
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
new solver proof tree generation #112351
Conversation
858ba62
to
71244d7
Compare
This comment has been minimized.
This comment has been minimized.
625c2ee
to
2ce5c7e
Compare
This comment has been minimized.
This comment has been minimized.
Some changes occurred to the core trait solver cc @rust-lang/initiative-trait-system-refactor |
4c2cc0e
to
40353ab
Compare
☔ The latest upstream changes (presumably #112716) made this pull request unmergeable. Please resolve the merge conflicts. |
have a bunch of nits but given that none of them change the general structure here, r=me after fixing the merge conflicts. |
40353ab
to
3a6ce74
Compare
this pretty much conflicts with everything which touches the trait solver, even just by renaming some shared types or whatever, so @bors r+ rollup=never |
☀️ Test successful - checks-actions |
Finished benchmarking commit (18a6d91): comparison URL. Overall result: ✅ improvements - no action needed@rustbot label: -perf-regression Instruction countThis is a highly reliable metric that was used to determine the overall result at the top of this comment.
Max RSS (memory usage)This benchmark run did not return any relevant results for this metric. CyclesResultsThis is a less reliable metric that may be of interest but was not used to determine the overall result at the top of this comment.
Binary sizeThis benchmark run did not return any relevant results for this metric. Bootstrap: 657.557s -> 658.179s (0.09%) |
Adds a new
-Z
flag-Zdump-solver-proof-tree
which causes us to generate proof trees for each call toinfcx.evaluate_root_goal
. Currently these just getdebug!
'd out rather than put in a file.Callers of
infcx.evaluate_root_goal
get the proof tree returned to them and can force one to be generated by passing inGenerateProofTree::Yes
. Currently we do not disable the global cache or do anything about the provisional cache when generating proof trees is enabled, this is optimal for debugging but not so much for diagnostics.Personally I think the exact formatting of proof trees here is not ideal but it's easy to change after this PR lands and would like to avoid bikeshedding the exact way we output this before we even have any of the logic merged to get all the information out of the solver.
This PR is best reviewed with whitespace changes hidden, there is also probably no point going commit by commit
r? @lcnr
Below is the proof tree output for the
AliasRelate(TAIT, sub, Alias)
case in rust-lang/trait-system-refactor-initiative#25 from the following command:RUSTC_LOG="rustc_trait_selection::solve::inspect::dump=debug" RUSTFLAGS="-Ztrait-solver=next -Zverbose -Zdump-solver-proof-tree" cargo +stage1 check
Proof tree