diff --git a/tests/gmap.ref b/tests/gmap.ref index 71a0b12899e8250eaad1c6535902bfb55ed16287..7e6c436b2490f2d6f417c76ba2c4ea110f04263c 100644 --- a/tests/gmap.ref +++ b/tests/gmap.ref @@ -70,6 +70,14 @@ Failed to progress. ============================ bool_decide (∅ ⊆ {[1; 2; 3]}) = true +"pmap_insert_positives_test" + : string + = true + : bool +"gmap_insert_positives_test" + : string + = true + : bool "gmap_insert_comm" : string 1 goal diff --git a/tests/gmap.v b/tests/gmap.v index 5973a432e00f5109251146c421db604c7315bfb5..158b665c085c2fe25dc075f067303d9265647c73 100644 --- a/tests/gmap.v +++ b/tests/gmap.v @@ -76,11 +76,13 @@ Definition pmap_insert_positives_rev (n : positive) : Pmap unit := Pos.iter (λ rec p m, 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 := 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 2000. Time Eval vm_compute in pmap_insert_positives_test 4000. @@ -93,6 +95,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 1000000. *) +Check "pmap_insert_positives_test". +Eval vm_compute in pmap_insert_positives_test 256000. Definition gmap_insert_positives (n : positive) : gmap positive unit := Pos.iter (λ rec p m, @@ -106,7 +110,9 @@ Definition gmap_insert_positives_test (p : positive) : bool := 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 -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 2000. Time Eval vm_compute in gmap_insert_positives_test 4000. @@ -119,6 +125,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 1000000. *) +Check "gmap_insert_positives_test". +Eval vm_compute in gmap_insert_positives_test 256000. Check "gmap_insert_comm". Theorem gmap_insert_comm :