From 8dd6ba825881e9b2e683b647c65364f787321a69 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 28 Jul 2021 00:07:05 +0200
Subject: [PATCH] Further improve tests.

---
 tests/gmap.ref |  8 ++++++++
 tests/gmap.v   | 14 +++++++++++---
 2 files changed, 19 insertions(+), 3 deletions(-)

diff --git a/tests/gmap.ref b/tests/gmap.ref
index 71a0b128..7e6c436b 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 5973a432..158b665c 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 :
-- 
GitLab