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.
For the records, this libobject is everywhere (after each and every declaration)
It's a map that associates a name to a monomorphic level, e.g. here Logic.3461 ↦ Logic.absurd.u1
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
IIRC this was introduced by @Gaëtan Gilbert
Do I understand correctly that every monomorphic definition gets a monomorphic level? (Is it even used later?)
Every monomorphic definition declares global universes
It could be an empty set, but this would be quite rare.
It's the dreaded global state of Coq.
Atop of that we register fancy names for those levels, so that the upper layers remember that some cryptic name comes from another definition.
But that is the part I do not understand: Why are empty sets rare?
Universes are generated everytime you write e.g. Type or use a template polymorphic universe.
So it's quite often.
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
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?
Let me check, it seems surprising but with universes one can never know.
seems to be universe-free, thankfully
There should be a fast-path not to declare an empty set of universes, probably.
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?
Those names are autogenerated most of the time.
anyway it would be trivial to avoid adding an object when there are no universes, it just wasn't done
Yes, I just wrote the patch
being autogenerated doesn't mean it's reasonable to reconstruct dynamically
Why not?
I don't see the interest of bloating the vo with such interesting names as Foo.bar.u3781
We could just reconstruct the table with fresh names at vo loading or something
Or better, store the actual info in the universe level
That is, instead of a dirpath + gensym, use a dirpath + ident + gensym
I'll try the fix suggested by gaetan
https://github.com/coq/coq/pull/13736
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?
Ah, you're right, in my haste I forgot that one.
I'll centralize the check, that's probably even better.
https://github.com/coq/coq/pull/13737
damn
the one in do_universe is nonempty because Universes .
doesn't parse
I am disappointed, my theories
was 96MB before, and it is still 96MB after the pull request.
but you can require it 0.000001% faster
(maybe)
Last updated: Jun 04 2023 at 19:30 UTC