From 4d59fa0c4fb418b17394fa53fa8e8ee3f52d840f Mon Sep 17 00:00:00 2001
From: Georges Gonthier
Date: Mon, 4 Mar 2019 13:20:33 +0100
Subject: locking definitions to address `integral.v` divergence

Line 426 in `integral.v` diverged to over 40 minutes with the new
`finfun.v`, because matching `mod_Iirr` to `quo_Iirr` goes into
exponential backtracking. This is currently averted by limiting the
repetition of `mod_IirrE` in this `rewrite` line.
Making `finfun` mixing opaque brings this down to 40 seconds, and
locking `cfIirr` to a tractable 0.15 seconds, hopefully improving the
instances. This line also takes 47 seconds to execute in the master
branch, so this is likely an undetected Coq performance regression.
---
 mathcomp/character/character.v | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'mathcomp/character')

diff --git a/mathcomp/character/character.v b/mathcomp/character/character.v
index 783c46f..eda6f5a 100644
--- a/mathcomp/character/character.v
+++ b/mathcomp/character/character.v
@@ -667,11 +667,13 @@ Proof. by rewrite eqr_le ltr_geF ?irr1_gt0. Qed.
 Lemma irr_neq0 i : 'chi_i != 0.
 Proof. by apply: contraNneq (irr1_neq0 i) => ->; rewrite cfunE. Qed.
 
-Definition cfIirr B (chi : 'CF(B)) : Iirr B := inord (index chi (irr B)).
+Local Remark cfIirr_key : unit. Proof. by []. Qed.
+Definition cfIirr : forall B, 'CF(B) -> Iirr B :=
+  locked_with cfIirr_key (fun B chi => inord (index chi (irr B))).
 
 Lemma cfIirrE chi : chi \in irr G -> 'chi_(cfIirr chi) = chi.
 Proof.
-move=> chi_irr; rewrite (tnth_nth 0) inordK ?nth_index //.
+move=> chi_irr; rewrite (tnth_nth 0) [cfIirr]unlock inordK ?nth_index //.
 by rewrite -index_mem size_tuple in chi_irr.
 Qed.
 
-- 
cgit v1.2.3