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`.
This commit is contained in:
Cameron Zwarich 2025-06-16 22:01:12 -07:00 committed by GitHub
parent 471553102c
commit c9d0af1d7e
No known key found for this signature in database
GPG key ID: B5690EEEBB952194

View file

@ -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)