From 1add44916cf8ca3f3b5eafbb66bc8d9b868fb1b3 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Fri, 13 Nov 2020 19:57:06 +0100
Subject: [PATCH] chore: remove broken & redundant "new parser Core.lean"
 benchmark

---
 src/CMakeLists.txt                       | 4 ++--
 tests/bench/parser.lean                  | 8 --------
 tests/bench/speedcenter.exec.velcom.yaml | 8 --------
 3 files changed, 2 insertions(+), 18 deletions(-)
 delete mode 100644 tests/bench/parser.lean

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 16404b7bef..6a26bafba7 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -314,9 +314,9 @@ include_directories(${CMAKE_BINARY_DIR}/include)
 # libleancpp and the stdlib libraries are cyclically dependent. This works by default on macOS, which also doesn't like
 # the linker flags necessary on other platforms.
 if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
-  set(LEANC_STATIC_LINKER_FLAGS "-lleancpp" "-lInit" "-lStd" "-lLean")
+  set(LEANC_STATIC_LINKER_FLAGS "-lleancpp -lInit -lStd -lLean")
 else()
-  set(LEANC_STATIC_LINKER_FLAGS "-Wl,--start-group" "-lleancpp" "-lInit" "-lStd" "-lLean" "-Wl,--end-group")
+  set(LEANC_STATIC_LINKER_FLAGS "-Wl,--start-group -lleancpp -lInit -lStd -lLean -Wl,--end-group")
 endif()
 
 if(${CMAKE_SYSTEM_NAME} MATCHES "Linux")
diff --git a/tests/bench/parser.lean b/tests/bench/parser.lean
deleted file mode 100644
index 3560876538..0000000000
--- a/tests/bench/parser.lean
+++ /dev/null
@@ -1,8 +0,0 @@
-import Lean.Parser
-
-def main : List String → IO Unit
-| [fname, n] => do
-  let env ← Lean.mkEmptyEnvironment
-  for _ in [0:n.toNat!] do
-    discard $ Lean.Parser.parseFile env fname
-| _    => throw $ IO.userError "give file"
diff --git a/tests/bench/speedcenter.exec.velcom.yaml b/tests/bench/speedcenter.exec.velcom.yaml
index d14b1b36ab..ce47f8b452 100644
--- a/tests/bench/speedcenter.exec.velcom.yaml
+++ b/tests/bench/speedcenter.exec.velcom.yaml
@@ -94,14 +94,6 @@
     cmd: bash -c "ulimit -s unlimited && ./const_fold.lean.out 23"
   build_config:
     cmd: ./compile.sh const_fold.lean
-- attributes:
-    description: new parser Core.lean
-    tags: [fast, suite]
-  run_config:
-    <<: *time
-    cmd: ./parser.lean.out ../../src/Init/Core.lean 100
-  build_config:
-    cmd: ./compile.sh parser.lean
 - attributes:
     description: qsort
     tags: [fast, suite]