-
-
Notifications
You must be signed in to change notification settings - Fork 14.4k
add flag for enabling global cache usage for proof trees and printing proof trees on error #113296
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
Changes from 3 commits
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
| Original file line number | Diff line number | Diff line change | ||||
|---|---|---|---|---|---|---|
|
|
@@ -418,6 +418,8 @@ mod desc { | |||||
| "a `,` separated combination of `bti`, `b-key`, `pac-ret`, or `leaf`"; | ||||||
| pub const parse_proc_macro_execution_strategy: &str = | ||||||
| "one of supported execution strategies (`same-thread`, or `cross-thread`)"; | ||||||
| pub const parse_solver_proof_tree_condition: &str = | ||||||
| "one of: `always`, `on-request`, `on-error`"; | ||||||
| } | ||||||
|
|
||||||
| mod parse { | ||||||
|
|
@@ -1238,6 +1240,19 @@ mod parse { | |||||
| }; | ||||||
| true | ||||||
| } | ||||||
|
|
||||||
| pub(crate) fn parse_solver_proof_tree_condition( | ||||||
BoxyUwU marked this conversation as resolved.
Outdated
Show resolved
Hide resolved
|
||||||
| slot: &mut SolverProofTreeCondition, | ||||||
| v: Option<&str>, | ||||||
| ) -> bool { | ||||||
| match v { | ||||||
| None | Some("always") => *slot = SolverProofTreeCondition::Always, | ||||||
| Some("on-request") => *slot = SolverProofTreeCondition::OnRequest, | ||||||
| Some("on-error") => *slot = SolverProofTreeCondition::OnError, | ||||||
| _ => return false, | ||||||
| }; | ||||||
| true | ||||||
| } | ||||||
| } | ||||||
|
|
||||||
| options! { | ||||||
|
|
@@ -1463,8 +1478,11 @@ options! { | |||||
| "output statistics about monomorphization collection"), | ||||||
| dump_mono_stats_format: DumpMonoStatsFormat = (DumpMonoStatsFormat::Markdown, parse_dump_mono_stats, [UNTRACKED], | ||||||
| "the format to use for -Z dump-mono-stats (`markdown` (default) or `json`)"), | ||||||
| dump_solver_proof_tree: bool = (false, parse_bool, [UNTRACKED], | ||||||
| "dump a proof tree for every goal evaluated by the new trait solver"), | ||||||
| dump_solver_proof_tree: SolverProofTreeCondition = (SolverProofTreeCondition::OnRequest, parse_solver_proof_tree_condition, [UNTRACKED], | ||||||
| "dump a proof tree for every goal evaluated by the new trait solver. If the flag is specified without any options after it | ||||||
| then it defaults to `always`. If the flag is not specified at all it defaults to `on-request`."), | ||||||
| dump_solver_proof_tree_use_cache: Option<bool> = (None, parse_opt_bool, [UNTRACKED], | ||||||
| "determines whether proof tree generation uses the global cache"), | ||||||
|
||||||
| "determines whether proof tree generation uses the global cache"), | |
| "determines whether dumping proof trees should disable the global cache"), |
this flag should not affect general proof tree generation, only the proof trees which should get dumped
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
that's.... not how the code works. the flag does cause us to use or not use the global cache during proof tree creation. It's not a step done when we dump the proof tree to edit all the "GLOBAL CACHE HIT" to actual proof trees. Implementing it that way sounds trickier than what was done in this PR
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
from the description:
This flag currently would affect misc uses of GenerateProofTree::Yes which will be added in the future for things like diagnostics logic and rustdoc's auto_trait file. We can fix this when we start using proof tree generation for those use cases if it's desirable.
When -Zdump-solver-proof-tree-use-cache=no/yes is set it acts on every call to evaluate_goal with GenerateProofTree::Yes and also to all proof trees generated by -Zdump-solver-proof-tree=always
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
my thought was that setting this to true does/will not prevent diagnostics and auto trait computation from disabling the cache, so this only affects trait solving when we construct a tree for "proof tree dumping"
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
ideally that's how it would work but right now it wouldn't if you implemented auto_trait/diagnostics by callign evalaute_goal with GenerateProofTree::Yes(UseGlobalCache::No).
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
yes, but that would completely ignore this compile flag
This file was deleted.
Uh oh!
There was an error while loading. Please reload this page.