From fad343d9ef19d20dfd7b2a3dd2ccc6e6fc08072f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Wojciech=20R=C3=B3=C5=BCowski?= <wojciech@lean-fro.org>
Date: Thu, 19 Feb 2026 13:59:42 +0000
Subject: [PATCH] test: add `List.mergeSort` benchmark for `cbv` tactic
 (#12588)

This PR adds a benchmark for `cbv` tactic that involves evaluating
`List.mergeSort` on a reversed list on natural numbers.
---
 tests/bench/cbv/merge_sort.lean          | 50 ++++++++++++++++++++++++
 tests/bench/speedcenter.exec.velcom.yaml |  6 +++
 2 files changed, 56 insertions(+)
 create mode 100644 tests/bench/cbv/merge_sort.lean

diff --git a/tests/bench/cbv/merge_sort.lean b/tests/bench/cbv/merge_sort.lean
new file mode 100644
index 0000000000..e5d4d478c5
--- /dev/null
+++ b/tests/bench/cbv/merge_sort.lean
@@ -0,0 +1,50 @@
+import Lean
+open Lean
+
+/-- Build an `Expr` for the list `[1, 2, ..., n]` of type `List Nat`. -/
+partial def mkRangeListExpr (n : Nat) : Expr :=
+  let natExpr := mkConst ``Nat
+  let nil := mkApp (mkConst ``List.nil [.zero]) natExpr
+  let cons := fun (head tail : Expr) => mkApp3 (mkConst ``List.cons [.zero]) natExpr head tail
+  let rec mkList (i : Nat) (acc : Expr) : Expr :=
+    if i == 0 then acc
+    else mkList (i - 1) (cons (mkNatLit i) acc)
+  mkList n nil
+
+/-- Build an `Expr` for the list `[n, n-1, ..., 1]` of type `List Nat`. -/
+partial def mkRevRangeListExpr (n : Nat) : Expr :=
+  let natExpr := mkConst ``Nat
+  let nil := mkApp (mkConst ``List.nil [.zero]) natExpr
+  let cons := fun (head tail : Expr) => mkApp3 (mkConst ``List.cons [.zero]) natExpr head tail
+  let rec mkList (i : Nat) (acc : Expr) : Expr :=
+    if i == 0 then acc
+    else mkList (i - 1) (cons (mkNatLit (n - i + 1)) acc)
+  mkList n nil
+
+/-- Build the expression `List.mergeSort [n, ..., 1] Nat.ble`. -/
+def mkMergeSortProblem (n : Nat) : Expr :=
+  let natExpr := mkConst ``Nat
+  let list := mkRevRangeListExpr n
+  let le := mkConst ``Nat.ble
+  mkApp3 (mkConst ``List.mergeSort [.zero]) natExpr list le
+
+def runProblem (n : Nat) : MetaM Unit := do
+  let problem := mkMergeSortProblem n
+  let startTime ← IO.monoNanosNow
+  let executed ← Lean.Meta.Tactic.Cbv.cbvEntry problem
+  let endTime ← IO.monoNanosNow
+  let ms := (endTime - startTime).toFloat / 1000000.0
+  match executed with
+  | .rfl _ => IO.println s!"mergeSort_{n}: {ms} ms (rfl)"
+  | .step _ proof _ =>
+    let startTime ← IO.monoNanosNow
+    Meta.checkWithKernel proof
+    let endTime ← IO.monoNanosNow
+    let kernelMs := (endTime - startTime).toFloat / 1000000.0
+    IO.println s!"mergeSort_{n}: cbv {ms} ms, kernel {kernelMs} ms"
+
+def runBenchmarks : MetaM Unit := do
+  IO.println "=== Merge Sort CBV Benchmarks ==="
+  IO.println ""
+  for n in [10, 25, 50, 75, 100, 125, 175] do
+    runProblem n
diff --git a/tests/bench/speedcenter.exec.velcom.yaml b/tests/bench/speedcenter.exec.velcom.yaml
index 734f3de270..98c08d3053 100644
--- a/tests/bench/speedcenter.exec.velcom.yaml
+++ b/tests/bench/speedcenter.exec.velcom.yaml
@@ -689,3 +689,9 @@
   run_config:
     <<: *time
     cmd: lean ./cbv/decide.lean
+- attributes:
+    description: cbv tactic (evaluating List.mergeSort)
+    tags: [other]
+  run_config:
+    <<: *time
+    cmd: lean ./cbv/merge_sort.lean
\ No newline at end of file