lean4-htt/tests
Leonardo de Moura aa95a1c03f
chore: cleaunp grind tests (#6616)
Tests using `logInfo` were taking an additional two seconds on my
machine. This is a performance issue with the old code generator, where
we spend all this time specializing the logging functions for `GoalM`. I
have not checked whether the new code generator is also affected by this
performance issue.

Here is a small example that exposes the issue:
```lean
import Lean

set_option profiler true
open Lean Meta Grind in
def test (e : Expr): GoalM Unit := do
  logInfo e
```

cc @zwarich
2025-01-13 00:07:48 +00:00
..
bench
compiler
elabissues
ir
lean chore: cleaunp grind tests (#6616) 2025-01-13 00:07:48 +00:00
pkg
playground
plugin
simpperf
.gitignore
common.sh
lean-toolchain