Stream: Coq devs & plugin devs

Topic: Section discharge


view this post on Zulip Hugo Herbelin (Jul 29 2021 at 11:38):

Hi, on a way trying to address ceps #51, I spent some time on cooking.ml. Is anyone working and having plans with it already? In any case, I would like to share a rather big factorization I could do of the code, having all the technical work (adding term and universe parameters to generalized globals, substituting vars by rels for both terms in universes, abstracting over the section context of local both terms and universes) concentrated in one function working on a refined formulation of what were called abstr_info and work_list. I'd be curious of opinions about it before proposing it as a PR. It is mostly one commit, with some documentation, but it is for instance difficult to judge it the documentation is clear enough.

If time allows, I'd be tempted to continue with some small cleaning of safe_typing and term_typing. Has anyone planned related projects, or would like to work on such kind of cleaning/documentation project, so that others can eventually enter and understand the structure of the code more easily?

view this post on Zulip Hugo Herbelin (Jul 29 2021 at 11:52):

This kind of cleaning/documentation would suspectingly help the work on MetaCoq's "safechecker".

view this post on Zulip Pierre-Marie Pédrot (Jul 29 2021 at 12:01):

Regarding safe_typing, I have some stuff pending for a long time about monomorphic universes and kernel side-effects, which are blocked for technical reasons on issues related to the higher layers (namely the STM). I don't know if this would interact much with your cleanup though.

view this post on Zulip Hugo Herbelin (Jul 29 2021 at 13:51):

Do you have the branch online?

view this post on Zulip Hugo Herbelin (Jul 29 2021 at 13:54):

By the way, was there a problem with #9380? I feel that we may gain a lot at factorizing the code around universes: it looks like we are doing always similar treatments which could be treated more uniformly.

view this post on Zulip Hugo Herbelin (Jul 29 2021 at 13:55):

About term_typing, I don't know why there is a detour by Cooking.result. It looks like a useless and easy cut to eliminate.

view this post on Zulip Hugo Herbelin (Jul 29 2021 at 13:57):

I don't know why the main typing functions are called translate rather than infer (or check). This looks like obfuscating their meaning to me.

view this post on Zulip Pierre-Marie Pédrot (Jul 29 2021 at 13:57):

@Hugo Herbelin IIRC the problem with that PR was that it was duplicating monomorphic constraints in several places. We should strive to remove them from all kernel datatypes except the environment, because that's the only place where they make sense (barring private monomorphic constants)

view this post on Zulip Pierre-Marie Pédrot (Jul 29 2021 at 13:57):

duplicating pieces of global state is not only error-prone, it's also inefficient

view this post on Zulip Pierre-Marie Pédrot (Jul 29 2021 at 13:58):

currently there is still a bit of nonsense in the kernel that we use to print "monomorphic constraints introduced by a constant"

view this post on Zulip Pierre-Marie Pédrot (Jul 29 2021 at 13:58):

but this is not sound, constraints really are global

view this post on Zulip Pierre-Marie Pédrot (Jul 29 2021 at 13:58):

thankfully it's only used by printing

view this post on Zulip Pierre-Marie Pédrot (Jul 29 2021 at 13:59):

(I think you mentioned that you wanted to remove this, which I support 100%)

view this post on Zulip Hugo Herbelin (Jul 29 2021 at 13:59):

OK, I see, I thought the problem was about unifying Polymorphic and Monomorphic. But the attachment of global universes to constants is indeed a bit strange.

view this post on Zulip Hugo Herbelin (Jul 29 2021 at 14:01):

Even in printing. You see (* {foo.u foo.v |= *) for constants with monomorphic universes while the only link they have with the constant is that they have been introduced by this constant, i.e. it's only about the name.

view this post on Zulip Pierre-Marie Pédrot (Jul 29 2021 at 14:01):

yes, but even this is handled outside of the kernel

view this post on Zulip Pierre-Marie Pédrot (Jul 29 2021 at 14:01):

(i.e. this is essentially debugging stuff)

view this post on Zulip Hugo Herbelin (Jul 29 2021 at 14:05):

So, if I understand correctly, you don't want to merge Monomorphic and Polymorphic. What you want is to move the universe levels out of the "monomorphic" constant and to keep in Monomorphic only the constraints.

view this post on Zulip Hugo Herbelin (Jul 29 2021 at 14:05):

In which case Monomorphic becomes mechanically a subcase of Polymorphic.

view this post on Zulip Pierre-Marie Pédrot (Jul 29 2021 at 14:06):

No no, even the constraints should get out.

view this post on Zulip Pierre-Marie Pédrot (Jul 29 2021 at 14:06):

the two things don't behave the same

view this post on Zulip Pierre-Marie Pédrot (Jul 29 2021 at 14:06):

a monomorphic definition with only constraints is not the same as a polymorphic one with only constraints

view this post on Zulip Hugo Herbelin (Jul 29 2021 at 14:06):

OK, and the constraints between non-polymorphic universes in Polymorphic would also go out of Polymorphic?

view this post on Zulip Pierre-Marie Pédrot (Jul 29 2021 at 14:07):

I don't care, but I think that there is no reason either

view this post on Zulip Pierre-Marie Pédrot (Jul 29 2021 at 14:07):

you might want to actually use the "weird" behaviour mentioned in an issue before

view this post on Zulip Pierre-Marie Pédrot (Jul 29 2021 at 14:07):

it's useful to quantify over ghost constraints

view this post on Zulip Hugo Herbelin (Jul 29 2021 at 14:08):

You mean because of lazyness of inclusion of constraints between non-variable universes in Polymorphic?

view this post on Zulip Pierre-Marie Pédrot (Jul 29 2021 at 14:08):

it's not laziness, it's quantification

view this post on Zulip Pierre-Marie Pédrot (Jul 29 2021 at 14:08):

a monomorphic constraints is just a polymorphic one with a set of constraints generated by default

view this post on Zulip Pierre-Marie Pédrot (Jul 29 2021 at 14:09):

(more generally, I would really like to separate universe constraint extension from constant definition per se)

view this post on Zulip Hugo Herbelin (Jul 29 2021 at 14:10):

Separate universe constraint extension from constant definition: sounds good a priori.

view this post on Zulip Hugo Herbelin (Jul 29 2021 at 14:11):

So, what do you intend to do with constraints between non-variables in poly constants?

view this post on Zulip Pierre-Marie Pédrot (Jul 29 2021 at 14:12):

Leave them around? You have to consider them anyways by transitivity.

view this post on Zulip Pierre-Marie Pédrot (Jul 29 2021 at 14:12):

As soon as you allow constraints between globals and variables, you must allow constraints between globals

view this post on Zulip Pierre-Marie Pédrot (Jul 29 2021 at 14:13):

and the former appear as soon as you mix mono with poly

view this post on Zulip Hugo Herbelin (Jul 29 2021 at 14:13):

Re-asking just to be sure: Do you intend to have the generators of constraints which are between non-variables once for all in the global env, or to re-add them at each use in another contant (and have them only increasing the local "global graph" of a constant)?

view this post on Zulip Pierre-Marie Pédrot (Jul 29 2021 at 14:14):

the second case.

view this post on Zulip Pierre-Marie Pédrot (Jul 29 2021 at 14:14):

i.e. don't change anything to what we have now

view this post on Zulip Pierre-Marie Pédrot (Jul 29 2021 at 14:14):

the first situation is not closed under transitivity

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

if you allow two constants with var < global then by uniformity you must allow constraints between globals

view this post on Zulip Hugo Herbelin (Jul 29 2021 at 14:16):

But then (wrt "the second case"), what to do with what is called monomorphic now? Will it also become "global graph" local to a constant?

view this post on Zulip Pierre-Marie Pédrot (Jul 29 2021 at 14:16):

no

view this post on Zulip Hugo Herbelin (Jul 29 2021 at 14:16):

why not?

view this post on Zulip Pierre-Marie Pédrot (Jul 29 2021 at 14:16):

because you don't want to make everybody polymorphic

view this post on Zulip Pierre-Marie Pédrot (Jul 29 2021 at 14:17):

sometimes you might have constraints local to a definition

view this post on Zulip Pierre-Marie Pédrot (Jul 29 2021 at 14:17):

but this is hard to compute

view this post on Zulip Pierre-Marie Pédrot (Jul 29 2021 at 14:17):

but in general you must have the global graph somewhere

view this post on Zulip Hugo Herbelin (Jul 29 2021 at 14:18):

But then the argument may apply in the other direction. You might want to have polymorphic definitions with global constraints not local to a definition?

view this post on Zulip Pierre-Marie Pédrot (Jul 29 2021 at 14:18):

yes, but this you can do

view this post on Zulip Pierre-Marie Pédrot (Jul 29 2021 at 14:18):

it's already possible today

view this post on Zulip Hugo Herbelin (Jul 29 2021 at 14:19):

But then, you still don't need to keep a notion of monomorphic constant.

view this post on Zulip Pierre-Marie Pédrot (Jul 29 2021 at 14:19):

I agree that in theory you could make everything polymorphic

view this post on Zulip Pierre-Marie Pédrot (Jul 29 2021 at 14:19):

but there is a reason you don't want to do that: efficiency

view this post on Zulip Hugo Herbelin (Jul 29 2021 at 14:20):

This I want to understand.

view this post on Zulip Pierre-Marie Pédrot (Jul 29 2021 at 14:20):

universe polymorphism is extremely costly, and for various reasons

view this post on Zulip Pierre-Marie Pédrot (Jul 29 2021 at 14:20):

if you have to recompute constraints every time you use a constant, even if they are the same, this has a cost

view this post on Zulip Hugo Herbelin (Jul 29 2021 at 14:21):

You mean that even the degenerate form of universe polymorphism is costly?

view this post on Zulip Pierre-Marie Pédrot (Jul 29 2021 at 14:21):

I am not even talking about substitutions

view this post on Zulip Pierre-Marie Pédrot (Jul 29 2021 at 14:21):

not sure what you're talking about

view this post on Zulip Hugo Herbelin (Jul 29 2021 at 14:22):

I mean: is it to re-add the delayed constraints every time which is costly?

view this post on Zulip Pierre-Marie Pédrot (Jul 29 2021 at 14:22):

anyways, I think we should have some live discussion about the topic with other devs working on the same kind of stuff

view this post on Zulip Pierre-Marie Pédrot (Jul 29 2021 at 14:22):

yes

view this post on Zulip Pierre-Marie Pédrot (Jul 29 2021 at 14:22):

but not only, substitution is costly

view this post on Zulip Pierre-Marie Pédrot (Jul 29 2021 at 14:22):

plus you have to store all these instances everywhere

view this post on Zulip Pierre-Marie Pédrot (Jul 29 2021 at 14:23):

"the best proof is the proof you don't write"

view this post on Zulip Pierre-Marie Pédrot (Jul 29 2021 at 14:23):

there is a reason why proof by reflection is efficient

view this post on Zulip Hugo Herbelin (Jul 29 2021 at 14:23):

So, a polymorphic constant which has no delayed constraints (i.e. which is the same as a monomorphic of which the associated graph actually lives on its own declaration) is not costly?

view this post on Zulip Pierre-Marie Pédrot (Jul 29 2021 at 14:24):

this is the same as a monomorphic constraint, barring potential weird code paths

view this post on Zulip Pierre-Marie Pédrot (Jul 29 2021 at 14:24):

but these things don't exist in practice

view this post on Zulip Hugo Herbelin (Jul 29 2021 at 14:25):

The weird code paths are my points. They are consuming useless our energy and makes things more complex to users too.

view this post on Zulip Pierre-Marie Pédrot (Jul 29 2021 at 14:25):

but these things are not in the kernel

view this post on Zulip Pierre-Marie Pédrot (Jul 29 2021 at 14:25):

the problem lies up ahead

view this post on Zulip Pierre-Marie Pédrot (Jul 29 2021 at 14:26):

the kernel is mostly ok, if you forget about the horrible side-effect system

view this post on Zulip Hugo Herbelin (Jul 29 2021 at 14:26):

Yes, the management of "side effect" in the kernel is not easy to follow.

view this post on Zulip Pierre-Marie Pédrot (Jul 29 2021 at 14:26):

it's also wrong

view this post on Zulip Hugo Herbelin (Jul 29 2021 at 14:27):

About the kernel, it would still be better it it had more uniformity. It looks a bit like a draft paper, missing the last week of polishing before submission to reviewers.

view this post on Zulip Hugo Herbelin (Jul 29 2021 at 14:29):

Afaicu, there are still universe problems at the interaction between declare.ml and safe_typing.ml. Cleaning the code would help to find them.

view this post on Zulip Pierre-Marie Pédrot (Jul 29 2021 at 14:29):

Agreed.

view this post on Zulip Pierre-Marie Pédrot (Jul 29 2021 at 14:29):

but it's also due to intricate design issues

view this post on Zulip Pierre-Marie Pédrot (Jul 29 2021 at 14:30):

I have a PR that removes futures from the kernel, but it's a mess in the upper layers

view this post on Zulip Hugo Herbelin (Jul 29 2021 at 14:30):

It seems so.

view this post on Zulip Pierre-Marie Pédrot (Jul 29 2021 at 14:30):

It's not even clear what the invariants are

view this post on Zulip Pierre-Marie Pédrot (Jul 29 2021 at 14:30):

even in the current situation

view this post on Zulip Pierre-Marie Pédrot (Jul 29 2021 at 14:30):

making the code purely functional exposes these issues in plain light

view this post on Zulip Hugo Herbelin (Jul 29 2021 at 14:31):

About making the code purely functional, I fell on some issues too. What are the plans?

view this post on Zulip Pierre-Marie Pédrot (Jul 29 2021 at 14:32):

no idea

view this post on Zulip Pierre-Marie Pédrot (Jul 29 2021 at 14:33):

but we should have some meeting after the summer anyways

view this post on Zulip Hugo Herbelin (Jul 29 2021 at 14:33):

OK

view this post on Zulip Hugo Herbelin (Jul 29 2021 at 14:33):

Back to the kernel, I'm considering also merging push_named_* and add_constant. No objection?

view this post on Zulip Pierre-Marie Pédrot (Jul 29 2021 at 14:34):

dunno, it depends on the final design

view this post on Zulip Pierre-Marie Pédrot (Jul 29 2021 at 14:35):

I'd like some presentation on the topic as well

view this post on Zulip Hugo Herbelin (Jul 29 2021 at 14:36):

Incidentally, about the double status of section variables as local and global objects, I made some progresses, but this is where I blocked on the dependency of proof states on the global environment.

view this post on Zulip Hugo Herbelin (Jul 29 2021 at 14:38):

My current conclusion is that we don't need to define x:=S.x in the goal context but rather S.x:=x outside the goal context!! (where S.x is the global copy of the section variable).

view this post on Zulip Hugo Herbelin (Jul 29 2021 at 14:39):

But for that, we need to be able to modify the env_globals local to an evar...

view this post on Zulip Hugo Herbelin (Jul 29 2021 at 14:40):

which is incompatible with the way it works now.

view this post on Zulip Gaëtan Gilbert (Jul 29 2021 at 14:56):

why are you copying section variables?

view this post on Zulip Hugo Herbelin (Jul 29 2021 at 15:17):

why are you copying section variables?

I used the word "copying" informally. The point is that it we want section variables in a goal to behave like any other goal variable, we need to be able to hide/clear them on demand. But even if we clear them, they continue to be there in the global context, potentially depending in global constants of the section. So, we may need two "copies" (one in the global env for reference from global constants, with say a qualified name, and one in the goal context, with an atomic name). Which one should be called a copy of the other is not clear. (I'm not sure I answer your question though.)

view this post on Zulip Gaëtan Gilbert (Jul 29 2021 at 15:19):

we want section variables in a goal to behave like any other goal variable

do we?

view this post on Zulip Hugo Herbelin (Jul 29 2021 at 16:02):

do we?

A typical situation where "we" (or at least some persons, I don't know how to estimate how many) want to clear a section variable is destruct n where n has been "consumed" and there is no reason to have its name continuing to clutter the name space.

view this post on Zulip Paolo Giarrusso (Jul 29 2021 at 16:25):

Or when a tactic loops and works over all assumptions, so if you exclude a section variable from using, the Qed fails.

view this post on Zulip Paolo Giarrusso (Jul 29 2021 at 16:33):

(I'm sure that point has been brought up before, together with the idea to hide those variables in the upper layers only?)

view this post on Zulip Gaëtan Gilbert (Jul 29 2021 at 16:41):

isn't it just that we want to stop treating section variables as assumptions?


Last updated: Oct 16 2021 at 03:02 UTC