diff --git a/tests/bench/speedcenter.exec.velcom.yaml b/tests/bench/speedcenter.exec.velcom.yaml index dc5cb8f4af..31c473af20 100644 --- a/tests/bench/speedcenter.exec.velcom.yaml +++ b/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 diff --git a/tests/bench/workspaceSymbols.lean b/tests/bench/workspaceSymbols.lean index 8612cce112..06f6892fe6 100644 --- a/tests/bench/workspaceSymbols.lean +++ b/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 diff --git a/tests/bench/workspaceSymbolsNewRanges.lean b/tests/bench/workspaceSymbolsNewRanges.lean index 1e56fa2db7..77e52e1b06 100644 --- a/tests/bench/workspaceSymbolsNewRanges.lean +++ b/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" diff --git a/tests/common.sh b/tests/common.sh index a5759abe14..52756c06f3 100644 --- a/tests/common.sh +++ b/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 }