From c9d0af1d7e95ab3152bc9b83706cca5494733266 Mon Sep 17 00:00:00 2001
From: Cameron Zwarich <cameron@lean-fro.org>
Date: Mon, 16 Jun 2025 22:01:12 -0700
Subject: [PATCH] chore: delete tests/lean/run/CompilerProbe.lean (#8833)

This test is essentially disabled on `master`, because it prints
nothing. With the new compiler enabled, it prints names of functions
throughout the Lean codebase satisfying certain conditions. Even just
maintaining this on the new compiler branch got old pretty quickly, so I
can't imagine we'd ever want to deal with this on `master`.
---
 tests/lean/run/CompilerProbe.lean | 49 -------------------------------
 1 file changed, 49 deletions(-)
 delete mode 100644 tests/lean/run/CompilerProbe.lean

diff --git a/tests/lean/run/CompilerProbe.lean b/tests/lean/run/CompilerProbe.lean
deleted file mode 100644
index 5fc496b688..0000000000
--- a/tests/lean/run/CompilerProbe.lean
+++ /dev/null
@@ -1,49 +0,0 @@
-import Lean
-import Lean.Compiler.LCNF.Probing
-open Lean.Compiler.LCNF
-
--- Note: 2024-05-15: At the time of adding #guard_msgs here, the tests seem to all be failing.
-
--- Find functions that have jps which take a lambda
-/-- info: #[] -/
-#guard_msgs in
-#eval
-  Probe.runGlobally (phase := .mono) <|
-  Probe.filterByJp (·.params.anyM (fun param => return param.type.isForall)) >=>
-  Probe.declNames >=>
-  Probe.toString
-
--- Count lambda lifted functions
-def lambdaCounter : Probe Decl Nat :=
-  Probe.filter (fun decl =>
-    if let .str _ val := decl.name then
-      return val.startsWith "_lam"
-    else
-      return false) >=>
-  Probe.declNames >=>
-  Probe.count
-
--- Run everywhere
-/-- info: #[0] -/
-#guard_msgs in
-#eval
-  Probe.runGlobally (phase := .mono) <|
-  lambdaCounter
-
--- Run limited
-/-- info: #[0] -/
-#guard_msgs in
-#eval
-  Probe.runOnModule `Lean.Compiler.LCNF.JoinPoints (phase := .mono) <|
-  lambdaCounter
-
--- Find most commonly used function with threshold
-/-- info: #[] -/
-#guard_msgs in
-#eval
-  Probe.runOnModule `Lean.Compiler.LCNF.JoinPoints (phase := .mono) <|
-  Probe.getLetValues >=>
-  Probe.filter (fun e => return e matches .const ..) >=>
-  Probe.map (fun | .const declName .. => return s!"{declName}" | _ => unreachable!) >=>
-  Probe.countUniqueSorted >=>
-  Probe.filter (fun (_, count) => return count > 100)