From 76cb1373b3af0c23579925562667d373ab792ef5 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Wed, 14 Oct 2026 17:25:21 +0200 Subject: [PATCH] fix(clone): no quadratic check of proved lemmas in theory overrides A theory override leaves alone the items that already have an override. For each lemma of the overridden theory, it scanned the whole list of the proofs given so far, which includes those implied by the previous theory overrides of the clone: a clone threading several large theories with theory overrides spent most of its time comparing qualified names. The names of the lemmas already proved are now collected in a hash table, once per theory override. --- src/ecThCloning.ml | 15 +++++++++++---- 1 file changed, 11 insertions(+), 4 deletions(-) diff --git a/src/ecThCloning.ml b/src/ecThCloning.ml index 93a208095..20562eaab 100644 --- a/src/ecThCloning.ml +++ b/src/ecThCloning.ml @@ -535,6 +535,16 @@ end = struct in { evc with evc_ths = ths }) nm evc in + (* The lemmas that already have a proof *) + let proved : (qsymbol, unit) Hashtbl.t = + let proved = Hashtbl.create 0 in + List.iter (fun prf -> + match prf.pthp_mode with + | `Named (y, _) -> Hashtbl.replace proved (unloc y) () + | `All _ -> ()) + proofs; + proved in + (* A more specific override takes precedence over the one implied * by the theory override. *) let overridden (prefix : symbol list) (dth : theory_item_r) = @@ -558,10 +568,7 @@ end = struct |> obind (fun (sub, _) -> sub.evc_target) |> is_some | Th_axiom (x, _) -> - List.exists (fun prf -> - match prf.pthp_mode with - | `Named (y, _) -> unloc y = (xdth @ prefix, x) - | `All _ -> false) proofs + Hashtbl.mem proved (xdth @ prefix, x) | _ -> false in let rec doit_r (prefix, tgprefix) (proofs, evc) dth =