Stream: Coq devs & plugin devs

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


view this post on Zulip 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.

view this post on Zulip Enrico Tassi (Jan 11 2021 at 15:23):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Jan 11 2021 at 15:27):

IIRC this was introduced by @Gaëtan Gilbert

view this post on Zulip 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?)

view this post on Zulip Pierre-Marie Pédrot (Jan 11 2021 at 15:29):

Every monomorphic definition declares global universes

view this post on Zulip Pierre-Marie Pédrot (Jan 11 2021 at 15:30):

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

view this post on Zulip Pierre-Marie Pédrot (Jan 11 2021 at 15:30):

It's the dreaded global state of Coq.

view this post on Zulip 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.

view this post on Zulip Guillaume Melquiond (Jan 11 2021 at 15:31):

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

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Jan 11 2021 at 15:32):

So it's quite often.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Pierre-Marie Pédrot (Jan 11 2021 at 15:35):

Let me check, it seems surprising but with universes one can never know.

view this post on Zulip Pierre-Marie Pédrot (Jan 11 2021 at 15:37):

seems to be universe-free, thankfully

view this post on Zulip Pierre-Marie Pédrot (Jan 11 2021 at 15:38):

There should be a fast-path not to declare an empty set of universes, probably.

view this post on Zulip Gaëtan Gilbert (Jan 11 2021 at 15:41):

Pierre-Marie Pédrot said:

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

how?

view this post on Zulip Pierre-Marie Pédrot (Jan 11 2021 at 15:41):

Those names are autogenerated most of the time.

view this post on Zulip Gaëtan Gilbert (Jan 11 2021 at 15:42):

anyway it would be trivial to avoid adding an object when there are no universes, it just wasn't done

view this post on Zulip Pierre-Marie Pédrot (Jan 11 2021 at 15:42):

Yes, I just wrote the patch

view this post on Zulip Gaëtan Gilbert (Jan 11 2021 at 15:42):

being autogenerated doesn't mean it's reasonable to reconstruct dynamically

view this post on Zulip Pierre-Marie Pédrot (Jan 11 2021 at 15:43):

Why not?

view this post on Zulip Pierre-Marie Pédrot (Jan 11 2021 at 15:43):

I don't see the interest of bloating the vo with such interesting names as Foo.bar.u3781

view this post on Zulip Pierre-Marie Pédrot (Jan 11 2021 at 15:43):

We could just reconstruct the table with fresh names at vo loading or something

view this post on Zulip Pierre-Marie Pédrot (Jan 11 2021 at 15:44):

Or better, store the actual info in the universe level

view this post on Zulip Pierre-Marie Pédrot (Jan 11 2021 at 15:44):

That is, instead of a dirpath + gensym, use a dirpath + ident + gensym

view this post on Zulip Enrico Tassi (Jan 11 2021 at 15:45):

I'll try the fix suggested by gaetan

view this post on Zulip Pierre-Marie Pédrot (Jan 11 2021 at 15:45):

https://github.com/coq/coq/pull/13736

view this post on Zulip Guillaume Melquiond (Jan 11 2021 at 15:48):

There are two instances of input_univ_names and you have conditionalized only one of them. Is the other one guaranteed to always be nonempty?

view this post on Zulip Pierre-Marie Pédrot (Jan 11 2021 at 15:48):

Ah, you're right, in my haste I forgot that one.

view this post on Zulip Pierre-Marie Pédrot (Jan 11 2021 at 15:48):

I'll centralize the check, that's probably even better.

view this post on Zulip Enrico Tassi (Jan 11 2021 at 15:54):

https://github.com/coq/coq/pull/13737

view this post on Zulip Enrico Tassi (Jan 11 2021 at 15:54):

damn

view this post on Zulip Gaëtan Gilbert (Jan 11 2021 at 15:55):

the one in do_universe is nonempty because Universes . doesn't parse

view this post on Zulip Guillaume Melquiond (Jan 11 2021 at 16:02):

I am disappointed, my theories was 96MB before, and it is still 96MB after the pull request.

view this post on Zulip Enrico Tassi (Jan 11 2021 at 16:03):

but you can require it 0.000001% faster

view this post on Zulip Enrico Tassi (Jan 11 2021 at 16:03):

(maybe)


Last updated: Oct 16 2021 at 02:03 UTC