chore: benchmark for deriving BEq on large inductive (#10028)

tests/bench/big_beq.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 BEq
+      )
+    elabCommand idecl
+  | _ =>
+    throwIllFormedSyntax
+
+#time #test_gen T 100

tests/bench/big_beq_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 BEq
+      )
+    elabCommand idecl
+  | _ =>
+    throwIllFormedSyntax
+
+#time #test_gen T 100

tests/bench/speedcenter.exec.velcom.yaml

@@ -441,6 +441,18 @@
   run_config:
     <<: *time
     cmd: lean big_match.lean
+- attributes:
+    description: big_beq
+    tags: [fast, suite]
+  run_config:
+    <<: *time
+    cmd: lean big_beq.lean
+- attributes:
+    description: big_beq_rec
+    tags: [fast, suite]
+  run_config:
+    <<: *time
+    cmd: lean big_beq_rec.lean
 - attributes:
     description: nat_repr
     tags: [fast, suite]