diff --git a/tests/bench/Makefile b/tests/bench/Makefile index 45ce06d7f3..545abb475a 100644 --- a/tests/bench/Makefile +++ b/tests/bench/Makefile @@ -26,7 +26,7 @@ MLTON_BIN ?= /usr/bin MLKIT ?= mlkit SWIFTC ?= swiftc -PARSER_TEST_FILE ?= ../../src/Init/Core.lean +PARSER_TEST_FILE ?= ../../src/Init/Prelude.lean ## IMPLEMENTATION @@ -103,7 +103,7 @@ bench: bench/%.bench: %.out | bench ulimit -s unlimited && $(TEMCI) short exec $(TEMCI_FLAGS) -d $< "./$< $(BENCH_PARAMS)" --out $@ -bench/parser.%.bench: BENCH_PARAMS = $(PARSER_TEST_FILE) 10 +bench/parser.%.bench: BENCH_PARAMS = $(PARSER_TEST_FILE) 50 bench/binarytrees.%.bench: BENCH_PARAMS = 21 bench/binarytrees.ml.bench: BENCH_PARAMS = $$(nproc) 21 diff --git a/tests/bench/parser.lean b/tests/bench/parser.lean index de4a6ea7f5..9d6807bddd 100644 --- a/tests/bench/parser.lean +++ b/tests/bench/parser.lean @@ -1,8 +1,12 @@ import Lean.Parser.Module +/-! + Test parsing only on a .lean file, which necessarily has to be one that does + not depend on non-built-in syntax, e.g. `Init.Prelude`. -/ + def main : List String → IO Unit | [fname, n] => do let env ← Lean.mkEmptyEnvironment for _ in [0:n.toNat!] do discard $ Lean.Parser.testParseFile env fname -| _ => throw $ IO.userError "give file" +| _ => throw $ IO.userError "give file and iteration count" diff --git a/tests/bench/speedcenter.exec.velcom.yaml b/tests/bench/speedcenter.exec.velcom.yaml index 6e8cf8baeb..c9249d96ad 100644 --- a/tests/bench/speedcenter.exec.velcom.yaml +++ b/tests/bench/speedcenter.exec.velcom.yaml @@ -112,6 +112,14 @@ cmd: ./liasolver.lean.out ex-50-50-1.leq build_config: cmd: ./compile.sh liasolver.lean +- attributes: + description: parser + tags: [fast, suite] + run_config: + <<: *time + cmd: ./parser.lean.out ../../src/Init/Prelude.lean 50 + build_config: + cmd: ./compile.sh parser.lean - attributes: description: qsort tags: [fast, suite] @@ -144,14 +152,6 @@ cmd: ./rbmap_checkpoint.lean.out 2000000 10 build_config: cmd: ./compile.sh rbmap_checkpoint.lean -- attributes: - description: rbmap_library - tags: [fast, suite] - run_config: - <<: *time - cmd: ./rbmap_library.lean.out 2000000 - build_config: - cmd: ./compile.sh rbmap_library.lean - attributes: description: rbmap_fbip tags: [fast, suite] @@ -160,6 +160,14 @@ cmd: ./rbmap_fbip.lean.out 2000000 build_config: cmd: ./compile.sh rbmap_fbip.lean +- attributes: + description: rbmap_library + tags: [fast, suite] + run_config: + <<: *time + cmd: ./rbmap_library.lean.out 2000000 + build_config: + cmd: ./compile.sh rbmap_library.lean - attributes: description: unionfind tags: [fast, suite]