From 72e8970848d787d7888c6384dd5839b3cea0eefd Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Wed, 27 Aug 2025 14:05:04 +0200
Subject: [PATCH] chore: benchmarks for deriving DecidableEq on large
 inductives (#10149)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR adds benchmarks for deriving `DecidableEq` on inductives with
many constructors. (Although at the moment, many is “many” as we timeout
for more than 30 or 40 constructors.)
---
 tests/bench/big_deceq.lean               | 42 ++++++++++++++++++++++++
 tests/bench/big_deceq_rec.lean           | 42 ++++++++++++++++++++++++
 tests/bench/speedcenter.exec.velcom.yaml | 12 +++++++
 3 files changed, 96 insertions(+)
 create mode 100644 tests/bench/big_deceq.lean
 create mode 100644 tests/bench/big_deceq_rec.lean

diff --git a/tests/bench/big_deceq.lean b/tests/bench/big_deceq.lean
new file mode 100644
index 0000000000..9c89bdf5a2
--- /dev/null
+++ b/tests/bench/big_deceq.lean
@@ -0,0 +1,42 @@
+import Lean
+
+/-!
+Creates an non-recursive inductive data type with n constructors and deriving `BEq`.
+-/
+
+set_option Elab.async false
+
+open Lean Elab
+open Elab.Command (CommandElab CommandElabM elabCommand)
+open Parser.Command
+open Parser.Term
+
+-- Create a name.
+def strName (s : String) : Name := Name.anonymous |>.str s
+def mkCtorStr (idx : Nat) : String := s!"con{idx}"
+def mkCtorIdent (idx : Nat) : Ident := mkIdent <| strName <| mkCtorStr idx
+
+/--
+`#test_gen name cnt` creates an inductive type with icnt` unary constructors
+-/
+syntax (name := testGen) (docComment)? "#test_gen" ident num : command -- declare the syntax
+
+@[command_elab testGen]
+def testGenImpl: CommandElab := fun stx => do
+  match stx with
+  | `(#test_gen $t $con_count) =>
+    let con_count := con_count.getNat
+    let cons ← Array.ofFnM (n := con_count) fun cIdx =>
+      let con := mkCtorIdent cIdx
+      `(ctor| | $con:ident : α → $t:ident α )
+    let idecl ←
+      -- Create constant case definitions
+      `(inductive $t:ident (α : Type) : Type where
+        $cons:ctor*
+        deriving DecidableEq
+      )
+    elabCommand idecl
+  | _ =>
+    throwIllFormedSyntax
+
+#time #test_gen T 30
diff --git a/tests/bench/big_deceq_rec.lean b/tests/bench/big_deceq_rec.lean
new file mode 100644
index 0000000000..192d0065f6
--- /dev/null
+++ b/tests/bench/big_deceq_rec.lean
@@ -0,0 +1,42 @@
+import Lean
+
+/-!
+Creates an recursive inductive data type with n constructors and deriving `BEq`.
+-/
+
+set_option Elab.async false
+
+open Lean Elab
+open Elab.Command (CommandElab CommandElabM elabCommand)
+open Parser.Command
+open Parser.Term
+
+-- Create a name.
+def strName (s : String) : Name := Name.anonymous |>.str s
+def mkCtorStr (idx : Nat) : String := s!"con{idx}"
+def mkCtorIdent (idx : Nat) : Ident := mkIdent <| strName <| mkCtorStr idx
+
+/--
+`#test_gen name cnt` creates an inductive type with icnt` unary constructors
+-/
+syntax (name := testGen) (docComment)? "#test_gen" ident num : command -- declare the syntax
+
+@[command_elab testGen]
+def testGenImpl: CommandElab := fun stx => do
+  match stx with
+  | `(#test_gen $t $con_count) =>
+    let con_count := con_count.getNat
+    let cons ← Array.ofFnM (n := con_count) fun cIdx =>
+      let con := mkCtorIdent cIdx
+      `(ctor| | $con:ident : α → $t:ident α → $t:ident α)
+    let idecl ←
+      -- Create constant case definitions
+      `(inductive $t:ident (α : Type) : Type where
+        $cons:ctor*
+        deriving DecidableEq
+      )
+    elabCommand idecl
+  | _ =>
+    throwIllFormedSyntax
+
+#time #test_gen T 30
diff --git a/tests/bench/speedcenter.exec.velcom.yaml b/tests/bench/speedcenter.exec.velcom.yaml
index ccf8d98b46..38a9aeaad2 100644
--- a/tests/bench/speedcenter.exec.velcom.yaml
+++ b/tests/bench/speedcenter.exec.velcom.yaml
@@ -453,6 +453,18 @@
   run_config:
     <<: *time
     cmd: lean big_beq_rec.lean
+- attributes:
+    description: big_deceq
+    tags: [fast, suite]
+  run_config:
+    <<: *time
+    cmd: lean big_deceq.lean
+- attributes:
+    description: big_deceq_rec
+    tags: [fast, suite]
+  run_config:
+    <<: *time
+    cmd: lean big_deceq_rec.lean
 - attributes:
     description: nat_repr
     tags: [fast, suite]