Libobject: what is "Global universe name state"? · Coq devs & plugin devs

Stream: Coq devs & plugin devs

Topic: Libobject: what is "Global universe name state"?

Enrico Tassi (Jan 11 2021 at 15:22):

I'm playing with the idea of printing module/libstack so that we print everything (or at least, Instances & co, so that Print Module becomes a bit more informative).

Now, I hacked a new print_function into libobject and this is what I see printing Logic. (just an excerpt):

Theorem  absurd :  forall A C : Prop, A -> ~ A -> C.
  TODO: printer for object IMPLICITS
  TODO: printer for object ARGUMENTS-SCOPE
  TODO: printer for object Global universe name state

It makes sense to me that the theorem comes equipped with impargs and argscope declarations.
But what is this "Global universe name state"? Note that there is not even a Type in the statement.

Enrico Tassi (Jan 11 2021 at 15:23):

For the records, this libobject is everywhere (after each and every declaration)

Pierre-Marie Pédrot (Jan 11 2021 at 15:25):

It's a map that associates a name to a monomorphic level, e.g. here Logic.3461 ↦ Logic.absurd.u1

Pierre-Marie Pédrot (Jan 11 2021 at 15:26):

FTR, it consumes a lot of the vo space and I am not quite sure of its interest, since we could recompute names on the fly

Pierre-Marie Pédrot (Jan 11 2021 at 15:27):

IIRC this was introduced by @Gaëtan Gilbert

Guillaume Melquiond (Jan 11 2021 at 15:28):

Do I understand correctly that every monomorphic definition gets a monomorphic level? (Is it even used later?)

Pierre-Marie Pédrot (Jan 11 2021 at 15:29):

Every monomorphic definition declares global universes

Pierre-Marie Pédrot (Jan 11 2021 at 15:30):

It could be an empty set, but this would be quite rare.

Pierre-Marie Pédrot (Jan 11 2021 at 15:30):

It's the dreaded global state of Coq.

Pierre-Marie Pédrot (Jan 11 2021 at 15:30):

Atop of that we register fancy names for those levels, so that the upper layers remember that some cryptic name comes from another definition.

Guillaume Melquiond (Jan 11 2021 at 15:31):

But that is the part I do not understand: Why are empty sets rare?

Pierre-Marie Pédrot (Jan 11 2021 at 15:32):

Universes are generated everytime you write e.g. Type or use a template polymorphic universe.

Pierre-Marie Pédrot (Jan 11 2021 at 15:32):

So it's quite often.

Pierre-Marie Pédrot (Jan 11 2021 at 15:33):

I am not a specialist of universe minimization, but I think that Coq does a best effort to reduce that set of globals, even in monomorphic mode

Guillaume Melquiond (Jan 11 2021 at 15:34):

I guess your mileage may vary, depending on what you use Coq for. Or are you saying that even Enrico's propositional logic example would get a non-empty set?