Skip to content
Snippets Groups Projects
Commit a72a0a46 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Further improve tests.

parent 88f8b9a3
No related branches found
No related tags found
No related merge requests found
Pipeline #51312 failed
This commit is part of merge request !309. Comments created here will be created in the context of that merge request.
Hide whitespace changes
Inline Side-by-side
Showing
with 11 additions and 3 deletions
tests/gmap.v
+ 11
− 3
View file @ a72a0a46
...@@ -7,11 +7,13 @@ Definition pmap_insert_positives_rev (n : positive) : Pmap unit := ...@@ -7,11 +7,13 @@ Definition pmap_insert_positives_rev (n : positive) : Pmap unit :=
Pos.iter (λ rec p m, Pos.iter (λ rec p m,
rec (p - 1)%positive (<[p:=tt]> m)) (λ _ m, m) n n ∅. rec (p - 1)%positive (<[p:=tt]> m)) (λ _ m, m) n n ∅.
(* Test that the time is approximately n-log-n. We cannot test this on CI since
you get different timings all the time.
Definition pmap_insert_positives_test (p : positive) : bool := Definition pmap_insert_positives_test (p : positive) : bool :=
bool_decide (pmap_insert_positives p = pmap_insert_positives_rev p). bool_decide (pmap_insert_positives p = pmap_insert_positives_rev p).
(* Test that the time is approximately n-log-n. We cannot test this on CI since
you get different timings all the time. Instead we just test for [256000], which
likely takes forever if the complexity is not n-log-n. *)
(*
Time Eval vm_compute in pmap_insert_positives_test 1000. Time Eval vm_compute in pmap_insert_positives_test 1000.
Time Eval vm_compute in pmap_insert_positives_test 2000. Time Eval vm_compute in pmap_insert_positives_test 2000.
Time Eval vm_compute in pmap_insert_positives_test 4000. Time Eval vm_compute in pmap_insert_positives_test 4000.
...@@ -24,6 +26,8 @@ Time Eval vm_compute in pmap_insert_positives_test 256000. ...@@ -24,6 +26,8 @@ Time Eval vm_compute in pmap_insert_positives_test 256000.
Time Eval vm_compute in pmap_insert_positives_test 512000. Time Eval vm_compute in pmap_insert_positives_test 512000.
Time Eval vm_compute in pmap_insert_positives_test 1000000. Time Eval vm_compute in pmap_insert_positives_test 1000000.
*) *)
Check "pmap_insert_positives_test".
Eval vm_compute in pmap_insert_positives_test 256000.
Definition gmap_insert_positives (n : positive) : gmap positive unit := Definition gmap_insert_positives (n : positive) : gmap positive unit :=
Pos.iter (λ rec p m, Pos.iter (λ rec p m,
...@@ -37,7 +41,9 @@ Definition gmap_insert_positives_test (p : positive) : bool := ...@@ -37,7 +41,9 @@ Definition gmap_insert_positives_test (p : positive) : bool :=
bool_decide (gmap_insert_positives p = gmap_insert_positives_rev p). bool_decide (gmap_insert_positives p = gmap_insert_positives_rev p).
(* Test that the time is approximately n-log-n. We cannot test this on CI since (* Test that the time is approximately n-log-n. We cannot test this on CI since
you get different timings all the time. you get different timings all the time. Instead we just test for [256000], which
likely takes forever if the complexity is not n-log-n. *)
(*
Time Eval vm_compute in gmap_insert_positives_test 1000. Time Eval vm_compute in gmap_insert_positives_test 1000.
Time Eval vm_compute in gmap_insert_positives_test 2000. Time Eval vm_compute in gmap_insert_positives_test 2000.
Time Eval vm_compute in gmap_insert_positives_test 4000. Time Eval vm_compute in gmap_insert_positives_test 4000.
...@@ -50,6 +56,8 @@ Time Eval vm_compute in gmap_insert_positives_test 256000. ...@@ -50,6 +56,8 @@ Time Eval vm_compute in gmap_insert_positives_test 256000.
Time Eval vm_compute in gmap_insert_positives_test 512000. Time Eval vm_compute in gmap_insert_positives_test 512000.
Time Eval vm_compute in gmap_insert_positives_test 1000000. Time Eval vm_compute in gmap_insert_positives_test 1000000.
*) *)
Check "gmap_insert_positives_test".
Eval vm_compute in gmap_insert_positives_test 256000.
Check "gmap_insert_comm". Check "gmap_insert_comm".
Theorem gmap_insert_comm : Theorem gmap_insert_comm :
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment