chore: add import Lean benchmark

This commit is contained in:
Sebastian Ullrich 2023-11-07 17:38:51 +01:00
parent d9eddc9652
commit b278172b7c

View file

@ -47,6 +47,12 @@
wc -c ${BUILD:-../../build/release}/stage2/lib/lean/libleanshared.so | cut -d' ' -f 1
max_runs: 1
runner: output
- attributes:
description: import Lean
tags: [fast]
run_config:
<<: *time
cmd: lean ../../src/Lean.lean
- attributes:
description: tests/compiler
tags: [deterministic, slow]