From f7a251b75f60b0237425a7e7fb98a68f20521a8a Mon Sep 17 00:00:00 2001 From: Cameron Zwarich Date: Thu, 21 Aug 2025 20:15:36 -0700 Subject: [PATCH] chore: set `experimental.module=true` when running `grind` benchmarks (#10041) --- tests/bench/speedcenter.exec.velcom.yaml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/tests/bench/speedcenter.exec.velcom.yaml b/tests/bench/speedcenter.exec.velcom.yaml index b81dbab650..ccf8d98b46 100644 --- a/tests/bench/speedcenter.exec.velcom.yaml +++ b/tests/bench/speedcenter.exec.velcom.yaml @@ -599,16 +599,16 @@ tags: [fast] run_config: <<: *time - cmd: lean ../lean/run/grind_bitvec2.lean + cmd: lean -Dexperimental.module=true ../lean/run/grind_bitvec2.lean - attributes: description: grind_list2.lean tags: [fast] run_config: <<: *time - cmd: lean ../lean/run/grind_list2.lean + cmd: lean -Dexperimental.module=true ../lean/run/grind_list2.lean - attributes: description: grind_ring_5.lean tags: [fast] run_config: <<: *time - cmd: lean ../lean/run/grind_ring_5.lean + cmd: lean -Dexperimental.module=true ../lean/run/grind_ring_5.lean