max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: set experimental.module=true when running grind benchmarks (#10041)

Browse source
This commit is contained in:
Cameron Zwarich 2025-08-21 20:15:36 -07:00 • committed by GitHub
parent 5aa706435a
commit f7a251b75f
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
tests/bench/speedcenter.exec.velcom.yaml
View file

@ -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