From af96bb341481cc5ca715e033f6219f9561385e12 Mon Sep 17 00:00:00 2001
From: Gavin Gray <20209337+gavinleroy@users.noreply.github.com>
Date: Wed, 27 Nov 2024 17:22:23 -0500
Subject: [PATCH] Testing Infrastructure (#47)

* Update the evaluation framework to use Nix. Run Fmt and Fix. Restructure the Makefile

* Update evaluation scripts
---
 .gitignore                                    |   1 +
 Makefile.toml                                 |  83 +++++-
 crates/argus-cli/tests/test_examples.rs       |  27 +-
 crates/argus/src/aadebug/mod.rs               |   6 +-
 crates/argus/src/aadebug/tree.rs              |  14 +
 crates/argus/src/ext.rs                       |   4 +-
 crates/argus/src/proof_tree/serialize.rs      |  34 +--
 flake.lock                                    |  77 ++++-
 flake.nix                                     |  39 ++-
 ide/packages/common/src/TreeInfo.ts           |  67 +++--
 ide/packages/common/src/context.ts            |  13 +-
 ide/packages/common/src/lib.ts                |   5 +-
 ide/packages/evaluation/package.json          |   4 +-
 ide/packages/evaluation/src/basic.ts          |  19 +-
 ide/packages/evaluation/src/main.ts           |  35 ++-
 ide/packages/evaluation/src/page.ts           |   7 +-
 ide/packages/evaluation/src/random.ts         |  95 -------
 ide/packages/evaluation/src/rootCauses.ts     |   5 +-
 ide/packages/evaluation/src/utils.ts          |  18 +-
 ide/packages/evaluation/src/visual.ts         |   2 +-
 ide/packages/panoptes/src/App.tsx             |   6 +-
 .../panoptes/src/TreeView/BottomUp.tsx        |  47 +--
 .../panoptes/src/TreeView/Erotisi.tsx         |   6 +-
 .../panoptes/src/TreeView/TreeApp.tsx         |   2 +-
 .../panoptes/src/TreeView/heuristic.ts        | 268 ------------------
 ide/pnpm-lock.yaml                            |  26 +-
 26 files changed, 363 insertions(+), 547 deletions(-)
 delete mode 100644 ide/packages/evaluation/src/random.ts
 delete mode 100644 ide/packages/panoptes/src/TreeView/heuristic.ts

diff --git a/.gitignore b/.gitignore
index 2edd08e..ab1e14e 100644
--- a/.gitignore
+++ b/.gitignore
@@ -26,3 +26,4 @@ bindings/
 
 # Evaluation cache
 data/
+*.csv
diff --git a/Makefile.toml b/Makefile.toml
index 189b7ca..69ee2cc 100644
--- a/Makefile.toml
+++ b/Makefile.toml
@@ -2,27 +2,84 @@
 skip_core_tasks = true
 default_to_workspace = false
 
-[tasks.watch-front]
-script = "cargo watch -i frontend -x 'install --path crates/argus-cli'"
+# #################### #
+# Binding initializers #
+# #################### #
 
-[tasks.watch-front-debug]
-script = "cargo watch -i frontend -x 'install --path crates/argus-cli --frozen --offline --debug'"
+[tasks.init-bindings-lib]
+command = "cargo"
+args = [
+  "test", "-p", "argus-lib", "--lib", "export_bindings", "--locked"
+]
 
-[tasks.watch.run_task]
-name = ["watch-front"]
-parallel = true
+[tasks.init-bindings-ser]
+command = "cargo"
+args = ["test", "-p", "argus-ser", "--locked"]
 
 [tasks.init-bindings]
+command = "./scripts/ts-rs.scm"
+dependences = ["tasks.init-bindings-lib", "tasks.init-bindings-ser"]
+
+[tasks.evaluation-node]
+command = "node"
+args = ["ide/packages/evaluation/dist/evaluation.cjs", "-s", "./data", "${@}"]
+
+# #################### #
+#       Builders       #
+# #################### #
+
+[tasks.build-back]
+command = "cargo"
+args = [
+  "install", "--path", "crates/argus-cli", "--locked", 
+]
+
+# TODO: is there a way to set a command specific environment variable?
+#       The below will make the configuration global...
+# [env]
+# CARGO_MAKE_WORKING_DIRECTORY = "ide"
+[tasks.build-ide]
 script = """
-cargo test -p argus-lib --lib export_bindings --locked
-cargo test -p argus-ser --locked
-./scripts/ts-rs.scm
+cd ide && depot build
 """
 
-[tasks.evaluation]
+[tasks.build.run_task]
+name = ["build-back", "build-ide"]
+parallel = true
+
+[tasks.watch-back]
+command = "cargo"
+args = [	
+  "watch", 
+  "-i", 
+  "frontend", 
+  "-x", 
+  "'install", "--path", "crates/argus-cli", "${@}", "'", 
+]
+
+[tasks.watch.run_task]
+name = ["watch-back"]
+parallel = true
+
+# ############### #
+# Evaluation Crap #
+# ############### #
+
+[tasks.eval]
+command = "node"
+args = ["ide/packages/evaluation/dist/evaluation.cjs", "-h", "${@}"]
+dependencies = ["build"]
+
+[tasks.eval-init]
+command = "node"
+args = ["ide/packages/evaluation/dist/evaluation.cjs", "-s", "./data", "${@}"]
+dependencies = ["build"]
+
+[tasks.eval-serve]
 script = """
-cd ide && depot build && cd ..
-node ide/packages/evaluation/dist/evaluation.cjs -s ./data
 python3 -m webbrowser http://localhost:8080/eval
 ./scripts/evaluation.scm
 """
+
+[tasks.evaluation]
+dependencies = ["evaluation-init", "evaluation-serve"]
diff --git a/crates/argus-cli/tests/test_examples.rs b/crates/argus-cli/tests/test_examples.rs
index f070b17..1dcdb72 100644
--- a/crates/argus-cli/tests/test_examples.rs
+++ b/crates/argus-cli/tests/test_examples.rs
@@ -1,9 +1,16 @@
-use std::{env, fs, path::Path, process::Command, sync::Once};
+use std::{
+  env, fs,
+  path::Path,
+  process::{Command, Stdio},
+  sync::Once,
+};
 
 use anyhow::{ensure, Context, Result};
 
 static SETUP: Once = Once::new();
 
+static DNF_PERF_P: &str = "dnf-perf.csv";
+
 fn run<P: AsRef<Path>>(dir: P, f: impl FnOnce(&mut Command)) -> Result<String> {
   let root = env::temp_dir().join("argus");
   let heredir = Path::new(".").canonicalize()?;
@@ -17,12 +24,13 @@ fn run<P: AsRef<Path>>(dir: P, f: impl FnOnce(&mut Command)) -> Result<String> {
     if !status.success() {
       panic!("installing argus failed")
     }
+
+    fs::write(DNF_PERF_P, "Label,N,Time\n").unwrap();
   });
 
   let mut cmd = Command::new("cargo");
   cmd.arg("argus");
-  cmd.arg("obligations");
-  // Don't specify a file to analyze all local crates.
+  cmd.arg("bundle");
 
   let path = format!(
     "{}:{}",
@@ -34,6 +42,14 @@ fn run<P: AsRef<Path>>(dir: P, f: impl FnOnce(&mut Command)) -> Result<String> {
   let ws = heredir.join("tests").join(dir);
   cmd.current_dir(&ws);
 
+  // NOTE: performance data is written to STDERR, so we capture it and place it in a file.
+  let perf_file = fs::OpenOptions::new()
+    .create(true)
+    .append(true)
+    .open(DNF_PERF_P)
+    .unwrap();
+  cmd.stderr(Stdio::from(perf_file));
+
   f(&mut cmd);
 
   let _ = fs::remove_dir_all(ws.join("target"));
@@ -61,13 +77,12 @@ macro_rules! mk_tests_for {
 mk_tests_for! {
   axum,
   bevy,
-  // chumsky, // NOTE: as of now this consumes too much memory
+  // chumsky,
   diesel,
-  easy_ml,
+  // easy_ml,
   entrait,
   nalgebra,
   uom
-  // tauri_project
 }
 
 // TODO: include individual test if we want to see a particular output
diff --git a/crates/argus/src/aadebug/mod.rs b/crates/argus/src/aadebug/mod.rs
index 3b69702..64d6fe5 100644
--- a/crates/argus/src/aadebug/mod.rs
+++ b/crates/argus/src/aadebug/mod.rs
@@ -18,6 +18,7 @@ use crate::proof_tree::{topology::TreeTopology, ProofNodeIdx};
 pub struct Storage<'tcx> {
   pub ns: IndexVec<ProofNodeIdx, tree::N<'tcx>>,
   maybe_ambiguous: bool,
+  report_performance: bool,
 }
 
 #[derive(Serialize, Debug, Clone)]
@@ -30,9 +31,11 @@ pub struct AnalysisResults {
 
 impl<'tcx> Storage<'tcx> {
   pub fn new(maybe_ambiguous: bool) -> Self {
+    let report_performance = std::env::var("ARGUS_DNF_PERF").is_ok();
     Self {
       ns: IndexVec::new(),
       maybe_ambiguous,
+      report_performance,
     }
   }
 
@@ -106,7 +109,8 @@ impl<'tcx> Storage<'tcx> {
     root: ProofNodeIdx,
     topo: &TreeTopology,
   ) -> AnalysisResults {
-    let tree = &tree::T::new(root, &self.ns, topo, false);
+    let tree =
+      &tree::T::new(root, &self.ns, topo, false, self.report_performance);
     let tree_start = Instant::now();
 
     let mut sets = vec![];
diff --git a/crates/argus/src/aadebug/tree.rs b/crates/argus/src/aadebug/tree.rs
index fb6d1f9..0aeaba0 100644
--- a/crates/argus/src/aadebug/tree.rs
+++ b/crates/argus/src/aadebug/tree.rs
@@ -333,6 +333,7 @@ pub struct T<'a, 'tcx: 'a> {
   pub ns: &'a IndexVec<I, N<'tcx>>,
   pub topology: &'a TreeTopology,
   pub maybe_ambiguous: bool,
+  report_performance: bool,
   dnf: RefCell<Option<Dnf<I>>>,
 }
 
@@ -342,12 +343,14 @@ impl<'a, 'tcx: 'a> T<'a, 'tcx> {
     ns: &'a IndexVec<I, N<'tcx>>,
     topology: &'a TreeTopology,
     maybe_ambiguous: bool,
+    report_performance: bool,
   ) -> Self {
     Self {
       root,
       ns,
       topology,
       maybe_ambiguous,
+      report_performance,
       dnf: RefCell::new(None),
     }
   }
@@ -436,8 +439,19 @@ impl<'a, 'tcx: 'a> T<'a, 'tcx> {
 
     let root = self.goal(self.root).expect("invalid root");
     let dnf = _goal(self, &root).unwrap_or_else(Dnf::default);
+
     timer::elapsed(&dnf_report_msg, dnf_start);
 
+    // HACK to gather the performance report we write to stderr the CSV values `PERF<NODES><TIME>`
+    // The testing harness will take the stderr output and place it in a file for analysis.
+    if self.report_performance {
+      eprintln!(
+        "PERF,{:?},{:.04}",
+        self.ns.len(),
+        dnf_start.elapsed().as_secs_f64()
+      );
+    }
+
     self.dnf.replace(Some(dnf));
     self.expect_dnf()
   }
diff --git a/crates/argus/src/ext.rs b/crates/argus/src/ext.rs
index 2f404f4..f7a0bc0 100644
--- a/crates/argus/src/ext.rs
+++ b/crates/argus/src/ext.rs
@@ -53,7 +53,9 @@ impl<'tcx> InferCtxtExt<'tcx> for InferCtxt<'tcx> {
       let items = vec![LI::Iterator, LI::Sized, LI::Deref];
       let lis = self.tcx.lang_items();
       for i in items {
-        if let Some(def_id) = lis.get(i) && p.is_trait_pred_rhs(def_id) {
+        if let Some(def_id) = lis.get(i)
+          && p.is_trait_pred_rhs(def_id)
+        {
           return true;
         }
       }
diff --git a/crates/argus/src/proof_tree/serialize.rs b/crates/argus/src/proof_tree/serialize.rs
index f1784de..4cd15fd 100644
--- a/crates/argus/src/proof_tree/serialize.rs
+++ b/crates/argus/src/proof_tree/serialize.rs
@@ -50,6 +50,7 @@ impl SerializedTreeVisitor<'_> {
   }
 
   fn check_goal_projection(&mut self, goal: &InspectGoal) {
+    // We only care about successful alias relations
     if goal.result().is_yes()
       && let ty::PredicateKind::AliasRelate(
         t1,
@@ -74,6 +75,7 @@ impl SerializedTreeVisitor<'_> {
         let idx2: TyIdx = interner.borrow().get_idx(&t2)?;
         Some((idx1, idx2))
       }) && t1 != t2
+        && !self.projection_values.contains_key(&t1)
       {
         let not_empty = self.projection_values.insert(t1, t2);
         debug_assert!(not_empty.is_none());
@@ -81,39 +83,7 @@ impl SerializedTreeVisitor<'_> {
     }
   }
 
-  #[cfg(debug_assertions)]
-  fn is_valid(&self) -> Result<()> {
-    for (pidx, node) in self.nodes.iter_enumerated() {
-      match node {
-        Node::Goal(g) => {
-          anyhow::ensure!(
-            !self.topology.is_leaf(pidx),
-            "non-leaf node (goal) has no children {:?}",
-            self.interners.goal(*g)
-          );
-        }
-        Node::Candidate(c) => {
-          anyhow::ensure!(
-            !self.topology.is_leaf(pidx),
-            "non-leaf node (candidate) has no children {:?}",
-            self.interners.candidate(*c)
-          );
-        }
-        Node::Result(..) => {
-          anyhow::ensure!(
-            self.topology.is_leaf(pidx),
-            "result node is not a leaf"
-          );
-        }
-      }
-    }
-    Ok(())
-  }
-
   pub fn into_tree(self) -> Result<SerializedTree> {
-    #[cfg(debug_assertions)]
-    self.is_valid()?;
-
     let SerializedTreeVisitor {
       root: Some(root),
       mut nodes,
diff --git a/flake.lock b/flake.lock
index fdc5449..d4056a4 100644
--- a/flake.lock
+++ b/flake.lock
@@ -1,9 +1,46 @@
 {
   "nodes": {
+    "depot-js": {
+      "inputs": {
+        "flake-utils": "flake-utils",
+        "nixpkgs": "nixpkgs"
+      },
+      "locked": {
+        "lastModified": 1731019925,
+        "narHash": "sha256-Yp2ib3rSza/0YNTtzGQmsDi4uD+COAd4OYfAcvCA0f4=",
+        "owner": "cognitive-engineering-lab",
+        "repo": "depot",
+        "rev": "e7464c57bc11aaeb88930719b84b21c7dfe87536",
+        "type": "github"
+      },
+      "original": {
+        "owner": "cognitive-engineering-lab",
+        "repo": "depot",
+        "type": "github"
+      }
+    },
     "flake-utils": {
       "inputs": {
         "systems": "systems"
       },
+      "locked": {
+        "lastModified": 1726560853,
+        "narHash": "sha256-X6rJYSESBVr3hBoH0WbKE5KvhPU5bloyZ2L4K60/fPQ=",
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "rev": "c1dfcf08411b08f6b8615f7d8971a2bfa81d5e8a",
+        "type": "github"
+      },
+      "original": {
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "type": "github"
+      }
+    },
+    "flake-utils_2": {
+      "inputs": {
+        "systems": "systems_2"
+      },
       "locked": {
         "lastModified": 1710146030,
         "narHash": "sha256-SZ5L6eA7HJ/nmkzGG7/ISclqe6oZdOZTNoesiInkXPQ=",
@@ -19,6 +56,22 @@
       }
     },
     "nixpkgs": {
+      "locked": {
+        "lastModified": 1730531603,
+        "narHash": "sha256-Dqg6si5CqIzm87sp57j5nTaeBbWhHFaVyG7V6L8k3lY=",
+        "owner": "nixos",
+        "repo": "nixpkgs",
+        "rev": "7ffd9ae656aec493492b44d0ddfb28e79a1ea25d",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nixos",
+        "ref": "nixos-unstable",
+        "repo": "nixpkgs",
+        "type": "github"
+      }
+    },
+    "nixpkgs_2": {
       "locked": {
         "lastModified": 1720031269,
         "narHash": "sha256-rwz8NJZV+387rnWpTYcXaRNvzUSnnF9aHONoJIYmiUQ=",
@@ -34,7 +87,7 @@
         "type": "github"
       }
     },
-    "nixpkgs_2": {
+    "nixpkgs_3": {
       "locked": {
         "lastModified": 1720181791,
         "narHash": "sha256-i4vJL12/AdyuQuviMMd1Hk2tsGt02hDNhA0Zj1m16N8=",
@@ -52,14 +105,15 @@
     },
     "root": {
       "inputs": {
-        "flake-utils": "flake-utils",
-        "nixpkgs": "nixpkgs",
+        "depot-js": "depot-js",
+        "flake-utils": "flake-utils_2",
+        "nixpkgs": "nixpkgs_2",
         "rust-overlay": "rust-overlay"
       }
     },
     "rust-overlay": {
       "inputs": {
-        "nixpkgs": "nixpkgs_2"
+        "nixpkgs": "nixpkgs_3"
       },
       "locked": {
         "lastModified": 1720318855,
@@ -89,6 +143,21 @@
         "repo": "default",
         "type": "github"
       }
+    },
+    "systems_2": {
+      "locked": {
+        "lastModified": 1681028828,
+        "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=",
+        "owner": "nix-systems",
+        "repo": "default",
+        "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nix-systems",
+        "repo": "default",
+        "type": "github"
+      }
     }
   },
   "root": "root",
diff --git a/flake.nix b/flake.nix
index 07973af..3b73734 100644
--- a/flake.nix
+++ b/flake.nix
@@ -3,9 +3,10 @@
     nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable";
     flake-utils.url = "github:numtide/flake-utils";
     rust-overlay.url = "github:oxalica/rust-overlay";
+    depot-js.url = "github:cognitive-engineering-lab/depot";
   };
 
-  outputs = { self, nixpkgs, flake-utils, rust-overlay }:
+  outputs = { self, nixpkgs, flake-utils, rust-overlay, depot-js }:
     flake-utils.lib.eachDefaultSystem (system:
       let
         overlays = [ (import rust-overlay) ];
@@ -17,27 +18,6 @@
         meta = (builtins.fromTOML (builtins.readFile (entry-crate/Cargo.toml))).package;
         inherit (meta) name version;
 
-        depotjs = pkgs.rustPlatform.buildRustPackage rec {
-          pname = "depot";
-          version = "0.2.17";
-
-          # Depot tests require lots of external toolchains, node, typedoc, biome, ...
-          # so we'll just skip all tests for now and figure this out later.
-          doCheck = false;
-
-          src = pkgs.fetchFromGitHub {
-            owner = "cognitive-engineering-lab";
-            repo = pname;
-            rev = "v${version}";
-            hash = "sha256-kiQXxTVvzfovCn0YmOH/vTUQHyRS39gH7iBGaKyRZFg=";
-          };
-
-          cargoHash = "sha256-m9sG//vBUqGLwWHkyq+sJ8rkQOeaif56l394dgPU1uQ=";
-          buildInputs = with pkgs; lib.optionals stdenv.isDarwin [
-            darwin.apple_sdk.frameworks.SystemConfiguration
-          ];
-        };
-
         mdbook-image-size = with pkgs; rustPlatform.buildRustPackage rec {
           pname = "mdbook-image-size";
           version = "0.2.0";
@@ -85,8 +65,11 @@
 
             toolchain
 
+            # Required for the evaluation
             guile
-            depotjs
+            guile-json
+
+            depot-js.packages.${system}.default
             nodejs_22
             nodePackages.pnpm
             codespell
@@ -109,7 +92,17 @@
             udev.dev
           ];
 
+          # Needed in order to run `cargo argus ...` within the directory
+          shellHook = ''
+            export DYLD_LIBRARY_PATH="$DYLD_LIBRARY_PATH:$(rustc --print target-libdir)"
+          '';
+
           RUSTC_LINKER = "${llvmPackages.clangUseLLVM}/bin/clang";
+
+          # NOTE: currently playwright-driver uses version 1.40.0, when something inevitably fails,
+          # check that the version of playwright-driver and that of the NPM playwright 
+          # `packages/evaluation/package.json` match.
+          PLAYWRIGHT_BROWSERS_PATH="${playwright-driver.browsers}";
         };
       });
 }
diff --git a/ide/packages/common/src/TreeInfo.ts b/ide/packages/common/src/TreeInfo.ts
index 65da1d9..5d873cf 100644
--- a/ide/packages/common/src/TreeInfo.ts
+++ b/ide/packages/common/src/TreeInfo.ts
@@ -6,6 +6,7 @@ import type {
   EvaluationResult,
   GoalIdx,
   GoalKind,
+  Heuristic,
   Implementors,
   ProofNodeIdx,
   ResultIdx,
@@ -13,6 +14,7 @@ import type {
   SetHeuristic,
   TreeTopology
 } from "./bindings";
+import type { SortStrategy } from "./lib";
 
 export type TreeViewWithRoot = TreeView & { root: ProofNodeIdx };
 
@@ -280,21 +282,51 @@ export class TreeInfo {
     return this.tree.root;
   }
 
-  public failedSets() {
+  public numFailedSets() {
+    return this.failedSets().length;
+  }
+
+  public failedSetsSorted(sortAs: SortStrategy = "inertia"): SetHeuristic[] {
+    const sets = this.failedSets();
+
+    switch (sortAs) {
+      case "inertia":
+        return _.sortBy(sets, TreeInfo.setInertia);
+      case "depth":
+        return _.sortBy(sets, s => this.setDepth(s));
+      case "vars":
+        return _.sortBy(sets, s => this.setInferVars(s));
+      default:
+        throw new Error("Unknown sort strategy");
+    }
+  }
+
+  private failedSets(): SetHeuristic[] {
     if (this.showHidden) return this.tree.analysis.problematicSets;
 
+    const setHasBadUnification = (s: SetHeuristic) =>
+      _.some(s.goals, g => isBadUnification(g.kind));
+
+    // Find the lowest inertia set that *does not* have a unification failure.
+    const nonUnificationFailureLowestInertia = _.min(
+      _.map(this.tree.analysis.problematicSets, s =>
+        setHasBadUnification(s) ? undefined : TreeInfo.setInertia(s)
+      )
+    );
+
     // If all the problematic sets involve a bad unification, then we
     // have to live with them, don't filter.
-    if (
-      _.every(this.tree.analysis.problematicSets, s =>
-        _.some(s.goals, g => isBadUnification(g.kind))
-      )
-    )
+    if (nonUnificationFailureLowestInertia === undefined) {
       return this.tree.analysis.problematicSets;
+    }
 
-    // Keep only the sets that don't have a bad unification
-    return _.filter(this.tree.analysis.problematicSets, s =>
-      _.every(s.goals, g => !isBadUnification(g.kind))
+    // Keep the sets that *don't* have unification failures OR have an
+    // inertia lower than `nonUnificationFailureLowestInertia`.
+    return _.filter(
+      this.tree.analysis.problematicSets,
+      s =>
+        !setHasBadUnification(s) ||
+        TreeInfo.setInertia(s) < nonUnificationFailureLowestInertia
     );
   }
 
@@ -349,13 +381,6 @@ export class TreeInfo {
 
   public children(n: ProofNodeIdx): ProofNodeIdx[] {
     const nodesToUnifyFailures = this.nodesInUnificationFailurePath();
-
-    // if (_.includes(nodesToUnifyFailures, 6222)) {
-    //   throw new Error("NODE NOT THERE");
-    // } else {
-    //   console.debug("Nodes to unify failures includes 6222");
-    // }
-
     const children = this.view.topology.children[n] ?? [];
     return _.difference(children, nodesToUnifyFailures);
   }
@@ -433,6 +458,16 @@ export class TreeInfo {
     return set.momentum;
   };
 
+  public setDepth(set: SetHeuristic) {
+    const heuristicDepth = (h: Heuristic) => this.depth(h.idx);
+    return _.sum(_.map(set.goals, heuristicDepth));
+  }
+
+  public setInferVars(set: SetHeuristic) {
+    const heuristicVars = (h: Heuristic) => this.inferVars(h.idx);
+    return _.sum(_.map(set.goals, heuristicVars));
+  }
+
   public minInertiaOnPath(n: ProofNodeIdx): number {
     const hs = _.filter(this.failedSets(), h =>
       _.some(h.goals, g => _.includes(this.pathToRoot(g.idx).pathInclusive, n))
diff --git a/ide/packages/common/src/context.ts b/ide/packages/common/src/context.ts
index 7840a22..622f477 100644
--- a/ide/packages/common/src/context.ts
+++ b/ide/packages/common/src/context.ts
@@ -3,12 +3,7 @@ import { createContext } from "react";
 import type BodyInfo from "./BodyInfo";
 import type TreeInfo from "./TreeInfo";
 import type { MessageSystem, TreeRenderParams } from "./communication";
-import type {
-  EvaluationMode,
-  Filename,
-  PanoptesConfig,
-  SystemSpec
-} from "./lib";
+import type { Filename, PanoptesConfig, SystemSpec } from "./lib";
 
 export const settingsToggles = ["show-hidden-obligations"] as const;
 
@@ -18,9 +13,9 @@ export type Settings = {
 
 export const AppContext = {
   MessageSystemContext: createContext<MessageSystem | undefined>(undefined),
-  ConfigurationContext: createContext<
-    (PanoptesConfig & { evalMode: EvaluationMode }) | undefined
-  >(undefined),
+  ConfigurationContext: createContext<Required<PanoptesConfig> | undefined>(
+    undefined
+  ),
   SystemSpecContext: createContext<SystemSpec | undefined>(undefined),
   SettingsContext: createContext<Settings>({ "show-hidden-obligations": false })
 };
diff --git a/ide/packages/common/src/lib.ts b/ide/packages/common/src/lib.ts
index 4d7f440..4e75d19 100644
--- a/ide/packages/common/src/lib.ts
+++ b/ide/packages/common/src/lib.ts
@@ -31,10 +31,13 @@ export const ConfigConsts = {
 export type PanoptesOptionalData = {
   target?: ErrorJumpTargetInfo;
   evalMode?: EvaluationMode;
+  rankMode?: SortStrategy;
 };
 
 export type SystemSpec = Omit<IssueOptions, "logText">;
-export type EvaluationMode = "release" | "rank" | "random";
+export type EvaluationMode = "release" | "evaluate";
+export type SortStrategy = "inertia" | "depth" | "vars";
+
 export interface FileInfo {
   fn: Filename;
   data: ObligationsInBody[];
diff --git a/ide/packages/evaluation/package.json b/ide/packages/evaluation/package.json
index 3c3647c..020809d 100644
--- a/ide/packages/evaluation/package.json
+++ b/ide/packages/evaluation/package.json
@@ -16,9 +16,9 @@
     "@types/tmp": "^0.2.6",
     "glob": "^8.1.0",
     "lodash": "^4.17.21",
-    "playwright": "^1.42.1",
+    "playwright": "1.40.0",
     "tmp": "^0.2.3",
     "unique-filename": "^3.0.0",
     "vite": "^4.4.9"
   }
-}
\ No newline at end of file
+}
diff --git a/ide/packages/evaluation/src/basic.ts b/ide/packages/evaluation/src/basic.ts
index 3a3e32f..32cb87e 100644
--- a/ide/packages/evaluation/src/basic.ts
+++ b/ide/packages/evaluation/src/basic.ts
@@ -32,7 +32,7 @@ async function createWorkspaceRunner() {
         console.debug(`MISSING: cause ${workspace}/${filename}`);
         return;
       }
-      const page = await openPage(context, filename, bundles, "rank");
+      const page = await openPage(context, filename, bundles);
 
       await sleep(5000);
       await expandBottomUpView(page);
@@ -48,22 +48,21 @@ async function createWorkspaceRunner() {
       const ranksStr = await Promise.all(
         _.map(goals, goal => goal.getAttribute("data-rank"))
       );
-      const rank = _.min(_.map(_.compact(ranksStr), r => Number(r)));
+      const rank = _.min(_.map(_.compact(ranksStr), r => Number(r))) ?? -1;
 
-      const numberTreeNodes = _.max(
-        _.flatten(
-          _.map(bundles, bundle =>
-            _.map(_.values(bundle.trees), tree => tree.nodes.length)
+      const numberTreeNodes =
+        _.max(
+          _.flatten(
+            _.map(bundles, bundle =>
+              _.map(_.values(bundle.trees), tree => tree.nodes.length)
+            )
           )
-        )
-      );
+        ) ?? -1;
 
       await page.close();
       return {
         workspace,
         filename,
-        cause: cause.message,
-        numberTreeNodes,
         rank
       };
     });
diff --git a/ide/packages/evaluation/src/main.ts b/ide/packages/evaluation/src/main.ts
index 7ac2dcb..90121d7 100644
--- a/ide/packages/evaluation/src/main.ts
+++ b/ide/packages/evaluation/src/main.ts
@@ -1,7 +1,7 @@
 import _ from "lodash";
 
+import fs from "node:fs";
 import { run as runBasic } from "./basic";
-import { run as runRandom } from "./random";
 import { rootCauses as TEST_CAUSES } from "./rootCauses";
 import { PORT, withServerOnPort } from "./serve";
 import { run as runVisual } from "./visual";
@@ -9,6 +9,8 @@ import { run as runVisual } from "./visual";
 declare global {
   var debugging: boolean;
   var testMatcher: string;
+  var outputFile: string;
+  var rankBy: string;
 }
 
 async function runForJson<T>(func: () => Promise<T>) {
@@ -16,11 +18,18 @@ async function runForJson<T>(func: () => Promise<T>) {
 }
 
 async function main() {
-  global.debugging = _.includes(process.argv, "--debug");
   const hasTestMatcher = _.find(process.argv, arg => arg.startsWith("--test="));
+  const hasOutputFile = _.find(process.argv, arg => arg.startsWith("--ofile="));
+  let hasRankBy = _.find(process.argv, arg => arg.startsWith("--rankBy="));
+
+  global.debugging = _.includes(process.argv, "--debug");
   global.testMatcher = hasTestMatcher
     ? hasTestMatcher.split("=")[1]
     : "[\\s\\S]*";
+  global.rankBy = hasRankBy ? hasRankBy.split("=")[1] : "inertia";
+  global.outputFile = hasOutputFile
+    ? hasOutputFile?.split("=")[1]
+    : `heuristic-precision[${global.rankBy}].csv`;
 
   const argv = _.filter(
     process.argv,
@@ -28,17 +37,10 @@ async function main() {
   );
 
   switch (argv[2]) {
-    case "-r": {
-      const N = Number(argv[3] ?? "10");
-      await withServerOnPort(PORT, () =>
-        runForJson(() => runRandom(N, TEST_CAUSES))
-      ).then(console.log);
-      break;
-    }
     case "-h": {
-      await withServerOnPort(PORT, () =>
-        runForJson(() => runBasic(TEST_CAUSES))
-      ).then(console.log);
+      await withServerOnPort(PORT, () => runBasic(TEST_CAUSES)).then(
+        writeToCSV(global.outputFile)
+      );
       break;
     }
     case "-s": {
@@ -54,6 +56,15 @@ async function main() {
   process.exit(0);
 }
 
+const writeToCSV = (filename: string) => (os: Object[]) => {
+  if (os.length === 0) return;
+
+  const names = Object.keys(os[0]).join(",");
+  const data = _.map(os, obj => _.map(_.values(obj), JSON.stringify).join(","));
+  const all = [names, ...data];
+  return fs.writeFileSync(filename, all.join("\n"));
+};
+
 main().catch(err => {
   console.error("Error running evaluation");
   console.error(err);
diff --git a/ide/packages/evaluation/src/page.ts b/ide/packages/evaluation/src/page.ts
index 960625a..f7ae460 100644
--- a/ide/packages/evaluation/src/page.ts
+++ b/ide/packages/evaluation/src/page.ts
@@ -6,6 +6,7 @@ import {
   type EvaluationMode,
   type Filename,
   type PanoptesConfig,
+  type SortStrategy,
   configToString
 } from "@argus/common/lib";
 import _ from "lodash";
@@ -741,13 +742,15 @@ export function webHtml(
   title: string,
   filename: Filename,
   bundles: BodyBundle[],
-  evalMode: EvaluationMode = "rank"
+  rankMode: SortStrategy,
+  evalMode: EvaluationMode = "evaluate"
 ) {
   const config: PanoptesConfig = {
     type: "WEB_BUNDLE",
     target: findErrorTargetInBundles(bundles),
     closedSystem: bundles,
-    evalMode
+    evalMode,
+    rankMode
   };
 
   const panoptesDir = path.resolve(__dirname, "..", "..", "panoptes");
diff --git a/ide/packages/evaluation/src/random.ts b/ide/packages/evaluation/src/random.ts
deleted file mode 100644
index ded0792..0000000
--- a/ide/packages/evaluation/src/random.ts
+++ /dev/null
@@ -1,95 +0,0 @@
-import path from "node:path";
-import type { BodyBundle } from "@argus/common/bindings";
-import _ from "lodash";
-import { chromium } from "playwright";
-
-import type { RootCause } from "./rootCauses";
-import {
-  argusData,
-  expandBottomUpView,
-  forFileInBundle,
-  openPage,
-  sleep,
-  testCases
-} from "./utils";
-
-async function createInnerRun(N: number) {
-  const workspaceDir = path.resolve(__dirname, "..", "workspaces");
-  const browser = await chromium.launch({ headless: !global.debugging });
-  const context = await browser.newContext();
-  context.setDefaultTimeout(5_000);
-
-  return async (workspace: string, causes: any[]) => {
-    const fullSubdir = path.resolve(workspaceDir, workspace);
-    const argusBundles = await argusData(fullSubdir);
-
-    if (!("Ok" in argusBundles)) throw new Error("Argus failed");
-    const fileBundles = (await forFileInBundle(
-      argusBundles.Ok,
-      async (filename, bundles) => [filename, bundles]
-    )) as [string, BodyBundle[]][];
-
-    let results = [];
-    for (const [filename, bundles] of fileBundles) {
-      const cause = _.find(causes, cause => filename.endsWith(cause.file));
-
-      if (!cause) {
-        console.error(`No cause found for ${filename} in ${workspace}`);
-        continue;
-      }
-
-      console.debug(`Running ${N} samples for ${filename}`);
-      let ranks = await Promise.all(
-        _.times(N, async () => {
-          const page = await openPage(context, filename, bundles, "random");
-          await sleep(3000);
-          await expandBottomUpView(page);
-          await sleep(3000);
-          try {
-            const goals = await page
-              .locator(".BottomUpArea .EvalGoal")
-              .filter({ hasText: cause.message })
-              .all();
-
-            const ranksStr = await Promise.all(
-              _.map(goals, goal => goal.getAttribute("data-rank"))
-            );
-
-            return _.min(_.map(_.compact(ranksStr), r => Number(r)));
-          } catch (e) {
-            return undefined;
-          } finally {
-            await page.close();
-          }
-        })
-      );
-
-      const noUndef = _.compact(ranks);
-      if (noUndef.length === 0) {
-        console.error(`No ranks found for ${filename} in ${workspace}`);
-      }
-
-      results.push({
-        workspace,
-        filename,
-        cause: cause.message,
-        ranks: noUndef
-      });
-    }
-
-    return results;
-  };
-}
-
-export async function run(N: number, rootCauses: RootCause[]) {
-  const innerF = await createInnerRun(N);
-  const tcs = testCases();
-
-  let results = [];
-  for (const { workspace, causes } of rootCauses) {
-    if (!_.includes(tcs, workspace)) continue;
-    results.push(await innerF(workspace, causes));
-  }
-
-  return _.flatten(results);
-}
diff --git a/ide/packages/evaluation/src/rootCauses.ts b/ide/packages/evaluation/src/rootCauses.ts
index 2326343..be9201f 100644
--- a/ide/packages/evaluation/src/rootCauses.ts
+++ b/ide/packages/evaluation/src/rootCauses.ts
@@ -47,7 +47,7 @@ export const rootCauses: RootCause[] = [
       },
       {
         file: "extract_self_ref.rs",
-        message: "&'_ A: FromRequestParts"
+        message: "&A: FromRequestParts"
       },
       {
         file: "missing_deserialize.rs",
@@ -71,7 +71,8 @@ export const rootCauses: RootCause[] = [
       },
       {
         file: "too_many_extractors.rs",
-        message: ": FnOnce<(_, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _)>"
+        // NOTE: HACK: the commas are added by CSS, so we don't need them here.
+        message: ": FnOnce<(________________)>"
       },
       {
         file: "wrong_return_type.rs",
diff --git a/ide/packages/evaluation/src/utils.ts b/ide/packages/evaluation/src/utils.ts
index 5f89ffb..5b84622 100644
--- a/ide/packages/evaluation/src/utils.ts
+++ b/ide/packages/evaluation/src/utils.ts
@@ -1,6 +1,6 @@
 import fs from "node:fs";
 import type { BodyBundle } from "@argus/common/bindings";
-import type { EvaluationMode, Filename, Result } from "@argus/common/lib";
+import type { Filename, Result, SortStrategy } from "@argus/common/lib";
 import { type ExecNotifyOpts, execNotify as _execNotify } from "@argus/system";
 import _ from "lodash";
 import type { BrowserContext, Page } from "playwright";
@@ -35,7 +35,8 @@ export function testCases() {
     "axum",
     "bevy",
     "diesel",
-    "easy_ml",
+    // "easy_ml",
+    // "chumsky",
     "entrait",
     "nalgebra",
     "uom"
@@ -89,14 +90,21 @@ export async function forFileInBundle<T>(
   );
 }
 
+function sanitizeSort(s: string | undefined): s is SortStrategy {
+  return s !== undefined && (s === "inertia" || s === "depth" || s === "vars");
+}
+
 export async function openPage(
   context: BrowserContext,
   filename: string,
-  bundles: BodyBundle[],
-  evalMode: EvaluationMode
+  bundles: BodyBundle[]
 ) {
+  if (!sanitizeSort(global.rankBy)) {
+    throw new Error(`Invalid rank mode: ${global.rankBy}`);
+  }
+
   const tmpobj = tmp.fileSync({ postfix: ".html" });
-  const html = webHtml("EVAL", filename, bundles, evalMode);
+  const html = webHtml("EVAL", filename, bundles, global.rankBy, "evaluate");
   fs.writeSync(tmpobj.fd, html);
   const page = await context.newPage();
   await page.goto(`file://${tmpobj.name}`, {
diff --git a/ide/packages/evaluation/src/visual.ts b/ide/packages/evaluation/src/visual.ts
index 9bcebc6..e2f33d7 100644
--- a/ide/packages/evaluation/src/visual.ts
+++ b/ide/packages/evaluation/src/visual.ts
@@ -38,7 +38,7 @@ async function argusScreenshots(
     filename: Filename,
     bundles: BodyBundle[]
   ) => {
-    const page = await openPage(context, filename, bundles, "rank");
+    const page = await openPage(context, filename, bundles);
     await expandBottomUpView(page);
     await page.screenshot({ path: out, fullPage: true });
   };
diff --git a/ide/packages/panoptes/src/App.tsx b/ide/packages/panoptes/src/App.tsx
index b51c1e9..c92746a 100644
--- a/ide/packages/panoptes/src/App.tsx
+++ b/ide/packages/panoptes/src/App.tsx
@@ -9,7 +9,6 @@ import {
   settingsToggles
 } from "@argus/common/context";
 import {
-  type EvaluationMode,
   type FileInfo,
   type PanoptesConfig,
   type SystemSpec,
@@ -245,8 +244,9 @@ const App = observer(({ config }: { config: PanoptesConfig }) => {
     config.type === "VSCODE_BACKING" ? config.spec : webSysSpec;
 
   config.evalMode = config.evalMode ?? "release";
-  const configNoUndef: PanoptesConfig & { evalMode: EvaluationMode } =
-    config as any;
+  config.rankMode = config.rankMode ?? "inertia";
+
+  const configNoUndef: Required<PanoptesConfig> = config as any;
 
   useEffect(() => {
     const listen = (e: MessageEvent) =>
diff --git a/ide/packages/panoptes/src/TreeView/BottomUp.tsx b/ide/packages/panoptes/src/TreeView/BottomUp.tsx
index dc0e2e4..a7d7536 100644
--- a/ide/packages/panoptes/src/TreeView/BottomUp.tsx
+++ b/ide/packages/panoptes/src/TreeView/BottomUp.tsx
@@ -1,4 +1,3 @@
-import type { EvaluationMode } from "@argus/common/lib";
 import { PrintGoal } from "@argus/print/lib";
 import React, { useContext, useState } from "react";
 import { flushSync } from "react-dom";
@@ -23,6 +22,7 @@ import { WrapImplCandidates, mkJumpToTopDownWrapper } from "./Wrappers";
 
 import { CollapsibleElement, DirRecursive } from "./Directory";
 import "./BottomUp.css";
+import { TyCtxt } from "@argus/print/context";
 
 const RenderEvaluationViews = ({
   recommended,
@@ -31,8 +31,11 @@ const RenderEvaluationViews = ({
 }: {
   recommended: TreeViewWithRoot[];
   others: TreeViewWithRoot[];
-  mode: "rank" | "random";
+  mode: "evaluate";
 }) => {
+  const tree = useContext(TreeAppContext.TreeContext)!;
+  const tyCtxt = useContext(TyCtxt)!;
+
   const nodeToString = (node: React.ReactNode) => {
     const div = document.createElement("div");
     const root = createRoot(div);
@@ -40,19 +43,16 @@ const RenderEvaluationViews = ({
     return div.innerText;
   };
 
-  const tree = useContext(TreeAppContext.TreeContext)!;
   let together = _.concat(recommended, others);
 
-  if (mode === "random") {
-    together = _.shuffle(together);
-  }
-
   const [goals, setGoals] = React.useState<string[]>([]);
   const nodeList: React.ReactNode[] = _.compact(
     _.map(together, (leaf, i) => {
       const node = tree.node(leaf.root);
       return "Goal" in node ? (
-        <PrintGoal key={i} o={tree.goal(node.Goal)} />
+        <TyCtxt.Provider value={tyCtxt} key={i}>
+          <PrintGoal o={tree.goal(node.Goal)} />
+        </TyCtxt.Provider>
       ) : null;
     })
   );
@@ -120,27 +120,6 @@ export function liftTo(
   return curr;
 }
 
-// A bit of a hack to allow the evaluation script to render the bottom up view differently.
-export const BottomUpImpersonator = ({
-  recommended,
-  others,
-  mode
-}: {
-  recommended: TreeViewWithRoot[];
-  others: TreeViewWithRoot[];
-  mode: EvaluationMode;
-}) => {
-  return mode === "release" ? (
-    <RenderBottomUpViews recommended={recommended} others={others} />
-  ) : (
-    <RenderEvaluationViews
-      recommended={recommended}
-      others={others}
-      mode={mode}
-    />
-  );
-};
-
 export const sortedSubsets = (sets: SetHeuristic[]) =>
   _.sortBy(sets, TreeInfo.setInertia);
 
@@ -253,9 +232,11 @@ const BottomUp = ({
   jumpToTopDown
 }: { jumpToTopDown: (n: ProofNodeIdx) => void }) => {
   const tree = useContext(TreeAppContext.TreeContext)!;
-  const evaluationMode =
-    useContext(AppContext.ConfigurationContext)?.evalMode ?? "release";
-  const sets = sortedSubsets(tree.failedSets());
+  const cfg = useContext(AppContext.ConfigurationContext)!;
+  const evaluationMode = cfg.evalMode ?? "release";
+  const rankMode = cfg.rankMode ?? "inertia";
+
+  const sets = tree.failedSetsSorted(rankMode);
 
   const makeSets = (sets: SetHeuristic[]) =>
     _.map(sets, h => {
@@ -286,7 +267,7 @@ const BottomUp = ({
   const suggestedPredicates = flattenSets(_.slice(sets, 0, 3));
   const others = flattenSets(_.slice(sets, 3));
   return (
-    <BottomUpImpersonator
+    <RenderEvaluationViews
       recommended={suggestedPredicates}
       others={others}
       mode={evaluationMode}
diff --git a/ide/packages/panoptes/src/TreeView/Erotisi.tsx b/ide/packages/panoptes/src/TreeView/Erotisi.tsx
index 312b384..0e75c3f 100644
--- a/ide/packages/panoptes/src/TreeView/Erotisi.tsx
+++ b/ide/packages/panoptes/src/TreeView/Erotisi.tsx
@@ -7,8 +7,6 @@ import ReportBugUrl from "@argus/print/ReportBugUrl";
 import { VSCodeButton } from "@vscode/webview-ui-toolkit/react";
 import _ from "lodash";
 import React, { useContext, useState } from "react";
-
-import { sortedSubsets } from "./BottomUp";
 import { Node } from "./Node";
 
 type Target =
@@ -83,8 +81,7 @@ function formOptions(
 
 const Erotisi = () => {
   const tree = useContext(TreeAppContext.TreeContext)!;
-  const sets = sortedSubsets(tree.failedSets());
-  if (sets.length === 0) {
+  if (tree.numFailedSets() <= 0) {
     return (
       <ErrorDiv>
         <p>
@@ -99,6 +96,7 @@ const Erotisi = () => {
     );
   }
 
+  const sets = tree.failedSetsSorted();
   const firstForm = formOptions(tree, sets, []);
   const [currentPanel, setCurrentPanel] = useState<MaybeProp>(firstForm);
 
diff --git a/ide/packages/panoptes/src/TreeView/TreeApp.tsx b/ide/packages/panoptes/src/TreeView/TreeApp.tsx
index 0341ec3..1e6d991 100644
--- a/ide/packages/panoptes/src/TreeView/TreeApp.tsx
+++ b/ide/packages/panoptes/src/TreeView/TreeApp.tsx
@@ -55,7 +55,7 @@ const TreeApp = ({
     }
   ];
 
-  if (treeInfo.failedSets().length > 0) {
+  if (0 < treeInfo.numFailedSets()) {
     // Unshift to place this first
     // NOTE: the passing the TopDown panel ID is important, make sure it's always correct.
     // FIXME: we probably shouldn't hard-code that value here...
diff --git a/ide/packages/panoptes/src/TreeView/heuristic.ts b/ide/packages/panoptes/src/TreeView/heuristic.ts
deleted file mode 100644
index c476e79..0000000
--- a/ide/packages/panoptes/src/TreeView/heuristic.ts
+++ /dev/null
@@ -1,268 +0,0 @@
-import type TreeInfo from "@argus/common/TreeInfo";
-import type { ProofNodeIdx } from "@argus/common/bindings";
-import { isTraitClause, mean, stdDev } from "@argus/common/func";
-import _ from "lodash";
-
-interface HeuristicI {
-  // Partition sets of failed nodes into two groups.
-  partition(
-    groups: _.Dictionary<ProofNodeIdx[]>
-  ): [ProofNodeIdx[], ProofNodeIdx[]];
-
-  rank<T>(data: T[], f: (t: T) => ProofNodeIdx): T[];
-}
-
-export function treeHeuristic(tree: TreeInfo): HeuristicI {
-  return new Heuristic(tree);
-}
-
-type Strategy = {
-  size: number;
-  sorter: (group: ProofNodeIdx[]) => number;
-  partitioner: (n: number) => <T>(groups: T[]) => [T[], T[]];
-};
-
-type PartitionTup<T> = [T[], T[]];
-function takeN(n: number) {
-  return <T>(groups: T[]): PartitionTup<T> => [
-    _.slice(groups, 0, n),
-    _.slice(groups, n)
-  ];
-}
-
-function takeAll<T>(groups: T[]) {
-  return takeN(groups.length)(groups);
-}
-
-class Heuristic implements HeuristicI {
-  public constructor(readonly tree: TreeInfo) {}
-
-  numMainUninferred(group: ProofNodeIdx[]) {
-    return _.reduce(
-      group,
-      (acc, leaf) =>
-        acc +
-        (() => {
-          const node = this.tree.node(leaf);
-          if ("Goal" in node) {
-            const goal = this.tree.goal(node.Goal);
-            return goal.isMainTv ? 1 : 0;
-          }
-          return 0;
-        })(),
-      0
-    );
-  }
-
-  numPrincipled(group: ProofNodeIdx[]) {
-    return group.length - this.numMainUninferred(group);
-  }
-
-  maxDepth(group: ProofNodeIdx[]) {
-    return _.max(_.map(group, leaf => this.tree.depth(leaf)))!;
-  }
-
-  numOutliers<T>(group: T[], f: (g: T) => number) {
-    const data = _.map(group, f);
-    const meanD = mean(data);
-    const stdDevD = stdDev(data, meanD);
-    return _.filter(data, d => d > meanD + stdDevD).length;
-  }
-
-  sortByNPT() {
-    return (group: ProofNodeIdx[]) => -this.numPrincipled(group);
-  }
-
-  sortByNPTRatio() {
-    return (group: ProofNodeIdx[]) => group.length / this.numPrincipled(group);
-  }
-
-  sortByDepth() {
-    return (group: ProofNodeIdx[]) =>
-      -_.max(_.map(group, leaf => this.tree.depth(leaf)))!;
-  }
-
-  // ----------------------
-  // Partitioning Algorithm
-
-  // NOTE: partitioning with heuristics can alsways be improved.
-  partition(
-    failedGroups: _.Dictionary<ProofNodeIdx[]>
-  ): PartitionTup<ProofNodeIdx> {
-    // Getting the right group is important but it's not precise.
-    // We currently use the following metrics.
-    //
-    // 1. Depth of the group. Generally, deep obligations are "more interesting."
-    //
-    // 2. The number of obligations whose "principle types" are known (NPT).
-    //    What this entails is that in an obligation such as `TYPE: TRAIT`,
-    //    neither TYPE nor TRAIT is an unresolved type variable `_`.
-    //
-    //    We use this number, NPT, to find groups whose NPT is more than
-    //    one standard deviation from the mean. This is useful when trait impls are
-    //    macro generated for varying arities, larger arities have a high number of
-    //    unresolved type variables.
-    //
-    // 3. The NPT is useful, until it isn't. We use the ratio of group size by
-    //    NPT to favor smaller groups with more concrete types.
-    const failedValues = _.values(failedGroups);
-    const strategies: Strategy[] = [
-      {
-        size: this.numOutliers(failedValues, g => this.maxDepth(g)),
-        sorter: this.sortByDepth(),
-        partitioner: takeN
-      },
-      {
-        size: this.numOutliers(failedValues, g => this.numPrincipled(g)),
-        sorter: this.sortByNPT(),
-        partitioner: takeN
-      },
-      {
-        size: this.numOutliers(
-          failedValues,
-          group => group.length / this.numPrincipled(group)
-        ),
-        sorter: this.sortByNPTRatio(),
-        partitioner: takeN
-      }
-    ];
-
-    const sortedAndPartitioned = _.map(strategies, s =>
-      this.applyStrategy(failedValues, s)
-    );
-
-    // Combine all strategies to get the final partition.
-    const [importantGroupsNonUnq, restNonUnq] = _.reduce(
-      sortedAndPartitioned,
-      ([accImp, accRest], [imp, rest]) => [
-        _.concat(accImp, _.flatten(imp)),
-        _.concat(accRest, _.flatten(rest))
-      ],
-      [[], []] as PartitionTup<ProofNodeIdx>
-    );
-
-    const [importantGroups, restWithDups] = [
-      _.uniq(importantGroupsNonUnq),
-      _.uniq(restNonUnq)
-    ];
-
-    // Remove recommended nodes from the hidden nodes, this can happen if
-    // one sort strategy recommends one while another doesn't.
-    const rest = _.difference(restWithDups, importantGroups);
-
-    // The "Argus recommended" errors are shown expanded, and the
-    // "others" are collapsed. Argus recommended errors are the ones
-    // that failed or are ambiguous with a concrete type on the LHS.
-    const [argusRecommendedLeaves, others] =
-      this.partitionSingles(importantGroups);
-
-    // Fallback to sorting by depth and showing everything. This, of course, is a HACK.
-    if (argusRecommendedLeaves.length === 0) {
-      return this.partitionDefault(failedValues);
-    }
-
-    const hiddenLeaves = _.concat(rest, others);
-    return [argusRecommendedLeaves, hiddenLeaves];
-  }
-
-  applyStrategy(
-    groups: ProofNodeIdx[][],
-    { size, sorter, partitioner }: Strategy
-  ) {
-    return size > 0
-      ? partitioner(size)(_.sortBy(groups, sorter))
-      : ([[], []] as PartitionTup<ProofNodeIdx>);
-  }
-
-  partitionSingles(group: ProofNodeIdx[]) {
-    return _.partition(group, leaf => {
-      const node = this.tree.node(leaf);
-      if ("Goal" in node) {
-        const goal = this.tree.goal(node.Goal);
-        const result = this.tree.result(goal.result);
-        return (
-          !goal.isMainTv && (result === "no" || result === "maybe-overflow")
-        );
-      }
-      // Leaves should only be goals...
-      throw new Error(`Leaves should only be goals ${node}`);
-    });
-  }
-
-  partitionDefault(failedGroups: ProofNodeIdx[][]) {
-    const defaultStrategy = {
-      size: failedGroups.length,
-      sorter: this.sortByDepth(),
-      partitioner: (_: any) => takeAll
-    };
-    const [important, hiddenLeaves] = this.applyStrategy(
-      failedGroups,
-      defaultStrategy
-    );
-    const [argusRecommendedLeaves, others] = this.partitionSingles(
-      _.flatten(important)
-    );
-    return [
-      argusRecommendedLeaves,
-      _.concat(_.flatten(hiddenLeaves), others)
-    ] as PartitionTup<ProofNodeIdx>;
-  }
-
-  // -------------------------
-  // Sort a list of flat nodes
-
-  rank<T>(data: T[], f: (t: T) => ProofNodeIdx) {
-    const sortErrorsFirst = (t: T) => {
-      const leaf = f(t);
-      switch (this.tree.nodeResult(leaf)) {
-        case "no":
-          return 0;
-        case "maybe-overflow":
-        case "maybe-ambiguity":
-          return 1;
-        case "yes":
-          return 2;
-      }
-    };
-
-    const sortWeightPaths = (t: T) => {
-      const leaf = f(t);
-      const pathToRoot = this.tree.pathToRoot(leaf);
-      const len = pathToRoot.length;
-      const numVars = _.reduce(
-        pathToRoot.pathInclusive,
-        (sum, k) => sum + this.tree.inferVars(k),
-        0
-      );
-
-      return numVars / len;
-    };
-
-    const bubbleTraitClauses = (t: T) => {
-      const leaf = f(t);
-      const n = this.tree.node(leaf);
-      if (
-        "Goal" in n &&
-        isTraitClause(this.tree.goal(n.Goal).value.predicate)
-      ) {
-        return 0;
-      }
-      return 1;
-    };
-
-    const recommendedOrder = _.sortBy(data, [
-      sortErrorsFirst,
-      bubbleTraitClauses,
-      sortWeightPaths
-    ]);
-
-    return recommendedOrder;
-  }
-
-  errorLeavesInSimpleRecommendedOrder() {
-    const errorLeaves = _.flatMap(this.tree.failedSets(), g =>
-      _.map(g.goals, g => g.idx)
-    );
-    return this.rank(errorLeaves, _.identity);
-  }
-}
diff --git a/ide/pnpm-lock.yaml b/ide/pnpm-lock.yaml
index 009f540..a503784 100644
--- a/ide/pnpm-lock.yaml
+++ b/ide/pnpm-lock.yaml
@@ -78,8 +78,8 @@ importers:
         specifier: ^4.17.21
         version: 4.17.21
       playwright:
-        specifier: ^1.42.1
-        version: 1.42.1
+        specifier: 1.40.0
+        version: 1.40.0
       tmp:
         specifier: ^0.2.3
         version: 0.2.3
@@ -1811,11 +1811,21 @@ packages:
   pkg-types@1.0.3:
     resolution: {integrity: sha512-nN7pYi0AQqJnoLPC9eHFQ8AcyaixBUOwvqc5TDnIKCMEE6I0y8P7OKA7fPexsXGCGxQDl/cmrLAp26LhcwxZ4A==}
 
+  playwright-core@1.40.0:
+    resolution: {integrity: sha512-fvKewVJpGeca8t0ipM56jkVSU6Eo0RmFvQ/MaCQNDYm+sdvKkMBBWTE1FdeMqIdumRaXXjZChWHvIzCGM/tA/Q==}
+    engines: {node: '>=16'}
+    hasBin: true
+
   playwright-core@1.42.1:
     resolution: {integrity: sha512-mxz6zclokgrke9p1vtdy/COWBH+eOZgYUVVU34C73M+4j4HLlQJHtfcqiqqxpP0o8HhMkflvfbquLX5dg6wlfA==}
     engines: {node: '>=16'}
     hasBin: true
 
+  playwright@1.40.0:
+    resolution: {integrity: sha512-gyHAgQjiDf1m34Xpwzaqb76KgfzYrhK7iih+2IzcOCoZWr/8ZqmdBw+t0RU85ZmfJMgtgAiNtBQ/KS2325INXw==}
+    engines: {node: '>=16'}
+    hasBin: true
+
   playwright@1.42.1:
     resolution: {integrity: sha512-PgwB03s2DZBcNRoW+1w9E+VkLBxweib6KTXM0M3tkiT4jVxKSi6PmVJ591J+0u10LUrgxB7dLRbiJqO5s2QPMg==}
     engines: {node: '>=16'}
@@ -3955,13 +3965,23 @@ snapshots:
       mlly: 1.4.2
       pathe: 1.1.1
 
-  playwright-core@1.42.1: {}
+  playwright-core@1.40.0: {}
+
+  playwright-core@1.42.1:
+    optional: true
+
+  playwright@1.40.0:
+    dependencies:
+      playwright-core: 1.40.0
+    optionalDependencies:
+      fsevents: 2.3.2
 
   playwright@1.42.1:
     dependencies:
       playwright-core: 1.42.1
     optionalDependencies:
       fsevents: 2.3.2
+    optional: true
 
   postcss@8.4.31:
     dependencies: