From f269ffd88b6a725d8f8f6a7bf1e91799b361a31f Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Mon, 25 Nov 2019 00:47:13 -0500
Subject: Add a complexity test for `pattern`

This is to hopefully prevent regressions on
https://github.com/coq/coq/issues/11150 and
https://github.com/coq/coq/issues/6502.
---
 test-suite/complexity/pattern.v | 38 ++++++++++++++++++++++++++++++++++++++
 1 file changed, 38 insertions(+)
 create mode 100644 test-suite/complexity/pattern.v

diff --git a/test-suite/complexity/pattern.v b/test-suite/complexity/pattern.v
new file mode 100644
index 0000000000..14e388cd75
--- /dev/null
+++ b/test-suite/complexity/pattern.v
@@ -0,0 +1,38 @@
+(** Testing the performance of [pattern].  For not regressing on COQBUG(https://github.com/coq/coq/issues/11150) and COQBUG(https://github.com/coq/coq/issues/6502) *)
+(* Expected time < 0.75s *)
+(* reference: 0.673s after adjustment *)
+Definition Let_In {A P} (v : A) (f : forall x : A, P x) : P v
+:= let x := v in f x.
+
+Fixpoint big (a : nat) (sz : nat) : nat
+  := match sz with
+     | O => a
+     | S sz' => Let_In (a * a) (fun a' => big a' sz')
+     end.
+
+Ltac do_time n :=
+  try (
+      once (assert (exists e, e = big 1 n);
+            [ lazy -[big]; (*match goal with |- ?G => idtac G end;*) lazy [big];
+              time pattern Nat.mul, S, O, (@Let_In nat (fun _ => nat))
+            | ]);
+      fail).
+
+Ltac do_time_to n :=
+  lazymatch (eval vm_compute in n) with
+  | O => idtac
+  | ?n' => do_time_to (Nat.div2 n'); idtac n'; do_time n'
+  end.
+
+Local Set Warnings Append "-abstract-large-number".
+
+(* Don't spend lots of time printing *)
+Notation hide := (_ = _).
+
+Goal True.
+Proof.
+  (* do_time_to 16384. *) (* should be linear, not quadratic *)
+  assert (exists e, e = big 1 16384).
+  lazy -[big]; (*match goal with |- ?G => idtac G end;*) lazy [big].
+  Timeout 15 Time pattern Nat.mul, S, O, (@Let_In nat (fun _ => nat)).
+Abort.
-- 
cgit v1.2.3


From 73bb54d1625ae6eafdb9eb7f2c673fb039150fdb Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Tue, 26 Nov 2019 13:27:56 -0500
Subject: Update test-suite/complexity/pattern.v

Co-Authored-By: Hugo Herbelin <herbelin@users.noreply.github.com>---
 test-suite/complexity/pattern.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/test-suite/complexity/pattern.v b/test-suite/complexity/pattern.v
index 14e388cd75..fb5bf5a00b 100644
--- a/test-suite/complexity/pattern.v
+++ b/test-suite/complexity/pattern.v
@@ -24,7 +24,7 @@ Ltac do_time_to n :=
   | ?n' => do_time_to (Nat.div2 n'); idtac n'; do_time n'
   end.
 
-Local Set Warnings Append "-abstract-large-number".
+Local Set Warnings "-abstract-large-number".
 
 (* Don't spend lots of time printing *)
 Notation hide := (_ = _).
-- 
cgit v1.2.3