remove proof tree formatter, make em shallow

Author: lcnr

compiler/rustc_interface/src/tests.rs

@@ -799,10 +799,7 @@ fn test_unstable_options_tracking_hash() {
     tracked!(mir_opt_level, Some(4));
     tracked!(move_size_limit, Some(4096));
     tracked!(mutable_noalias, false);
-    tracked!(
-        next_solver,
-        Some(NextSolverConfig { coherence: true, globally: false, dump_tree: Default::default() })
-    );
+    tracked!(next_solver, Some(NextSolverConfig { coherence: true, globally: false }));
     tracked!(no_generate_arange_section, true);
     tracked!(no_jump_tables, true);
     tracked!(no_link, true);

compiler/rustc_middle/src/arena.rs

@@ -61,7 +61,10 @@ macro_rules! arena_types {
             [] dtorck_constraint: rustc_middle::traits::query::DropckConstraint<'tcx>,
             [] candidate_step: rustc_middle::traits::query::CandidateStep<'tcx>,
             [] autoderef_bad_ty: rustc_middle::traits::query::MethodAutoderefBadTy<'tcx>,
-            [] canonical_goal_evaluation: rustc_next_trait_solver::solve::inspect::GoalEvaluationStep<rustc_middle::ty::TyCtxt<'tcx>>,
+            [] canonical_goal_evaluation:
+                rustc_next_trait_solver::solve::inspect::CanonicalGoalEvaluationStep<
+                    rustc_middle::ty::TyCtxt<'tcx>
+                >,
             [] query_region_constraints: rustc_middle::infer::canonical::QueryRegionConstraints<'tcx>,
             [] type_op_subtype:
                 rustc_middle::infer::canonical::Canonical<'tcx,

compiler/rustc_middle/src/traits/solve/cache.rs

@@ -17,7 +17,7 @@ pub struct EvaluationCache<'tcx> {
 #[derive(Debug, PartialEq, Eq)]
 pub struct CacheData<'tcx> {
     pub result: QueryResult<'tcx>,
-    pub proof_tree: Option<&'tcx [inspect::GoalEvaluationStep<TyCtxt<'tcx>>]>,
+    pub proof_tree: Option<&'tcx inspect::CanonicalGoalEvaluationStep<TyCtxt<'tcx>>>,
     pub additional_depth: usize,
     pub encountered_overflow: bool,
 }
@@ -28,7 +28,7 @@ impl<'tcx> EvaluationCache<'tcx> {
         &self,
         tcx: TyCtxt<'tcx>,
         key: CanonicalInput<'tcx>,
-        proof_tree: Option<&'tcx [inspect::GoalEvaluationStep<TyCtxt<'tcx>>]>,
+        proof_tree: Option<&'tcx inspect::CanonicalGoalEvaluationStep<TyCtxt<'tcx>>>,
         additional_depth: usize,
         encountered_overflow: bool,
         cycle_participants: FxHashSet<CanonicalInput<'tcx>>,
@@ -107,7 +107,7 @@ struct Success<'tcx> {
 #[derive(Clone, Copy)]
 pub struct QueryData<'tcx> {
     pub result: QueryResult<'tcx>,
-    pub proof_tree: Option<&'tcx [inspect::GoalEvaluationStep<TyCtxt<'tcx>>]>,
+    pub proof_tree: Option<&'tcx inspect::CanonicalGoalEvaluationStep<TyCtxt<'tcx>>>,
 }
 
 /// The cache entry for a goal `CanonicalInput`.

compiler/rustc_middle/src/ty/context.rs

@@ -103,7 +103,8 @@ impl<'tcx> Interner for TyCtxt<'tcx> {
     type PredefinedOpaques = solve::PredefinedOpaques<'tcx>;
     type DefiningOpaqueTypes = &'tcx ty::List<LocalDefId>;
     type ExternalConstraints = ExternalConstraints<'tcx>;
-    type GoalEvaluationSteps = &'tcx [solve::inspect::GoalEvaluationStep<TyCtxt<'tcx>>];
+    type CanonicalGoalEvaluationStepRef =
+        &'tcx solve::inspect::CanonicalGoalEvaluationStep<TyCtxt<'tcx>>;
 
     type Ty = Ty<'tcx>;
     type Tys = &'tcx List<Ty<'tcx>>;

compiler/rustc_session/src/config.rs

@@ -796,16 +796,6 @@ pub struct NextSolverConfig {
     /// Whether the new trait solver should be enabled everywhere.
     /// This is only `true` if `coherence` is also enabled.
     pub globally: bool,
-    /// Whether to dump proof trees after computing a proof tree.
-    pub dump_tree: DumpSolverProofTree,
-}
-
-#[derive(Default, Debug, Copy, Clone, Hash, PartialEq, Eq)]
-pub enum DumpSolverProofTree {
-    Always,
-    OnError,
-    #[default]
-    Never,
 }
 
 #[derive(Clone)]

compiler/rustc_session/src/options.rs

@@ -399,7 +399,8 @@ mod desc {
     pub const parse_instrument_xray: &str = "either a boolean (`yes`, `no`, `on`, `off`, etc), or a comma separated list of settings: `always` or `never` (mutually exclusive), `ignore-loops`, `instruction-threshold=N`, `skip-entry`, `skip-exit`";
     pub const parse_unpretty: &str = "`string` or `string=string`";
     pub const parse_treat_err_as_bug: &str = "either no value or a non-negative number";
-    pub const parse_next_solver_config: &str = "a comma separated list of solver configurations: `globally` (default), `coherence`, `dump-tree`, `dump-tree-on-error";
+    pub const parse_next_solver_config: &str =
+        "a comma separated list of solver configurations: `globally` (default), and `coherence`";
     pub const parse_lto: &str =
         "either a boolean (`yes`, `no`, `on`, `off`, etc), `thin`, `fat`, or omitted";
     pub const parse_linker_plugin_lto: &str =
@@ -1058,39 +1059,20 @@ mod parse {
         if let Some(config) = v {
             let mut coherence = false;
             let mut globally = true;
-            let mut dump_tree = None;
             for c in config.split(',') {
                 match c {
                     "globally" => globally = true,
                     "coherence" => {
                         globally = false;
                         coherence = true;
                     }
-                    "dump-tree" => {
-                        if dump_tree.replace(DumpSolverProofTree::Always).is_some() {
-                            return false;
-                        }
-                    }
-                    "dump-tree-on-error" => {
-                        if dump_tree.replace(DumpSolverProofTree::OnError).is_some() {
-                            return false;
-                        }
-                    }
                     _ => return false,
                 }
             }
 
-            *slot = Some(NextSolverConfig {
-                coherence: coherence || globally,
-                globally,
-                dump_tree: dump_tree.unwrap_or_default(),
-            });
+            *slot = Some(NextSolverConfig { coherence: coherence || globally, globally });
         } else {
-            *slot = Some(NextSolverConfig {
-                coherence: true,
-                globally: true,
-                dump_tree: Default::default(),
-            });
+            *slot = Some(NextSolverConfig { coherence: true, globally: true });
         }
 
         true

compiler/rustc_trait_selection/src/solve/eval_ctxt/mod.rs

@@ -1,6 +1,3 @@
-use std::io::Write;
-use std::ops::ControlFlow;
-
 use rustc_data_structures::stack::ensure_sufficient_stack;
 use rustc_hir::def_id::DefId;
 use rustc_infer::infer::at::ToTrace;
@@ -20,10 +17,10 @@ use rustc_middle::ty::{
     self, InferCtxtLike, OpaqueTypeKey, Ty, TyCtxt, TypeFoldable, TypeSuperVisitable,
     TypeVisitable, TypeVisitableExt, TypeVisitor,
 };
-use rustc_session::config::DumpSolverProofTree;
 use rustc_span::DUMMY_SP;
 use rustc_type_ir::{self as ir, CanonicalVarValues, Interner};
 use rustc_type_ir_macros::{Lift_Generic, TypeFoldable_Generic, TypeVisitable_Generic};
+use std::ops::ControlFlow;
 
 use crate::traits::coherence;
 use crate::traits::vtable::{count_own_vtable_entries, prepare_vtable_segments, VtblSegment};
@@ -135,8 +132,7 @@ impl<I: Interner> NestedGoals<I> {
 #[derive(PartialEq, Eq, Debug, Hash, HashStable, Clone, Copy)]
 pub enum GenerateProofTree {
     Yes,
-    IfEnabled,
-    Never,
+    No,
 }
 
 #[extension(pub trait InferCtxtEvalExt<'tcx>)]
@@ -182,7 +178,7 @@ impl<'a, 'tcx> EvalCtxt<'a, InferCtxt<'tcx>> {
             infcx,
             search_graph: &mut search_graph,
             nested_goals: NestedGoals::new(),
-            inspect: ProofTreeBuilder::new_maybe_root(infcx.tcx, generate_proof_tree),
+            inspect: ProofTreeBuilder::new_maybe_root(generate_proof_tree),
 
             // Only relevant when canonicalizing the response,
             // which we don't do within this evaluation context.
@@ -197,23 +193,14 @@ impl<'a, 'tcx> EvalCtxt<'a, InferCtxt<'tcx>> {
         };
         let result = f(&mut ecx);
 
-        let tree = ecx.inspect.finalize();
-        if let (Some(tree), DumpSolverProofTree::Always) = (
-            &tree,
-            infcx.tcx.sess.opts.unstable_opts.next_solver.map(|c| c.dump_tree).unwrap_or_default(),
-        ) {
-            let mut lock = std::io::stdout().lock();
-            let _ = lock.write_fmt(format_args!("{tree:?}\n"));
-            let _ = lock.flush();
-        }
-
+        let proof_tree = ecx.inspect.finalize();
         assert!(
             ecx.nested_goals.is_empty(),
             "root `EvalCtxt` should not have any goals added to it"
         );
 
         assert!(search_graph.is_empty());
-        (result, tree)
+        (result, proof_tree)
     }
 
     /// Creates a nested evaluation context that shares the same search graph as the
@@ -483,7 +470,6 @@ impl<'a, 'tcx> EvalCtxt<'a, InferCtxt<'tcx>> {
     // the certainty of all the goals.
     #[instrument(level = "trace", skip(self))]
     pub(super) fn try_evaluate_added_goals(&mut self) -> Result<Certainty, NoSolution> {
-        self.inspect.start_evaluate_added_goals();
         let mut response = Ok(Certainty::overflow(false));
         for _ in 0..FIXPOINT_STEP_LIMIT {
             // FIXME: This match is a bit ugly, it might be nice to change the inspect
@@ -501,8 +487,6 @@ impl<'a, 'tcx> EvalCtxt<'a, InferCtxt<'tcx>> {
             }
         }
 
-        self.inspect.evaluate_added_goals_result(response);
-
         if response.is_err() {
             self.tainted = Err(NoSolution);
         }
@@ -515,7 +499,6 @@ impl<'a, 'tcx> EvalCtxt<'a, InferCtxt<'tcx>> {
     /// Goals for the next step get directly added to the nested goals of the `EvalCtxt`.
     fn evaluate_added_goals_step(&mut self) -> Result<Option<Certainty>, NoSolution> {
         let tcx = self.tcx();
-        self.inspect.start_evaluate_added_goals_step();
         let mut goals = core::mem::take(&mut self.nested_goals);
 
         // If this loop did not result in any progress, what's our final certainty.

compiler/rustc_trait_selection/src/solve/fulfill.rs

@@ -79,7 +79,7 @@ impl<'tcx> ObligationStorage<'tcx> {
             // change.
             self.overflowed.extend(self.pending.extract_if(|o| {
                 let goal = o.clone().into();
-                let result = infcx.evaluate_root_goal(goal, GenerateProofTree::Never).0;
+                let result = infcx.evaluate_root_goal(goal, GenerateProofTree::No).0;
                 match result {
                     Ok((has_changed, _)) => has_changed,
                     _ => false,
@@ -159,7 +159,7 @@ impl<'tcx> TraitEngine<'tcx> for FulfillmentCtxt<'tcx> {
             let mut has_changed = false;
             for obligation in self.obligations.unstalled_for_select() {
                 let goal = obligation.clone().into();
-                let result = infcx.evaluate_root_goal(goal, GenerateProofTree::IfEnabled).0;
+                let result = infcx.evaluate_root_goal(goal, GenerateProofTree::No).0;
                 self.inspect_evaluated_obligation(infcx, &obligation, &result);
                 let (changed, certainty) = match result {
                     Ok(result) => result,
@@ -246,7 +246,7 @@ fn fulfillment_error_for_stalled<'tcx>(
     root_obligation: PredicateObligation<'tcx>,
 ) -> FulfillmentError<'tcx> {
     let (code, refine_obligation) = infcx.probe(|_| {
-        match infcx.evaluate_root_goal(root_obligation.clone().into(), GenerateProofTree::Never).0 {
+        match infcx.evaluate_root_goal(root_obligation.clone().into(), GenerateProofTree::No).0 {
             Ok((_, Certainty::Maybe(MaybeCause::Ambiguity))) => {
                 (FulfillmentErrorCode::Ambiguity { overflow: None }, true)
             }

compiler/rustc_trait_selection/src/solve/inspect/analyse.rs

@@ -317,7 +317,6 @@ impl<'a, 'tcx> InspectGoal<'a, 'tcx> {
                 inspect::ProbeStep::RecordImplArgs { impl_args: i } => {
                     assert_eq!(impl_args.replace(i), None);
                 }
-                inspect::ProbeStep::EvaluateGoals(_) => (),
             }
         }
 
@@ -359,13 +358,7 @@ impl<'a, 'tcx> InspectGoal<'a, 'tcx> {
                 warn!("unexpected root evaluation: {:?}", self.evaluation_kind);
                 return vec![];
             }
-            inspect::CanonicalGoalEvaluationKind::Evaluation { revisions } => {
-                if let Some(last) = revisions.last() {
-                    last
-                } else {
-                    return vec![];
-                }
-            }
+            inspect::CanonicalGoalEvaluationKind::Evaluation { final_revision } => final_revision,
         };
 
         let mut nested_goals = vec![];
@@ -392,9 +385,7 @@ impl<'a, 'tcx> InspectGoal<'a, 'tcx> {
         normalizes_to_term_hack: Option<NormalizesToTermHack<'tcx>>,
         source: GoalSource,
     ) -> Self {
-        let inspect::GoalEvaluation { uncanonicalized_goal, kind, evaluation } = root;
-        let inspect::GoalEvaluationKind::Root { orig_values } = kind else { unreachable!() };
-
+        let inspect::GoalEvaluation { uncanonicalized_goal, orig_values, evaluation } = root;
         let result = evaluation.result.and_then(|ok| {
             if let Some(term_hack) = normalizes_to_term_hack {
                 infcx