From 2260b8302b6635c448fa23e61bb963075e221040 Mon Sep 17 00:00:00 2001 From: gavinleroy Date: Wed, 17 Jul 2024 16:32:43 -0600 Subject: [PATCH 1/3] Remove subgoals implied by prior errors, filter all errors in a type-checking body --- Cargo.lock | 8 +- crates/argus-cli/Cargo.toml | 6 +- crates/argus-ext/Cargo.toml | 2 +- crates/argus-ext/src/ty.rs | 88 ++++++++---- crates/argus-ser/Cargo.toml | 4 +- crates/argus/Cargo.toml | 8 +- crates/argus/src/aadebug/mod.rs | 2 +- crates/argus/src/aadebug/tree.rs | 1 - crates/argus/src/analysis/entry.rs | 15 ++- crates/argus/src/analysis/transform.rs | 4 +- crates/argus/src/proof_tree/serialize.rs | 162 ++++++++++++++++------- ide/packages/extension/package.json | 2 +- 12 files changed, 206 insertions(+), 96 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index fac328f..0a807f9 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -25,7 +25,7 @@ checksum = "080e9890a082662b09c1ad45f567faeeb47f22b5fb23895fbe1e651e718e25ca" [[package]] name = "argus-cli" -version = "0.1.9" +version = "0.1.10" dependencies = [ "anyhow", "argus-ext", @@ -42,7 +42,7 @@ dependencies = [ [[package]] name = "argus-ext" -version = "0.1.9" +version = "0.1.10" dependencies = [ "anyhow", "fluid-let", @@ -55,7 +55,7 @@ dependencies = [ [[package]] name = "argus-lib" -version = "0.1.9" +version = "0.1.10" dependencies = [ "anyhow", "argus-ext", @@ -80,7 +80,7 @@ dependencies = [ [[package]] name = "argus-ser" -version = "0.1.9" +version = "0.1.10" dependencies = [ "anyhow", "argus-ext", diff --git a/crates/argus-cli/Cargo.toml b/crates/argus-cli/Cargo.toml index f7a7eec..cfb3aa5 100644 --- a/crates/argus-cli/Cargo.toml +++ b/crates/argus-cli/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "argus-cli" -version = "0.1.9" +version = "0.1.10" edition = "2021" authors = ["Gavin Gray "] repository = "https://github.com/cognitive-engineering-lab/argus" @@ -10,8 +10,8 @@ license = "MIT" # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html [dependencies] -argus-lib = { version = "0.1.9", path = "../argus" } -argus-ext = { version = "0.1.9", path = "../argus-ext" } +argus-lib = { version = "0.1.10", path = "../argus" } +argus-ext = { version = "0.1.10", path = "../argus-ext" } rustc_plugin = "=0.10.0-nightly-2024-05-20" rustc_utils.workspace = true diff --git a/crates/argus-ext/Cargo.toml b/crates/argus-ext/Cargo.toml index e1c086f..7756672 100644 --- a/crates/argus-ext/Cargo.toml +++ b/crates/argus-ext/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "argus-ext" -version = "0.1.9" +version = "0.1.10" edition = "2021" authors = ["Gavin Gray "] repository = "https://github.com/cognitive-engineering-lab/argus" diff --git a/crates/argus-ext/src/ty.rs b/crates/argus-ext/src/ty.rs index f342f9b..ea12461 100644 --- a/crates/argus-ext/src/ty.rs +++ b/crates/argus-ext/src/ty.rs @@ -8,6 +8,7 @@ use rustc_middle::ty::{self, Predicate, TyCtxt, TypeVisitable, TypeckResults}; use rustc_span::{FileName, Span}; use rustc_trait_selection::solve::inspect::InspectCandidate; use rustc_utils::source_map::range::CharRange; +use smallvec::SmallVec; use crate::EvaluationResult; @@ -101,6 +102,56 @@ pub trait VarCounterExt<'tcx>: TypeVisitable> { fn count_vars(self, tcx: TyCtxt<'tcx>) -> usize; } +fn make_failing_bound_implicationp<'a, 'tcx, T>( + items: &'a [(usize, &T)], + get_predicate: impl Fn(&T) -> Predicate<'tcx> + 'a, + get_tcx: impl Fn(&T) -> TyCtxt<'tcx> + 'a, +) -> impl Fn((usize, &T)) -> bool + 'a { + move |(i, other): (usize, &T)| { + items.iter().any(|&(j, bound)| { + let poly_tp = get_predicate(bound).expect_trait_predicate(); + if i != j // Don't consider reflexive implication + && let ty::TraitPredicate { + trait_ref, + polarity: ty::PredicatePolarity::Positive, + } = poly_tp.skip_binder() + { + get_tcx(other).does_trait_ref_occur_in( + poly_tp.rebind(trait_ref), + get_predicate(other), + ) + } else { + false + } + }) + } +} + +/// If possible, use `retain_error_sources` which sorts and filters in place. +pub fn identify_error_sources<'tcx, T>( + all_items: &[T], + get_result: impl Fn(&T) -> EvaluationResult, + get_predicate: impl Fn(&T) -> Predicate<'tcx>, + get_tcx: impl Fn(&T) -> TyCtxt<'tcx>, +) -> impl Iterator + '_ { + let (trait_preds, _): (Vec<(usize, &T)>, _) = + all_items.iter().enumerate().partition(|(_, t)| { + !get_result(t).is_yes() && get_predicate(t).is_trait_predicate() + }); + + let is_implied_by_failing_bound = + make_failing_bound_implicationp(&trait_preds, get_predicate, get_tcx); + + let mut to_keep = SmallVec::<[_; 8]>::default(); + for t in all_items.iter().enumerate() { + if !is_implied_by_failing_bound(t) { + to_keep.push(t.0); + } + } + + to_keep.into_iter() +} + /// Select only the items that are not implied by another failing bound. /// /// ## Example: @@ -116,7 +167,6 @@ pub fn retain_error_sources<'tcx, T>( get_result: impl Fn(&T) -> EvaluationResult, get_predicate: impl Fn(&T) -> Predicate<'tcx>, get_tcx: impl Fn(&T) -> TyCtxt<'tcx>, - eq: impl Fn(&T, &T) -> bool, ) { if all_items.is_empty() { return; @@ -127,34 +177,25 @@ pub fn retain_error_sources<'tcx, T>( }); let (trait_preds, _) = all_items.split_at(idx); + let trait_preds_enumerated = + trait_preds.iter().enumerate().collect::>(); - let is_implied_by_failing_bound = |other: &T| { - trait_preds.iter().any(|bound| { - let poly_tp = get_predicate(bound).expect_trait_predicate(); - if let ty::TraitPredicate { - trait_ref, - polarity: ty::PredicatePolarity::Positive, - } = poly_tp.skip_binder() - // Don't consider reflexive implication - && !eq(bound, other) - { - get_tcx(other).does_trait_ref_occur_in( - poly_tp.rebind(trait_ref), - get_predicate(other), - ) - } else { - false - } - }) - }; + let is_implied_by_failing_bound = make_failing_bound_implicationp( + &trait_preds_enumerated, + get_predicate, + get_tcx, + ); let to_remove = &mut vec![]; - for (i, here) in all_items.iter().enumerate() { - if is_implied_by_failing_bound(here) { - to_remove.push(i); + for t in all_items.iter().enumerate() { + if is_implied_by_failing_bound(t) { + to_remove.push(t.0); } } + drop(is_implied_by_failing_bound); + drop(trait_preds_enumerated); + for i in to_remove.iter().rev() { all_items.remove(*i); } @@ -165,7 +206,6 @@ pub fn retain_method_calls<'tcx, T>( _get_result: impl Fn(&T) -> EvaluationResult, get_predicate: impl Fn(&T) -> Predicate<'tcx>, get_tcx: impl Fn(&T) -> TyCtxt<'tcx>, - _eq: impl Fn(&T, &T) -> bool, ) { if all_items.is_empty() { return; diff --git a/crates/argus-ser/Cargo.toml b/crates/argus-ser/Cargo.toml index c7540c7..e020c35 100644 --- a/crates/argus-ser/Cargo.toml +++ b/crates/argus-ser/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "argus-ser" -version = "0.1.9" +version = "0.1.10" edition = "2021" authors = ["Gavin Gray "] repository = "https://github.com/cognitive-engineering-lab/argus" @@ -28,7 +28,7 @@ smallvec = "1.11.2" itertools = "0.12.0" ts-rs = { version = "7.1.1", features = ["indexmap-impl"], optional = true } index_vec = { version = "0.1.3", features = ["serde"] } -argus-ext = { version = "0.1.9", path = "../argus-ext" } +argus-ext = { version = "0.1.10", path = "../argus-ext" } [dev-dependencies] argus-ser = { path = ".", features = ["testing"] } diff --git a/crates/argus/Cargo.toml b/crates/argus/Cargo.toml index b59d42a..df76500 100644 --- a/crates/argus/Cargo.toml +++ b/crates/argus/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "argus-lib" -version = "0.1.9" +version = "0.1.10" edition = "2021" authors = ["Gavin Gray "] repository = "https://github.com/cognitive-engineering-lab/argus" @@ -21,8 +21,8 @@ fluid-let.workspace = true serde.workspace = true serde_json.workspace = true -argus-ext = { version = "0.1.9", path = "../argus-ext" } -argus-ser = { version = "0.1.9", path = "../argus-ser" } +argus-ext = { version = "0.1.10", path = "../argus-ext" } +argus-ser = { version = "0.1.10", path = "../argus-ser" } index_vec = { version = "0.1.3", features = ["serde"] } smallvec = "1.11.2" itertools = "0.12.0" @@ -35,7 +35,7 @@ ts-rs = { version = "7.1.1", features = ["indexmap-impl"], optional = true } [dev-dependencies] argus-lib = { path = ".", features = ["testing"] } -argus-ser = { version = "0.1.9", path = "../argus-ser", features = ["testing"] } +argus-ser = { version = "0.1.10", path = "../argus-ser", features = ["testing"] } rustc_utils = { version = "=0.10.0-nightly-2024-05-20", features = ["serde", "ts-rs"] } test-log = "0.2.11" env_logger = "0.9.3" diff --git a/crates/argus/src/aadebug/mod.rs b/crates/argus/src/aadebug/mod.rs index 7270b64..c167cf8 100644 --- a/crates/argus/src/aadebug/mod.rs +++ b/crates/argus/src/aadebug/mod.rs @@ -1,5 +1,5 @@ mod dnf; -mod tree; +pub(crate) mod tree; mod ty; use std::time::Instant; diff --git a/crates/argus/src/aadebug/tree.rs b/crates/argus/src/aadebug/tree.rs index b116b09..7914d58 100644 --- a/crates/argus/src/aadebug/tree.rs +++ b/crates/argus/src/aadebug/tree.rs @@ -297,7 +297,6 @@ impl<'a, 'tcx> Candidate<'a, 'tcx> { |g| g.result, |g| g.goal.predicate, |g| g.infcx.tcx, - |a, b| a.idx == b.idx, ); all_goals.into_iter() diff --git a/crates/argus/src/analysis/entry.rs b/crates/argus/src/analysis/entry.rs index 63de739..5ce7504 100644 --- a/crates/argus/src/analysis/entry.rs +++ b/crates/argus/src/analysis/entry.rs @@ -204,11 +204,22 @@ pub(in crate::analysis) fn build_obligations_in_body<'tcx>( body_id: BodyId, typeck_results: &'tcx TypeckResults<'tcx>, ) -> (Forgettable>, ObligationsInBody) { - let obligations = tls::take_obligations(); + let mut obligations = tls::take_obligations(); let obligation_data = tls::unsafe_take_data(); - let obligation_data = FullData::new(obligation_data); + // XXX: it's possible that Argus reports false negatives. Meaning that + // in a body that type checks, failing obligations are reported. + // This happens as a result of how predicates are extracted from rustc (ask gavin) + // so as a first heuristic, if the body isn't tainted by errors, we'll just remove + // all non-successful obligations. + if typeck_results.tainted_by_errors.is_none() { + log::info!("BODY HAS NO ERRORS"); + obligations.retain(|prov| prov.it.result.is_yes()); + } else { + log::info!("BODY TAINTED! {:?}", typeck_results.hir_owner); + } + let ctx = ErrorAssemblyCtx { tcx, body_id, diff --git a/crates/argus/src/analysis/transform.rs b/crates/argus/src/analysis/transform.rs index f51c4e3..b85d60d 100644 --- a/crates/argus/src/analysis/transform.rs +++ b/crates/argus/src/analysis/transform.rs @@ -232,14 +232,13 @@ impl<'a, 'tcx: 'a> ObligationsBuilder<'a, 'tcx> { // Filter down the set of obligations as much as possible. // // 1. Remove obligations that shouldn't have been checked. (I.e., a failed - // precondition dissalows it from succeeding.) Hopefully, in the future these + // precondition dissallows it from succeeding.) Hopefully, in the future these // aren't even solved for. retain_error_sources( &mut obligations, |&i| gfdata(i).result, |&i| gfdata(i).obligation.predicate, |_| self.tcx, - |&a, &b| a == b, ); retain_method_calls( @@ -247,7 +246,6 @@ impl<'a, 'tcx: 'a> ObligationsBuilder<'a, 'tcx> { |&i| gfdata(i).result, |&i| gfdata(i).obligation.predicate, |_| self.tcx, - |&a, &b| a == b, ); let obligations = obligations diff --git a/crates/argus/src/proof_tree/serialize.rs b/crates/argus/src/proof_tree/serialize.rs index 75c4ccf..1d3f74e 100644 --- a/crates/argus/src/proof_tree/serialize.rs +++ b/crates/argus/src/proof_tree/serialize.rs @@ -3,7 +3,7 @@ use argus_ext::ty::{EvaluationResultExt, TyExt}; use index_vec::IndexVec; use rustc_hir::def_id::DefId; use rustc_infer::infer::InferCtxt; -use rustc_middle::ty::Predicate; +use rustc_middle::ty; use rustc_span::Span; use rustc_trait_selection::{ solve::inspect::{ @@ -171,6 +171,64 @@ impl SerializedTreeVisitor<'_> { } } +impl<'tcx> SerializedTreeVisitor<'tcx> { + /// Visited the nested subgoals of `candidate`, removing subgoals whose + /// success depends on another failing goal.. + // TODO: See the commented out `InspectCandidateExt`, this should replace the below + // function when the necessary changes have been upstreamed to rustc. That trait + // will allow us to *only* traverse the subgoals to keep, rather than removed + // goals after visiting them initially. + fn visit_nested_roots( + &mut self, + tcx: ty::TyCtxt<'tcx>, + candidate_idx: ProofNodeIdx, + candidate: InspectCandidate<'_, 'tcx>, + ) -> >::Result { + use crate::aadebug::tree as dgb_tree; + + // HACK: visit all nested candidates then remove them after the fact if they + // shouldn't have been visited in the first place. + candidate.visit_nested_in_probe(self); + + // After visiting nested subgoals, remove those from the tree that + // depend on a failing subgoal. + let subgoals = self + .topology + .children(candidate_idx) + .collect::>(); + + // XXX: rust can't infer the more generic type for this, so it needs to get + // annotated ... argh + let get_result: &dyn for<'a> Fn(&'a ProofNodeIdx) -> EvaluationResult = + &|&idx| match self.aadebug.ns[idx] { + dgb_tree::N::R { result, .. } => result, + _ => unreachable!(), + }; + + let error_sources = argus_ext::ty::identify_error_sources( + &subgoals, + get_result, + |&idx| match self.aadebug.ns[idx] { + dgb_tree::N::R { goal, .. } => goal.predicate, + _ => unreachable!(), + }, + move |_| tcx, + ) + .collect::>(); + + for (i, subgoal) in subgoals.into_iter().enumerate() { + if get_result(&subgoal).is_no() && !error_sources.contains(&i) { + self + .topology + .children + .get_mut(&candidate_idx) + .map(|v| v.retain(|&n| n != subgoal)); + self.topology.parent.remove(&subgoal); + } + } + } +} + impl<'tcx> ProofTreeVisitor<'tcx> for SerializedTreeVisitor<'tcx> { type Result = (); @@ -222,7 +280,7 @@ impl<'tcx> ProofTreeVisitor<'tcx> for SerializedTreeVisitor<'tcx> { self.topology.add(here_idx, candidate_idx); self.previous = Some(candidate_idx); - c.visit_nested_roots(self); + self.visit_nested_roots(goal.infcx().tcx, candidate_idx, c); // FIXME: is this necessary now that we store all nodes? add_result_if_empty(self, candidate_idx); @@ -234,7 +292,7 @@ impl<'tcx> ProofTreeVisitor<'tcx> for SerializedTreeVisitor<'tcx> { } pub fn try_serialize<'tcx>( - goal: solve::Goal<'tcx, Predicate<'tcx>>, + goal: solve::Goal<'tcx, ty::Predicate<'tcx>>, result: EvaluationResult, span: Span, infcx: &InferCtxt<'tcx>, @@ -249,50 +307,54 @@ pub fn try_serialize<'tcx>( }) } -trait InspectCandidateExt<'tcx> { - fn visit_nested_roots>( - &self, - visitor: &mut V, - ) -> V::Result; -} - -impl<'tcx> InspectCandidateExt<'tcx> for InspectCandidate<'_, 'tcx> { - fn visit_nested_roots>( - &self, - visitor: &mut V, - ) -> V::Result { - self.visit_nested_in_probe(visitor) - // TODO: if we can lobby lcnr to make `visit_with` public then we don't have to visit - // all subgoals, only those that cause errors. This means that if `F: Fn()` fails, we - // don't need to check the bound `::Output: ResBound`. - // - // If this gets used we no longer have to check this in the `aadebug` module. - // - // // TODO: add rustc_ast_ir to extern crates. - // use rustc_ast_ir::visit::VisitorResult; - // use rustc_ast_ir::try_visit; - // - // self.goal().infcx().probe(|_| { - // let mut all_sub_goals = self.instantiate_nested_goals(visitor.span()); - // // Put all successful subgoals at the front of the list. - // let err_start_idx = itertools::partition(&mut all_sub_goals, |g| g.result().is_yes()); - // let (successful_subgoals, failed_subgoals) = all_sub_goals.split_at_mut(err_start_idx); - // // TODO: make a version of `retain_error_sources` that iterates over - // // a slice and picks out the errors by index, then we can avoid the clone. - // let mut failed_subgoals_vec = failed_subgoals.to_vec(); - // argus_ext::ty::retain_error_sources( - // &mut failed_subgoals_vec, - // |g| g.result(), - // |g| g.goal().predicate, - // |g| g.infcx().tcx, - // |a, b| a.goal().predicate == b.goal().predicate, - // ); - // - // for goal in failed_subgoals_vec.iter().chain(successful_subgoals.iter()) { - // try_visit!(goal.visit_with(visitor)); - // } - // - // V::Result::output() - // }) - } -} +// TODO: after we make the `visit_with` method public this can be a generic trait. +// trait InspectCandidateExt<'tcx> { +// fn visit_nested_roots>( +// &self, +// visitor: &mut V, +// ) -> V::Result; +// } + +// impl<'tcx> InspectCandidateExt<'tcx> for InspectCandidate<'_, 'tcx> { +// fn visit_nested_roots>( +// &self, +// visitor: &mut V, +// ) -> V::Result { +// // HACK: visit all nested candidates then remove them after the fact if they +// // shouldn't have been visited in the first place. +// self.visit_nested_in_probe(visitor); + +// // TODO: if we can lobby lcnr to make `visit_with` public then we don't have to visit +// // all subgoals, only those that cause errors. This means that if `F: Fn()` fails, we +// // don't need to check the bound `::Output: ResBound`. +// // +// // If this gets used we no longer have to check this in the `aadebug` module. +// // +// // // TODO: add rustc_ast_ir to extern crates. +// // use rustc_ast_ir::visit::VisitorResult; +// // use rustc_ast_ir::try_visit; +// // +// // self.goal().infcx().probe(|_| { +// // let mut all_sub_goals = self.instantiate_nested_goals(visitor.span()); +// // // Put all successful subgoals at the front of the list. +// // let err_start_idx = itertools::partition(&mut all_sub_goals, |g| g.result().is_yes()); +// // let (successful_subgoals, failed_subgoals) = all_sub_goals.split_at_mut(err_start_idx); +// // // TODO: make a version of `retain_error_sources` that iterates over +// // // a slice and picks out the errors by index, then we can avoid the clone. +// // let mut failed_subgoals_vec = failed_subgoals.to_vec(); +// // argus_ext::ty::retain_error_sources( +// // &mut failed_subgoals_vec, +// // |g| g.result(), +// // |g| g.goal().predicate, +// // |g| g.infcx().tcx, +// // |a, b| a.goal().predicate == b.goal().predicate, +// // ); +// // +// // for goal in failed_subgoals_vec.iter().chain(successful_subgoals.iter()) { +// // try_visit!(goal.visit_with(visitor)); +// // } +// // +// // V::Result::output() +// // }) +// } +// } diff --git a/ide/packages/extension/package.json b/ide/packages/extension/package.json index 29d096a..9b618d9 100644 --- a/ide/packages/extension/package.json +++ b/ide/packages/extension/package.json @@ -5,7 +5,7 @@ "description": "A trait debugger for Rust", "license": "MIT", "icon": "argus-logo-128.png", - "version": "0.1.9", + "version": "0.1.10", "engines": { "vscode": "^1.79.0" }, From bd3fc38edbeeeefd775fb9728429d36df0d43671 Mon Sep 17 00:00:00 2001 From: gavinleroy Date: Mon, 22 Jul 2024 15:41:32 -0600 Subject: [PATCH 2/3] Remove double angles, shade TreeApp, hide extra failing subsets. --- ide/packages/common/src/BodyInfo.ts | 11 ++++--- ide/packages/panoptes/src/File.tsx | 2 +- ide/packages/panoptes/src/Obligation.css | 8 +++++ ide/packages/panoptes/src/Obligation.tsx | 4 ++- .../panoptes/src/TreeView/Subsets.tsx | 32 ++++++++++++------- .../panoptes/src/TreeView/TreeApp.tsx | 5 ++- ide/packages/print/src/private/path.tsx | 6 ++-- 7 files changed, 45 insertions(+), 23 deletions(-) diff --git a/ide/packages/common/src/BodyInfo.ts b/ide/packages/common/src/BodyInfo.ts index ade3a83..72ddbb6 100644 --- a/ide/packages/common/src/BodyInfo.ts +++ b/ide/packages/common/src/BodyInfo.ts @@ -26,10 +26,6 @@ class BodyInfo { return this.oib.ambiguityErrors.length + this.oib.traitErrors.length; } - get exprs(): ExprIdx[] { - return _.map(this.oib.exprs, (_, idx) => idx); - } - get name() { return this.oib.name; } @@ -49,6 +45,7 @@ class BodyInfo { get tyInterner() { return this.oib.tys; } + notHidden(hash: ObligationIdx): boolean { const o = this.getObligation(hash); if (o === undefined) { @@ -57,8 +54,12 @@ class BodyInfo { return this.showHidden || isHiddenObl(o); } + exprs(): ExprIdx[] { + return _.map(this.oib.exprs, (_, idx) => idx); + } + hasVisibleExprs() { - return _.some(this.exprs, idx => this.hasVisibleObligations(idx)); + return _.some(this.exprs(), idx => this.hasVisibleObligations(idx)); } hasVisibleObligations(idx: ExprIdx) { diff --git a/ide/packages/panoptes/src/File.tsx b/ide/packages/panoptes/src/File.tsx index 38e61b7..1740746 100644 --- a/ide/packages/panoptes/src/File.tsx +++ b/ide/packages/panoptes/src/File.tsx @@ -59,7 +59,7 @@ const ObligationBody = observer(({ bodyInfo }: { bodyInfo: BodyInfo }) => { info={header} startOpen={openChildren} Children={() => - _.map(bodyInfo.exprs, (i, idx) => ) + _.map(bodyInfo.exprs(), (i, idx) => ) } /> diff --git a/ide/packages/panoptes/src/Obligation.css b/ide/packages/panoptes/src/Obligation.css index c47d216..e7a2166 100644 --- a/ide/packages/panoptes/src/Obligation.css +++ b/ide/packages/panoptes/src/Obligation.css @@ -1,3 +1,11 @@ .ObligationCard > vscode-text-area { display: block; } + +.TreeAppObligationWrapper { + background-color: var(--vscode-editor-selectionHighlightBackground); + border-radius: 3px; + padding: 0.15em; + + margin-bottom: 0.5em; +} \ No newline at end of file diff --git a/ide/packages/panoptes/src/Obligation.tsx b/ide/packages/panoptes/src/Obligation.tsx index 3079475..c4295cf 100644 --- a/ide/packages/panoptes/src/Obligation.tsx +++ b/ide/packages/panoptes/src/Obligation.tsx @@ -97,7 +97,9 @@ const ProofTreeWrapper = ({ ) : tree === undefined ? ( ) : ( - +
+ +
); return content; diff --git a/ide/packages/panoptes/src/TreeView/Subsets.tsx b/ide/packages/panoptes/src/TreeView/Subsets.tsx index 0972888..619b2c5 100644 --- a/ide/packages/panoptes/src/TreeView/Subsets.tsx +++ b/ide/packages/panoptes/src/TreeView/Subsets.tsx @@ -50,18 +50,22 @@ export const RenderBottomUpSets = ({ return null; } + const [hovered, setHovered] = useState(false); + const cn = classNames("FailingSet", { "is-hovered": hovered }); + // If there is only a single predicate, no need to provide all the // extra information around "grouped predicate sets". if (views.tree.length === 1) { return ( - +
+ +
); } - const [hovered, setHovered] = useState(false); const onHover = () => { MiniBufferDataStore.set({ kind: "argus-note", @@ -80,7 +84,7 @@ export const RenderBottomUpSets = ({ }; return ( -
+
{_.map(views.tree, (leaf, i) => ( ( - - )); + const argusRecommends = ; + const tail = _.tail(views); + + const otherLabel = "Other failures"; const fallbacks = tail.length === 0 ? null : ( Other failures ...} + info={{otherLabel} ...} Children={() => _.map(tail, (v, i) => )} /> ); return ( - +

+ Argus recommends investigating these failed oblgiations. Click on ’ + {otherLabel}‘ below to see other failed obligations. +

+ {fallbacks} ); diff --git a/ide/packages/panoptes/src/TreeView/TreeApp.tsx b/ide/packages/panoptes/src/TreeView/TreeApp.tsx index 5cb3a84..f12b3e0 100644 --- a/ide/packages/panoptes/src/TreeView/TreeApp.tsx +++ b/ide/packages/panoptes/src/TreeView/TreeApp.tsx @@ -49,8 +49,11 @@ const TreeApp = ({ const tabs: [string, React.FC][] = [["Top Down", TopDown]]; if (treeInfo.errorLeaves().length > 0) { - tabs.unshift(["Help Me", Erotisi]); + // Unshift to place this first tabs.unshift(["Bottom Up", FailedSubsets]); + + // Push to place this last + tabs.push(["Help Me", Erotisi]); } // HACK: we shouldn't test for eval mode here but Playwright is off on the button click. diff --git a/ide/packages/print/src/private/path.tsx b/ide/packages/print/src/private/path.tsx index b1e31d5..347d5ef 100644 --- a/ide/packages/print/src/private/path.tsx +++ b/ide/packages/print/src/private/path.tsx @@ -79,11 +79,11 @@ export const PrintDefPath = ({ o }: { o: DefinedPath }) => { } + Children={() => } /> )} - Rest={() => } + Rest={() => } /> ); }; @@ -192,7 +192,7 @@ const PrintInToggleableEnvironment = ({ bypassToggle, Elem }: { bypassToggle: boolean; Elem: React.FC }) => { - // Use a metric of "type size" rather than inner lenght. + // Use a metric of "type size" rather than inner length. const useToggle = useContext(AllowToggle) && bypassToggle; return ( // TODO: do we want to allow nested toggles? From 5cf0e61e426077a7f31df33fcad34a5e2e1b39c5 Mon Sep 17 00:00:00 2001 From: gavinleroy Date: Mon, 22 Jul 2024 15:49:41 -0600 Subject: [PATCH 3/3] Add NBSP after impl --- ide/packages/print/src/private/ty.tsx | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/ide/packages/print/src/private/ty.tsx b/ide/packages/print/src/private/ty.tsx index b0e2512..42c4bad 100644 --- a/ide/packages/print/src/private/ty.tsx +++ b/ide/packages/print/src/private/ty.tsx @@ -667,7 +667,7 @@ export const PrintOpaqueImplType = ({ o }: { o: OpaqueImpl }) => { : null; const start = - implComponents.length === 0 && sized === "" ? "{opaque}" : "impl "; + implComponents.length === 0 && sized === "" ? "{opaque}" : `impl${nbsp}`; return ( <>