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

chore: even more independent benchmarks (#9970)

Browse source
This commit is contained in:
Henrik Böving 2025-08-18 20:36:33 +02:00 • committed by GitHub
parent 1b0d83e7fc
commit 2d4bcf202f
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
3 changed files with 7 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
tests/bench/hashmap.lean
View file

@ -137,7 +137,7 @@ def benchInsertMissEmpty (seed : UInt64) (size : Nat) : IO Float := do
while todo != 0 do
let mut map : Std.HashMap _ _ := {}
for val in iterRand seed |>.take size |>.allowNontermination do
map := map.insert val s!"{val}"
map := map.insert val val
if map.size > size then
throw <| .userError "Fail"
todo := todo - size
@ -152,7 +152,7 @@ def benchInsertMissEmptyWithCapacity (seed : UInt64) (size : Nat) : IO Float :=
while todo != 0 do
let mut map := Std.HashMap.emptyWithCapacity size
for val in iterRand seed |>.take size |>.allowNontermination do
map := map.insert val s!"{val}"
map := map.insert val val
if map.size > size then
throw <| .userError "Fail"
todo := todo - size

4
tests/bench/phashmap.lean
View file

@ -120,7 +120,7 @@ def benchInsertMissEmpty (seed : UInt64) (size : Nat) : IO Float := do
while todo != 0 do
let mut map : Lean.PersistentHashMap _ _ := {}
for val in iterRand seed |>.take size |>.allowNontermination do
map := map.insert val s!"{val}"
map := map.insert val val
if map.isEmpty then
throw <| .userError "Fail"
todo := todo - size
@ -137,7 +137,7 @@ def benchInsertMissEmptyShared (seed : UInt64) (size : Nat) : IO Float := do
let mut map : Lean.PersistentHashMap _ _ := {}
let mut maps := Array.emptyWithCapacity size
for val in iterRand seed |>.take size |>.allowNontermination do
map := map.insert val s!"{val}"
map := map.insert val val
if map.isEmpty then
throw <| .userError "Fail"
maps := maps.push map

6
tests/bench/treemap.lean
View file

@ -134,7 +134,7 @@ def benchInsertRandomMissEmpty (seed : UInt64) (size : Nat) : IO Float := do
while todo != 0 do
let mut map : Std.TreeMap UInt64 _ := {}
for val in iterRand seed |>.take size |>.allowNontermination do
map := map.insert val s!"{val}"
map := map.insert val val
if map.size > size then
throw <| .userError "Fail"
todo := todo - size
@ -149,7 +149,7 @@ def benchInsertSequentialMissEmpty (_seed : UInt64) (size : Nat) : IO Float := d
while todo != 0 do
let mut map : Std.TreeMap UInt64 _ := {}
for val in [0:size] do
map := map.insert val.toUInt64 s!"{val}"
map := map.insert val.toUInt64 val
if map.size > size then
throw <| .userError "Fail"
todo := todo - size
@ -166,7 +166,7 @@ def benchInsertRandomMissEmptyShared (seed : UInt64) (size : Nat) : IO Float :=
let mut map : Std.TreeMap UInt64 _ := {}
let mut maps := Array.emptyWithCapacity size
for val in iterRand seed |>.take size |>.allowNontermination do
map := map.insert val s!"{val}"
map := map.insert val val
if map.isEmpty then
throw <| .userError "Fail"
maps := maps.push map