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

chore: make perf tests more independent of external factors (#9960)

Browse source
This commit is contained in:
Henrik Böving 2025-08-18 10:45:23 +02:00 • committed by GitHub
parent 48a8dd4a56
commit e4be2b2cad
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
3 changed files with 14 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
tests/bench/hashmap.lean
View file

@ -34,10 +34,10 @@ instance [Pure m] : Std.Iterators.Iterator RandomIterator m UInt64 where
instance [Monad m] [Monad n] : Std.Iterators.IteratorLoopPartial (RandomIterator) m n :=
.defaultImplementation
def mkMapWithCap (seed : UInt64) (size : Nat) : Std.HashMap UInt64 String := Id.run do
def mkMapWithCap (seed : UInt64) (size : Nat) : Std.HashMap UInt64 UInt64 := Id.run 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
return map
def timeNanos (reps : Nat) (x : IO Unit) : IO Float := do
@ -105,7 +105,7 @@ def benchInsertIfNewHit (seed : UInt64) (size : Nat) : IO Float := do
let mut map := map
while todo != 0 do
for val in iterRand seed |>.take size |>.allowNontermination do
map := map.insertIfNew val s!"{val}"
map := map.insertIfNew val val
if map.size != size then
throw <| .userError "Fail"
todo := todo - size
@ -122,7 +122,7 @@ def benchInsertHit (seed : UInt64) (size : Nat) : IO Float := do
let mut map := map
while todo != 0 do
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
@ -170,7 +170,7 @@ def benchEraseInsert (seed : UInt64) (size : Nat) : IO Float := do
let mut todo := checks
while todo != 0 do
for (eraseVal, newVal) in eraseIter.zip newIter |>.take size |>.allowNontermination do
map := map.erase eraseVal |>.insert newVal s!"{newVal}"
map := map.erase eraseVal |>.insert newVal newVal
if map.size != size then
throw <| .userError "Fail"
todo := todo - size

8
tests/bench/phashmap.lean
View file

@ -34,10 +34,10 @@ instance [Pure m] : Std.Iterators.Iterator RandomIterator m UInt64 where
instance [Monad m] [Monad n] : Std.Iterators.IteratorLoopPartial (RandomIterator) m n :=
.defaultImplementation
def mkMapWithCap (seed : UInt64) (size : Nat) : Lean.PersistentHashMap UInt64 String := Id.run do
def mkMapWithCap (seed : UInt64) (size : Nat) : Lean.PersistentHashMap UInt64 UInt64 := Id.run do
let mut map := Lean.PersistentHashMap.empty
for val in iterRand seed |>.take size |>.allowNontermination do
map := map.insert val s!"{val}"
map := map.insert val val
return map
def timeNanos (reps : Nat) (x : IO Unit) : IO Float := do
@ -105,7 +105,7 @@ def benchInsertHit (seed : UInt64) (size : Nat) : IO Float := do
let mut map := map
while todo != 0 do
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
@ -158,7 +158,7 @@ def benchEraseInsert (seed : UInt64) (size : Nat) : IO Float := do
let mut todo := checks
while todo != 0 do
for (eraseVal, newVal) in eraseIter.zip newIter |>.take size |>.allowNontermination do
map := map.erase eraseVal |>.insert newVal s!"{newVal}"
map := map.erase eraseVal |>.insert newVal newVal
if map.isEmpty then
throw <| .userError "Fail"
todo := todo - size

10
tests/bench/treemap.lean
View file

@ -31,10 +31,10 @@ instance [Pure m] : Std.Iterators.Iterator RandomIterator m UInt64 where
instance [Monad m] [Monad n] : Std.Iterators.IteratorLoopPartial (RandomIterator) m n :=
.defaultImplementation
def mkMap (seed : UInt64) (size : Nat) : Std.TreeMap UInt64 String := Id.run do
def mkMap (seed : UInt64) (size : Nat) : Std.TreeMap UInt64 UInt64 := Id.run do
let mut map := {}
for val in iterRand seed |>.take size |>.allowNontermination do
map := map.insert val s!"{val}"
map := map.insert val val
return map
def timeNanos (reps : Nat) (x : IO Unit) : IO Float := do
@ -102,7 +102,7 @@ def benchInsertIfNewHit (seed : UInt64) (size : Nat) : IO Float := do
let mut map := map
while todo != 0 do
for val in iterRand seed |>.take size |>.allowNontermination do
map := map.insertIfNew val s!"{val}"
map := map.insertIfNew val val
if map.size != size then
throw <| .userError "Fail"
todo := todo - size
@ -119,7 +119,7 @@ def benchInsertHit (seed : UInt64) (size : Nat) : IO Float := do
let mut map := map
while todo != 0 do
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
@ -187,7 +187,7 @@ def benchEraseInsert (seed : UInt64) (size : Nat) : IO Float := do
let mut todo := checks
while todo != 0 do
for (eraseVal, newVal) in eraseIter.zip newIter |>.take size |>.allowNontermination do
map := map.erase eraseVal |>.insert newVal s!"{newVal}"
map := map.erase eraseVal |>.insert newVal newVal
if map.size != size then
throw <| .userError "Fail"
todo := todo - size