Fix slow Print Universes Subgraph when many ambient universes.

Fix #12688.

Original test:
~~~coq
Record my_mod: Type := mk { datatype: Type; }.
Print Universes Subgraph (my_mod.u0). (* OK *)
From ITree Require Export ITree.      (* using coq-itree for the sake of example *)
Print Universes Subgraph (my_mod.u0). (* Runs forever (> 1 min) *)
~~~

The issue is that we produce a subgraph with the user-given universes
+ Set and Prop. In the test the user given universes are not connected
to other universes, but Set is below every universe so we traverse the
whole graph.

We can go faster by just checking whether Set is strictly below each
universe we're interested in.

Maybe this would be better handled at the ugraph level but that
requires thinking about lbound so I didn't do it.

I tested locally with Require Reals, which makes the print take about
0.1s on my PC before this patch. This is enough to check that we're
now faster (near-instant) but not enough for automatic testing.

Note that the other uses of UGraph.constraints_for (for private
polymorphic universes and for context restriction) are interested in
all ambient universes so the traversals starting at Set end quickly
and do not cause the same issue.

1 files changed, 10 insertions, 6 deletions

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index d540e7f93d..548f59559a 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -345,17 +345,21 @@ let dump_universes_gen prl g s =
     close ();
     Exninfo.iraise reraise
 
-let universe_subgraph ?loc g univ =
+let universe_subgraph ?loc kept univ =
   let open Univ in
   let sigma = Evd.from_env (Global.env()) in
-  let univs_of q =
+  let parse q =
     let q =  Glob_term.(GType q) in
     (* this function has a nice error message for not found univs *)
-    LSet.singleton (Pretyping.interp_known_glob_level ?loc sigma q)
+    Pretyping.interp_known_glob_level ?loc sigma q
   in
-  let univs = List.fold_left (fun univs q -> LSet.union univs (univs_of q)) LSet.empty g in
-  let csts = UGraph.constraints_for ~kept:(LSet.add Level.prop (LSet.add Level.set univs)) univ in
-  let univ = LSet.fold UGraph.add_universe_unconstrained univs UGraph.initial_universes in
+  let kept = List.fold_left (fun kept q -> LSet.add (parse q) kept) LSet.empty kept in
+  let csts = UGraph.constraints_for ~kept univ in
+  let add u newgraph =
+    let strict = UGraph.check_constraint univ (Level.set,Lt,u) in
+    UGraph.add_universe u ~lbound:UGraph.Bound.Set ~strict newgraph
+  in
+  let univ = LSet.fold add kept UGraph.initial_universes in
   UGraph.merge_constraints csts univ
 
 let print_universes ?loc ~sort ~subgraph dst =