test: update parser benchmark, add to speedcenter suite

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

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"

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]