chore: make workspaceSymbol benchmarks modules (#11094)

This PR makes workspaceSymbol benchmarks `module`s, so that they are
less sensitive to additions of private symbols in the standard library.

tests/bench/speedcenter.exec.velcom.yaml

@@ -486,7 +486,7 @@
     tags: [other]
   run_config:
     <<: *time
-    cmd: lean workspaceSymbols.lean
+    cmd: lean -Dexperimental.module=true workspaceSymbols.lean
     max_runs: 2
 - attributes:
     description: bv_decide_realworld

tests/bench/workspaceSymbols.lean

@@ -1,4 +1,6 @@
+module
 import Lean
+meta import Lean.Data.FuzzyMatching
 open Lean Elab
 
 def bench (pattern : String) : TermElabM Unit := do

tests/bench/workspaceSymbolsNewRanges.lean

@@ -17,7 +17,9 @@ Because interpretation of the fuzzy matching algorithm is prohibitively slow, we
 just use `TermElabM` to extract the list of symbols from the environment.
 -/
 
-import Lean.Elab.Term
+module
+public import Lean.Elab.Term
+meta import Lean.Elab.Term.TermElabM
 
 @[specialize] private def iterateLookaround (f : (Option Char × Char × Option Char) → α) (string : String) : Array α :=
   if string.isEmpty then
@@ -250,7 +252,7 @@ def fuzzyMatch (pattern word : String) (threshold := 0.2) : Bool :=
 -- The constants have been generated using the following code.
 open Lean Elab Term Meta
 
-def getConsts : MetaM (List Name) := do
+meta def getConsts : MetaM (List Name) := do
   let env ← getEnv
   return env.constants.toList.map (·.1)
 
@@ -1268,7 +1270,7 @@ def bench (pattern : String) : IO Unit := do
     if fuzzyMatch pattern c then n := n + 1
   IO.println s!"{n} matches"
 
-def main : IO Unit := do
+public def main : IO Unit := do
   bench "L"
   bench "Lean."
   bench "Lean.Expr"

tests/common.sh

@@ -25,7 +25,7 @@ function lean_has_llvm_support {
 }
 
 function compile_lean_c_backend {
-    lean --c="$f.c" "$f" || fail "Failed to compile $f into C file"
+    lean -Dexperimental.module=true --c="$f.c" "$f" || fail "Failed to compile $f into C file"
     leanc ${LEANC_OPTS-} -O3 -DNDEBUG -o "$f.out" "$@" "$f.c" || fail "Failed to compile C file $f.c"
 }
 
@@ -34,7 +34,7 @@ function compile_lean_llvm_backend {
     rm "*.ll" || true # remove debugging files.
     rm "*.bc" || true # remove bitcode files
     rm "*.o" || true # remove object files
-    lean --bc="$f.linked.bc" "$f" || fail "Failed to compile $f into bitcode file"
+    lean -Dexperimental.module=true --bc="$f.linked.bc" "$f" || fail "Failed to compile $f into bitcode file"
     leanc ${LEANC_OPTS-} -O3 -DNDEBUG -o "$f.out" "$@" "$f.linked.bc" || fail "Failed to link object file '$f.linked.bc'"
     set +o xtrace
 }