chore: remove broken & redundant "new parser Core.lean" benchmark

This commit is contained in:
Sebastian Ullrich 2020-11-13 19:57:06 +01:00
parent fe03e70a8a
commit 1add44916c
3 changed files with 2 additions and 18 deletions

View file

@ -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")

View file

@ -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"

View file

@ -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]