From b278172b7c8be73678e40cb7fc38c7b2db2bbe1b Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Tue, 7 Nov 2023 17:38:51 +0100
Subject: [PATCH] chore: add `import Lean` benchmark

---
 tests/bench/speedcenter.exec.velcom.yaml | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/tests/bench/speedcenter.exec.velcom.yaml b/tests/bench/speedcenter.exec.velcom.yaml
index 6cc0d1783d..3e0b845910 100644
--- a/tests/bench/speedcenter.exec.velcom.yaml
+++ b/tests/bench/speedcenter.exec.velcom.yaml
@@ -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]