Skip to content

Commit

Permalink
test: benchmark workspace symbols search
Browse files Browse the repository at this point in the history
  • Loading branch information
Kha committed Oct 13, 2022
1 parent ac9d65b commit 6b8fa76
Show file tree
Hide file tree
Showing 2 changed files with 22 additions and 0 deletions.
6 changes: 6 additions & 0 deletions tests/bench/speedcenter.exec.velcom.yaml
Expand Up @@ -160,3 +160,9 @@
cmd: ./unionfind.lean.out 3000000
build_config:
cmd: ./compile.sh unionfind.lean
- attributes:
description: workspaceSymbols
tags: [fast, suite]
run_config:
<<: *time
cmd: lean workspaceSymbols.lean
16 changes: 16 additions & 0 deletions tests/bench/workspaceSymbols.lean
@@ -0,0 +1,16 @@
import Lean
open Lean Elab

def bench (pattern : String) : TermElabM Unit := do
let env ← getEnv
let mut n := 0
IO.println s!"{env.constants.size} decls"
for (c, _) in env.constants.toList do
if Lean.FuzzyMatching.fuzzyMatch pattern c.toString then n := n + 1
IO.println s!"{n} matches"

set_option profiler true
#eval bench "L"
#eval bench "Lean."
#eval bench "Lean.Expr"
#eval bench "Lean.Expr.const"

0 comments on commit 6b8fa76

Please sign in to comment.