Stream: Coq devs & plugin devs

Topic: Parsing / execution separation


view this post on Zulip Maxime Dénès (Dec 08 2021 at 17:33):

To answer some of your points, @Emilio Jesús Gallego Arias :

view this post on Zulip Enrico Tassi (Dec 08 2021 at 20:25):

Emilio Jesús Gallego Arias said:

for example you know that having parsing to depend on type checking is a long time wish

No. You want the selection of the right AST (among many possible ones, eg having different precedences for /\ and = in a lattice or in Prop) be done by typing. Not have the parser use typing while it parses.

view this post on Zulip Enrico Tassi (Dec 08 2021 at 20:26):

So you don't need to have the parsing environment up-to-date while parsing.

view this post on Zulip Maxime Dénès (Dec 09 2021 at 07:27):

Maxime Dénès said:

I believe this idea is from Georges Gonthier, btw.

view this post on Zulip Enrico Tassi (Dec 09 2021 at 09:14):

About Earley parsing yes. The disambiguation based on typing is "Italian tech" ;-)

view this post on Zulip Enrico Tassi (Dec 09 2021 at 09:15):

(which never worked well because camlp5...)

view this post on Zulip Maxime Dénès (Dec 09 2021 at 13:29):

@Pierre-Marie Pédrot Do you know why syntax extensions are marked as substitutive? https://github.com/coq/coq/blob/master/vernac/metasyntax.ml#L846

view this post on Zulip Maxime Dénès (Dec 09 2021 at 13:29):

They are not really, as witnessed by the identity subst function

view this post on Zulip Pierre-Marie Pédrot (Dec 09 2021 at 13:31):

doesn't it change the kername of the resulting object as well?

view this post on Zulip Pierre-Marie Pédrot (Dec 09 2021 at 13:31):

this we care about

view this post on Zulip Pierre-Marie Pédrot (Dec 09 2021 at 13:32):

(the fact we discard the substitution just means that we're broken for functors, but it still works for import)

view this post on Zulip Maxime Dénès (Dec 09 2021 at 13:35):

Ok, I think it is quizz time (was a long time!)

view this post on Zulip Maxime Dénès (Dec 09 2021 at 13:35):

Module Type T.
Notation F := False.
End T.

Module X : T.
Notation F := True.
End X.

Import X.

Print F.

view this post on Zulip Gaëtan Gilbert (Dec 09 2021 at 13:40):

Maxime Dénès said:

They are not really, as witnessed by the identity subst function

identity is a fine substitution
there doesn't seem to be much benefit to adding a IdentitySubst next to Subst / Keep

view this post on Zulip Maxime Dénès (Dec 09 2021 at 13:44):

Sure, my question is more about semantics. But maybe that's fine too.

view this post on Zulip Maxime Dénès (Dec 09 2021 at 13:48):

Wait, I got completely confused. My question was why are grammar rules extensions declared as substitutive.

view this post on Zulip Maxime Dénès (Dec 09 2021 at 13:49):

(not about "syntactic definitions")

view this post on Zulip Gaëtan Gilbert (Dec 09 2021 at 13:49):

because it works and the other choices don't

view this post on Zulip Pierre-Marie Pédrot (Dec 09 2021 at 13:49):

what would they be otherwise?

view this post on Zulip Pierre-Marie Pédrot (Dec 09 2021 at 13:49):

Keep is broken, Dispose not expressive enough

view this post on Zulip Pierre-Marie Pédrot (Dec 09 2021 at 13:50):

Anticipate, better not talk about it.

view this post on Zulip Pierre-Marie Pédrot (Dec 09 2021 at 13:50):

It's very rare for an object to be Keep.

view this post on Zulip Maxime Dénès (Dec 09 2021 at 13:51):

But Keep seems to have been intended precisely for this kind of object, no? https://github.com/coq/coq/blob/master/dev/doc/changes.md?plain=1#L1836

view this post on Zulip Pierre-Marie Pédrot (Dec 09 2021 at 13:52):

Keep objects are unconditionally cached at the end of a module / functor

view this post on Zulip Pierre-Marie Pédrot (Dec 09 2021 at 13:52):

so if they refer to stuff that is bound, boom

view this post on Zulip Maxime Dénès (Dec 09 2021 at 13:52):

How would a grammar rule refer to a functor object?

view this post on Zulip Gaëtan Gilbert (Dec 09 2021 at 13:53):

Pierre-Marie Pédrot said:

It's very rare for an object to be Keep.

unless they get it from default_object by mistake ;)

view this post on Zulip Gaëtan Gilbert (Dec 09 2021 at 13:53):

Pierre-Marie Pédrot said:

Keep objects are unconditionally cached at the end of a module / functor

no, keep is dropped at the end of modtype/functor

view this post on Zulip Pierre-Marie Pédrot (Dec 09 2021 at 13:53):

when you parse stuff and return a global that is bound in the parameters?

view this post on Zulip Maxime Dénès (Dec 09 2021 at 13:54):

but isn't this the interpretation of the notation?

view this post on Zulip Pierre-Marie Pédrot (Dec 09 2021 at 13:54):

?

view this post on Zulip Maxime Dénès (Dec 09 2021 at 13:54):

I'm talking about inSyntaxExtension, not inNotation.

view this post on Zulip Pierre-Marie Pédrot (Dec 09 2021 at 13:55):

but this can still refer to a name ?

view this post on Zulip Gaëtan Gilbert (Dec 09 2021 at 13:56):

how?

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

hm, it's true that we don't store anything named there AFAICT

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

Keep makes sense when you can have at most one object per instance

view this post on Zulip Maxime Dénès (Dec 09 2021 at 13:59):

You mean by functor instance?

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

yeah

view this post on Zulip Maxime Dénès (Dec 09 2021 at 14:00):

Isn't it the case for these grammar rules?

view this post on Zulip Gaëtan Gilbert (Dec 09 2021 at 14:00):

keep does not survive functors
keep is the same as dispose in functors and module types

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

you get them when you instantiate don't you ?

view this post on Zulip Gaëtan Gilbert (Dec 09 2021 at 14:00):

no

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

(disclaimer: every time I tried to use Keep it was not doing the thing I was looking for)

view this post on Zulip Maxime Dénès (Dec 09 2021 at 14:02):

and when is Keep not the same as Dispose?

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

@Gaëtan Gilbert what's the typical use case for Keep then?

view this post on Zulip Maxime Dénès (Dec 09 2021 at 14:02):

at discharge?

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

well clearly at module closure (but without subst then)

view this post on Zulip Gaëtan Gilbert (Dec 09 2021 at 14:02):

discharge does not run classify_function
keep is not the same as dispose at the end of a module (non functor, non modtype)

view this post on Zulip Maxime Dénès (Dec 09 2021 at 14:03):

Pierre-Marie Pédrot said:

Gaëtan Gilbert what's the typical use case for Keep then?

The doc says grammar rules. But they are Substitutive :D

view this post on Zulip Gaëtan Gilbert (Dec 09 2021 at 14:03):

Pierre-Marie Pédrot said:

Gaëtan Gilbert what's the typical use case for Keep then?

evil
backward compat
waiting for someone to continue https://github.com/coq/coq/pull/9408

view this post on Zulip Gaëtan Gilbert (Dec 09 2021 at 14:03):

maybe I should add it to my libobject pr while I'm breaking stuff

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

I've got a comment that advocates for Keep to escape functors

view this post on Zulip Maxime Dénès (Dec 09 2021 at 14:04):

Yeah, was reading that ^^

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

this is the only sane use case I've ever came upon, and Substitute doesn't work

view this post on Zulip Gaëtan Gilbert (Dec 09 2021 at 14:04):

to break everyone who uses Keep? just make a new classificaton

view this post on Zulip Maxime Dénès (Dec 09 2021 at 14:04):

I guess we know the answer know, you can juste put Dispose

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

what?

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

this doesn't work at all

view this post on Zulip Maxime Dénès (Dec 09 2021 at 14:05):

Keep also didn't, IIUC

view this post on Zulip Gaëtan Gilbert (Dec 09 2021 at 14:05):

Dispose means local

view this post on Zulip Gaëtan Gilbert (Dec 09 2021 at 14:06):

surviving functors would be more like ultraglobal

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

who uses Keep in the current code base then ?

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

beware that it's ultraglobal but substitution-bound

view this post on Zulip Gaëtan Gilbert (Dec 09 2021 at 14:06):

Generalizable Variables
whoever uses default_object without specifying classify_function

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

yeah, but my question is who's that ?

view this post on Zulip Gaëtan Gilbert (Dec 09 2021 at 14:07):

Pierre-Marie Pédrot said:

beware that it's ultraglobal but substitution-bound

what is?

view this post on Zulip Maxime Dénès (Dec 09 2021 at 14:07):

Gaëtan Gilbert said:

Dispose means local

Sure, but when I first read PMP's comment back when I was working on the PR, I thought Keep was already doing what he wanted. In fact, it doesn't.

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

also, are there people using Generalizable variables in modtypes / functors?

view this post on Zulip Gaëtan Gilbert (Dec 09 2021 at 14:07):

who knows

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

@Gaëtan Gilbert every instance of the functor should declare the object for the substitution

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

but when poking inside a functor I also want my libobjects to be locally added

view this post on Zulip Maxime Dénès (Dec 09 2021 at 14:08):

Pierre-Marie Pédrot said:

also, are there people using Generalizable variables in modtypes / functors?

The answer to this kind of questions is always yes.

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

and the answer to who is probably color

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

I know

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

it's the independence of premises of crappy coq features: if somebody uses it, then color uses it.

view this post on Zulip Gaëtan Gilbert (Dec 09 2021 at 14:09):

Pierre-Marie Pédrot said:

and the answer to who is probably color

nope https://github.com/fblanqui/color/search?q=Generalizable

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

incredibile

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

by contrapositive, the answer is then no

view this post on Zulip Maxime Dénès (Dec 09 2021 at 14:12):

btw, the reason I'm asking all this is that this "fake substitivity" makes it necessary to use the infamous ModSubstObjs for both parsing and execution

view this post on Zulip Maxime Dénès (Dec 09 2021 at 14:12):

with the set_missing_handler poetry

view this post on Zulip Gaëtan Gilbert (Dec 09 2021 at 14:14):

I'm happy to say that I don't know what that is

view this post on Zulip Maxime Dénès (Dec 09 2021 at 14:16):

https://github.com/coq/coq/blob/master/vernac/declaremods.ml#L76

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

forbidden knowledge

view this post on Zulip Maxime Dénès (Dec 09 2021 at 14:16):

I don't know how it works or what fundamental problem it solves, though.

view this post on Zulip Maxime Dénès (Dec 09 2021 at 14:16):

@Pierre-Marie Pédrot do you know more?

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

I think I used to know, but I am also happy for my sanity to have forgotten

view this post on Zulip Maxime Dénès (Dec 09 2021 at 14:17):

(I was precisely hoping that grammar rules were not stored there, but since they are substitutive...)

view this post on Zulip Maxime Dénès (Dec 09 2021 at 14:18):

The comment does say: Such missing entries may come from inner parts of module
types, which aren't registered by the standard libobject machinery.

view this post on Zulip Maxime Dénès (Dec 09 2021 at 14:19):

but it kind of begs the question: why? :)

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

the commit message of 466c4cb gives a tiny bit more info

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

this is to save memory use

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

we probably can't store a delayed structure there because marshalling

view this post on Zulip Enrico Tassi (Dec 09 2021 at 14:23):

Maxime Dénès said:

Module Type T.
Notation F := False.
End T.

Module X : T.
Notation F := True.
End X.

Import X.

Print F.

Isn't the answer irrelevant for parsing? (the interpretation changes, but not the parsing rule)

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

Given that there are no parsing rules added in this example...

view this post on Zulip Maxime Dénès (Dec 09 2021 at 14:23):

Yes, that's why I wrote I got confused. The question is valid, I guess, but for syndefs.

view this post on Zulip Enrico Tassi (Dec 09 2021 at 14:23):

Well, right... syndefs add no parsing rule

view this post on Zulip Enrico Tassi (Dec 09 2021 at 14:24):

But I take home that the parsing rules are the one from the signature, not the body

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

in general, any data should come from the signature, anything else is buggy

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

obviously we can't enforce that and this is a serious problem for proper programming languages that are not gallina

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

i.e. LtacX

view this post on Zulip Maxime Dénès (Dec 09 2021 at 14:25):

In fact, I can tell you what contributed to my confusion. Look at the name of the classification function for syntactic extensions (i.e. grammar rules) : https://github.com/coq/coq/blob/master/vernac/metasyntax.ml#L845

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

there sure are psychopaths in the Coq dev team

view this post on Zulip Enrico Tassi (Dec 09 2021 at 14:26):

eh eh

view this post on Zulip Enrico Tassi (Dec 09 2021 at 14:26):

let pipe = "not a pipe"

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

this wins the yearly "let's mess with the brain of the readers" award

view this post on Zulip Maxime Dénès (Dec 09 2021 at 14:28):

It worked on mine, at least. But I have been connected a bit too much with the real world, lately. Became less resistant.

view this post on Zulip Enrico Tassi (Dec 09 2021 at 14:28):

let (+) = (-) in ...

view this post on Zulip Enrico Tassi (Dec 09 2021 at 14:28):

I'll sneak that one in the middle of a file fiddling with De Bruijn indexes

view this post on Zulip Maxime Dénès (Dec 09 2021 at 14:29):

Maybe a good old let rel0 = Rel 1, then?

view this post on Zulip Enrico Tassi (Dec 09 2021 at 14:49):

a smarter constructor let mkRel x = Rel (x mod 7)

view this post on Zulip Gaëtan Gilbert (Dec 09 2021 at 14:54):

not let mkRel x = Rel (String.hash (string_of_int x))?

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

much safer, way less collisions!

view this post on Zulip Enrico Tassi (Dec 09 2021 at 15:01):

we should definitely do | Rel of float

view this post on Zulip Gaëtan Gilbert (Dec 09 2021 at 15:01):

is lift 1.0 (lift 2.0 x) the same as lift 3.0 x?

view this post on Zulip Enrico Tassi (Dec 09 2021 at 15:02):

no, but lift 1.5 (lift 1.5 x) surely is

view this post on Zulip Enrico Tassi (Dec 09 2021 at 15:02):

This thread is really killing my productivity ;-)

view this post on Zulip Gaëtan Gilbert (Dec 09 2021 at 15:03):

let equal_up_to_rel x y = equal (lift infty x) (lift infty y)

view this post on Zulip Gaëtan Gilbert (Dec 09 2021 at 15:03):

for free!

view this post on Zulip Pierre-Marie Pédrot (Dec 09 2021 at 15:03):

but it's enhancing your morale, so in the end you're more productive globallly

view this post on Zulip Maxime Dénès (Dec 09 2021 at 15:56):

You're such a master of management tricks, PMP

view this post on Zulip Maxime Dénès (Dec 09 2021 at 16:34):

Naive question: the code of Declaremods, e.g. the computation of functor substitutions, is not in the TCB?

view this post on Zulip Paolo Giarrusso (Dec 09 2021 at 20:12):

also, are there people using Generalizable variables in modtypes / functors?

If just having the flag set counts, I've done it, since I load stdpp and use modules. Is that bad?

view this post on Zulip Paolo Giarrusso (Dec 09 2021 at 20:13):

Or need one change the settings inside a functor? Not planning to.

view this post on Zulip Gaëtan Gilbert (Dec 09 2021 at 20:35):

a good chunk of the ci libobjects seem to use keep
not sure how much is intentional

view this post on Zulip Maxime Dénès (Dec 09 2021 at 20:52):

It would be surprising that it is all intentional :)

view this post on Zulip Maxime Dénès (Dec 09 2021 at 20:52):

FTR, separating parsing and execution gets tricky with module name substitutions, because of the infamous delta resolvers

view this post on Zulip Maxime Dénès (Dec 09 2021 at 20:53):

@Pierre-Marie Pédrot I remember you had started to work on replacing these by an equiv relation in the logical environment IIRC

view this post on Zulip Jason Gross (Dec 10 2021 at 05:43):

@Maxime Dénès you mentioned in the other thread that parsing does not depend on interpretation, but if Bind Scope works correctly I don't think this can possibly be the case. Consider

Definition foo n := eq_refl : n = 0.

Does the first argument to foo get stuffed in nat_scope? If it does, then I think this requires interpretation to decide (and if you think not, then just replace 0 with ltac:(exact 0) or something). Furthermore, you can bind some syntax to one custom entry in nat_scope and a different one in type_scope, I believe, and hence the parsing of applications of foo will depend on what type gets inferred for foo. (I haven't checked this, though, and I'm not at a computer right now; can someone test it for me?)

view this post on Zulip Jason Gross (Dec 10 2021 at 05:48):

Naive question: the code of Declaremods, e.g. the computation of functor substitutions, is not in the TCB?

It would make sense to me that this is not in the TCB, because AIUI there is no way to prove False by doing something evil in functor substitutions. Definitions and proofs in functors sort-of don't exist as real objects (conceptually / mathematically) until you instantiate the functor, right?

view this post on Zulip Guillaume Melquiond (Dec 10 2021 at 05:52):

Jason Gross said:

Does the first argument to foo get stuffed in nat_scope? If it does, then I think this requires interpretation to decide

Sure, but Coq is a read-evaluate-process loop. It alternates parsing and interpretation. So, n will indeed be in nat_scope, but only for subsequent vernacular commands. For the currently parsed command, interpretation does not matter.

view this post on Zulip Jason Gross (Dec 10 2021 at 05:55):

Oh, is this why implicit status on context variable types only works after the end of the Context command? And I take it scopes are the same?

view this post on Zulip Jason Gross (Dec 10 2021 at 05:57):

Like Context (foo : forall n, n = 1%nat) (bar : foo (1 + 1) = foo 2) will not work if you close nat_scope, but Context (foo : forall n, n = 1%nat). Context (bar : foo (1 + 1) = foo 2) will? (I haven't tested this)

view this post on Zulip Jason Gross (Dec 10 2021 at 05:59):

FTR, separating parsing and execution gets tricky with module name substitutions, because of the infamous delta resolvers

What does this mean, and what are delta resolvers?

view this post on Zulip Guillaume Melquiond (Dec 10 2021 at 06:23):

Jason Gross said:

Oh, is this why implicit status on context variable types only works after the end of the Context command? And I take it scopes are the same?

Most certainly.

view this post on Zulip Enrico Tassi (Dec 10 2021 at 06:52):

The parser does not know about types. Scopes pick notation interpretations, not grammar rules, and that happens after parsing.

Indeed you can't set the same infix at different levels, even if the scopes are different. You can do that in different grammars, but that are not selected by the type.

view this post on Zulip Maxime Dénès (Dec 10 2021 at 07:26):

Jason Gross said:

you can bind some syntax to one custom entry in nat_scope and a different one in type_scope, I believe

I hope not, because indeed it would probably make the separation impossible.

view this post on Zulip Maxime Dénès (Dec 10 2021 at 07:28):

Or maybe they'd end up being actually two different entries at the grammar level?

view this post on Zulip Jason Gross (Dec 10 2021 at 07:35):

Are you saying that the following (untested) doesn't work?

Notation "[[ x ]]" := x (x in custom foo) : nat_scope.
Notation "[[ x ]]" := x (x in custom bar) : type_scope.

(or whatever the syntax is)

view this post on Zulip Enrico Tassi (Dec 10 2021 at 08:00):

I hope it does not, and if it does, we should ditch it.

view this post on Zulip Enrico Tassi (Dec 10 2021 at 08:01):

Seriously, the parser does not know scopes. End of the story.

view this post on Zulip Enrico Tassi (Dec 10 2021 at 08:05):

Declare Custom Entry foo.
Declare Custom Entry bar.
Notation "'a'" := 1 (in custom foo).
Notation "'b'" := 2 (in custom bar).
Notation "[[ x ]]" := x (x custom foo) : nat_scope.
Notation "[[ x ]]" := x (x custom bar) : type_scope.

Check [[ a ]]%nat.
Check [[ a ]]%type. (* prints 1 *)
Fail Check [[ b ]]%nat. (* error: [custom:foo] expected *)
Fail Check [[ b ]]%type. (* error: [custom:foo] expected *)

No error is given at notation declaration time, but it does not (and it can't possibly) work. CC @Hugo Herbelin

view this post on Zulip Enrico Tassi (Dec 10 2021 at 08:06):

So the asteroid missed Earth by just one light year \o/

view this post on Zulip Enrico Tassi (Dec 10 2021 at 08:11):

Anyway, the refman is correct about scopes, they affect the interpretation of notations, not their presence in the grammar.

view this post on Zulip Enrico Tassi (Dec 10 2021 at 08:16):

About the foo example, the phase after parsing, interning (or globalization) will resolve "foo" as a GlobRef.Const and to that name one can associate interpretation scopes for the arguments.

So, @Maxime Dénès, the example of @Jason Gross shows that running globalization (alone, without interpretation/typing) once we have the AST is not possible as is (since one needs to type check foo in order to infer scopes for the arguments, which in turns are needed to globalize terms using foo since globalization also performs notation interpretation which depends on scopes).
I mean this foo: Definition foo n := eq_refl : n = 0.

view this post on Zulip Maxime Dénès (Dec 10 2021 at 08:19):

Sure, but functors already made that "trivially impossible" :)

view this post on Zulip Enrico Tassi (Dec 10 2021 at 08:20):

Dunno, not for the same reason I hope.

view this post on Zulip Maxime Dénès (Dec 10 2021 at 08:21):

Computing names of constants requires typing.

view this post on Zulip Enrico Tassi (Dec 10 2021 at 08:21):

Are we talking about C++ and templates, or Coq here?

view this post on Zulip Maxime Dénès (Dec 10 2021 at 08:23):

Unfortunately, today module name substitutions and constant name substitutions are mixed, so even computing module names (which does have an impact on parsing because they can contain grammar rules) requires typing.

view this post on Zulip Maxime Dénès (Dec 10 2021 at 08:24):

The culprit is the following line: https://github.com/coq/coq/blob/master/vernac/declaremods.ml#L486

view this post on Zulip Enrico Tassi (Dec 10 2021 at 08:25):

Hum, I see, but it seems less fundamental (I mean, it is because of the implementation, not because of the spec)

view this post on Zulip Enrico Tassi (Dec 10 2021 at 08:26):

Oh, delta resolvers... not worrying anymore, we should grep for omicron resolvers

view this post on Zulip Maxime Dénès (Dec 10 2021 at 08:26):

Enrico Tassi said:

Hum, I see, but it seems less fundamental (I mean, it is because of the implementation, not because of the spec)

Yes, that's why I wrote "today" :)

view this post on Zulip Enrico Tassi (Dec 10 2021 at 08:26):

Didn't someone try to purge delta resolvers?

view this post on Zulip Maxime Dénès (Dec 10 2021 at 08:27):

That's what I wrote above, @Pierre-Marie Pédrot was working on replacing them with something in the logical env IIRC

view this post on Zulip Maxime Dénès (Dec 10 2021 at 08:28):

I don't recall hearing news about this line of work, but I've missed a lot of things in the last months.

view this post on Zulip Maxime Dénès (Dec 10 2021 at 08:31):

I hope we can also phase the computation of these substitutions:

  1. Compute the pure module name substitution
  2. Enrich it with delta resolver info (which includes constant inlining)

So 1. would be done at parsing time, 2. would require typing

view this post on Zulip Hugo Herbelin (Dec 10 2021 at 09:28):

Regarding the cc above:

Seriously, the parser does not know scopes. End of the story.

Indeed, the parser does not know scopes and the fact that %key comes after the expression is a problem. At some time, I was imagining that we could require that notations respect the invariant that expressions are always well-parenthesized for some class of parentheses including (/), [[, ]] etc. Then, we could apply a first phase of parsing which detects the ( ... )%foo, or [[ ... ]]%foo blocks and have the scopes parsed in the appropriate entry.

Hardwiring a notion of matching parentheses in the parser is probably worth, since, after all, it is also an important aspect of how human eyes are parsing expressions. And there are only a few standard notations around which do not respect parentheses (e.g. the Dirac notation[b〉, but even for this notation, we could find a way to accept it in a system that hardwire a notion of matching parentheses).

No error is given at notation declaration time, but it does not (and it can't possibly) work.

Apparently a regression. In 8.11, there was an error. Thanks for telling.

view this post on Zulip Hugo Herbelin (Dec 10 2021 at 09:29):

Incidentally, once all issues involved in separating parsing from typing are collected, that would be useful to collect them somewhere!

view this post on Zulip Maxime Dénès (Dec 10 2021 at 09:35):

Yes, absolutely, that's the point of the exploration I'm working on.

view this post on Zulip Enrico Tassi (Dec 10 2021 at 14:31):

@Hugo Herbelin in general it is not possible, IMO, to use scopes in the parser. This is what the example of jason shows us, it is not just that the scopes are postfix and we parse using an LL engine.

If you parse foo x, the scope of x is (or may be) given by the metadata attached to foo. You would need the parser to do the globalization phase (eg carry a context of bound variables, access the nametab...) to figure out that foo is a global constant, then access the Arguments database for argument scopes attached to foo and finally pick the right non terminal for parsing x based on the scope active on the argument, if any.

This is really too much for a parser.

view this post on Zulip Hugo Herbelin (Dec 10 2021 at 15:59):

@Enrico Tassi : Good point. Having the parser dependent of implicit scopes would indeed require further ideas.

view this post on Zulip Paolo Giarrusso (Dec 10 2021 at 17:28):

And even with those extensions, the parser wouldn't understand typing, so a polymorphic function is enough to defeat it...

view this post on Zulip Gaëtan Gilbert (Dec 10 2021 at 17:29):

internalization doesn't understand polymorphism either
@id T x won't use T for the scope of x

view this post on Zulip Paolo Giarrusso (Dec 10 2021 at 17:38):

I know, that's the thing I was hinting at... it doesn't seem scopes can solve this, and it comes up in let x : list N := map (fun x => x + 1)%N xs in ...

view this post on Zulip Jason Gross (Dec 10 2021 at 18:51):

Are delta resolvers about Parameter Inline?

view this post on Zulip Pierre-Marie Pédrot (Dec 10 2021 at 18:52):

nope

view this post on Zulip Pierre-Marie Pédrot (Dec 10 2021 at 18:52):

(well, they do contain the inlining information but it's somewhat irrelevant)

view this post on Zulip Pierre-Marie Pédrot (Dec 10 2021 at 18:53):

they're just a way to associate kernel names, so they're used every time you have functors and include

view this post on Zulip Pierre-Marie Pédrot (Dec 10 2021 at 18:54):

as the name implies, they sort-of make true more δ-conversions between constants

view this post on Zulip Gaëtan Gilbert (Dec 10 2021 at 18:54):

and Module N := M. no?

view this post on Zulip Pierre-Marie Pédrot (Dec 10 2021 at 18:54):

also, yes

view this post on Zulip Pierre-Marie Pédrot (Dec 10 2021 at 18:54):

everything that introduces name aliasing

view this post on Zulip Jason Gross (Dec 10 2021 at 18:54):

So this is how you can unify inductive types across includes? (Also Qed-opaque lemmas and axioms?)

view this post on Zulip Pierre-Marie Pédrot (Dec 10 2021 at 18:54):

yes

view this post on Zulip Pierre-Marie Pédrot (Dec 10 2021 at 18:54):

I was about to say that actually

view this post on Zulip Jason Gross (Dec 10 2021 at 18:55):

And this requires typing somehow?

view this post on Zulip Pierre-Marie Pédrot (Dec 10 2021 at 18:55):

the litmus test to check for aliasing are inductive types, because there is really no other way to make two inductive equal

view this post on Zulip Pierre-Marie Pédrot (Dec 10 2021 at 18:55):

no, that's just a kind of association map

view this post on Zulip Pierre-Marie Pédrot (Dec 10 2021 at 18:56):

we can add mappings saying "the true value of this global entry is that other global"

view this post on Zulip Pierre-Marie Pédrot (Dec 10 2021 at 18:56):

needless to say, it's probably replete with soundness bugs

view this post on Zulip Gaëtan Gilbert (Dec 10 2021 at 18:57):

Jason Gross said:

So this is how you can unify inductive types across includes? (Also Qed-opaque lemmas and axioms?)

opaques and axioms get a definition

Module M.
  Axiom x : nat.
End M.

Module N := M.

Print N.x. (* N.x = M.x *)
Compute N.x. (* = M.x *)

view this post on Zulip Jason Gross (Dec 10 2021 at 18:57):

Oh, interesting, I was not aware that this is how they were implemented

view this post on Zulip Jason Gross (Dec 10 2021 at 18:58):

I guess you can't do this with inductives and constructors because otherwise you couldn't use constructors for pattern matching

view this post on Zulip Gaëtan Gilbert (Dec 10 2021 at 18:58):

nb axioms are also equated by the delta resolver thing:

Goal N.x = M.x.
  match goal with |- ?a = ?a => idtac end.

view this post on Zulip Pierre-Marie Pédrot (Dec 10 2021 at 18:59):

no, even inductive types cannot be aliased through definitions

view this post on Zulip Pierre-Marie Pédrot (Dec 10 2021 at 18:59):

there is a famous error in the kernel saying that this stuff is not implemented

view this post on Zulip Pierre-Marie Pédrot (Dec 10 2021 at 18:59):

so we need kernel support for inductive aliasing

view this post on Zulip Pierre-Marie Pédrot (Dec 10 2021 at 18:59):

@Gaëtan Gilbert that's another problem

view this post on Zulip Pierre-Marie Pédrot (Dec 10 2021 at 19:00):

this works because it was designed for this to work, and not through delta resolvers

view this post on Zulip Pierre-Marie Pédrot (Dec 10 2021 at 19:00):

Ltac doesn't see the delta resolvers, just constants

view this post on Zulip Pierre-Marie Pédrot (Dec 10 2021 at 19:00):

but because we compare canonical names, tadaa

view this post on Zulip Pierre-Marie Pédrot (Dec 10 2021 at 19:00):

(this is a HUGE PITA btw)

view this post on Zulip Paolo Giarrusso (Dec 10 2021 at 19:28):

BTW is that definition a real one, or is it a special alias that Print is lying about?

view this post on Zulip Paolo Giarrusso (Dec 10 2021 at 19:29):

Strangely enough, dnets seem to consider such definitions as automatically hint opaque, and IIRC some commands (like Locate?) knows they're special cc @Janno

view this post on Zulip Gaëtan Gilbert (Dec 10 2021 at 19:33):

there's the user equality and the canonical equality, they're only canonical-equal
env lookup uses user equality
transparent state lookup uses canonical equality

view this post on Zulip Pierre-Marie Pédrot (Dec 10 2021 at 21:58):

@Paolo Giarrusso for inductive types, a bit of both

view this post on Zulip Pierre-Marie Pédrot (Dec 10 2021 at 21:58):

the environment contains two different definitions which are the same up to a name substitution

view this post on Zulip Pierre-Marie Pédrot (Dec 10 2021 at 21:59):

given that we've already forgotten to substitute some fields of the inductive blocks in the past and that we have fancy checker bugs, I wouldn't bet much on the fact we actually have any spec for this

view this post on Zulip Paolo Giarrusso (Dec 10 2021 at 22:00):

Hm, my example involved a plain axiom, a module, and an alias from Include (yes, you warned me)

view this post on Zulip Pierre-Marie Pédrot (Dec 10 2021 at 22:00):

(I am thinking about https://github.com/coq/coq/issues/7609 FTR)

view this post on Zulip Pierre-Marie Pédrot (Dec 10 2021 at 22:01):

@Paolo Giarrusso "why do you hit yourself with a hammer? because it feels so good when I stop"

view this post on Zulip Paolo Giarrusso (Dec 10 2021 at 22:01):

I mostly only include module types!

view this post on Zulip Paolo Giarrusso (Dec 10 2021 at 22:02):

I'll happily stop if you give me Scala-like mixins, or just give me a good way to interleave axioms and definitions in an interface.

view this post on Zulip Pierre-Marie Pédrot (Dec 10 2021 at 22:03):

the worst part of this request is that it probably doesn't even need any kind of kernel support

view this post on Zulip Paolo Giarrusso (Dec 10 2021 at 22:03):

(not really excited to copy-paste the definitions in the implementation, assuming that even works; I've seen different bugs there)

view this post on Zulip Pierre-Marie Pédrot (Dec 10 2021 at 22:04):

the other discussion about Load-ing sections shows that there is a serious need for "mass abstraction"

view this post on Zulip Pierre-Marie Pédrot (Dec 10 2021 at 22:05):

I don't think it's that hard to design, but there are several competing proposals for this kind of feature

view this post on Zulip Pierre-Marie Pédrot (Dec 10 2021 at 22:06):

contrarily to some other devs I am not really afraid about redundant Coq features, e.g. CS vs. TC

view this post on Zulip Paolo Giarrusso (Dec 10 2021 at 22:06):

If you have an idea I'd be interested, but I wasn't very hopeful: my first blocker when I tried to think it through is that you risk needing termination checking across functors

view this post on Zulip Pierre-Marie Pédrot (Dec 10 2021 at 22:06):

if you have a precise design in mind, please open a CEP

view this post on Zulip Pierre-Marie Pédrot (Dec 10 2021 at 22:06):

yes, positivity / guardedness is not modular

view this post on Zulip Paolo Giarrusso (Dec 10 2021 at 22:06):

On this point I don't, but I'll keep that in mind

view this post on Zulip Paolo Giarrusso (Dec 10 2021 at 22:07):

Re redundancy, the problem is the maintenance cost and feature interactions

view this post on Zulip Pierre-Marie Pédrot (Dec 10 2021 at 22:07):

well, we've been maintaining horrible stuff in the Coq code so a bit more isn't going to kill us

view this post on Zulip Paolo Giarrusso (Dec 10 2021 at 22:08):

You joke about hammers, but it's hard to tell apart the good features from the bad ones :upside_down:

view this post on Zulip Pierre-Marie Pédrot (Dec 10 2021 at 22:08):

at least we should have an explicit marking of features à la Rust nightly

view this post on Zulip Paolo Giarrusso (Dec 10 2021 at 22:08):

list of stable features := [] ?

view this post on Zulip Paolo Giarrusso (Dec 10 2021 at 22:09):

nah I guess ssreflect’s pretty good until mixed with TCs :-D

view this post on Zulip Pierre-Marie Pédrot (Dec 10 2021 at 22:10):

my point is that there are a lot of small things that are 1. easy to implement 2. out of the kernel , that would make the life of our users much easier

view this post on Zulip Pierre-Marie Pédrot (Dec 10 2021 at 22:11):

for instance, the non-modularity of positivity / guardedness only matters if you want the abstraction to be statically type-checked

view this post on Zulip Pierre-Marie Pédrot (Dec 10 2021 at 22:11):

if you were to check at runtime that all instances are fine, who cares ?

view this post on Zulip Paolo Giarrusso (Dec 10 2021 at 22:12):

but IIRC that’s not really how functors work, right? Still, I can fix that problem with manual desugaring, so pretyper or elpi might be able to as well

view this post on Zulip Pierre-Marie Pédrot (Dec 10 2021 at 22:12):

Functors are (un)fortunately statically checked

view this post on Zulip Pierre-Marie Pédrot (Dec 10 2021 at 22:12):

so, your salvation won't lie in functors

view this post on Zulip Paolo Giarrusso (Dec 10 2021 at 22:13):

but I really don’t want the abstractions to leave traces in terms :-|

view this post on Zulip Pierre-Marie Pédrot (Dec 10 2021 at 22:13):

not sure what you mean

view this post on Zulip Pierre-Marie Pédrot (Dec 10 2021 at 22:13):

you could encompass a different kind of functor system

view this post on Zulip Paolo Giarrusso (Dec 10 2021 at 22:14):

and I _can_ mix axioms and definitions in a module type, as long as I close and open a new one, every time I switch across the two…

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

where you have no guarantee that applying a functor to an argument will succeed

view this post on Zulip Paolo Giarrusso (Dec 10 2021 at 22:14):

hmmmmm, this kinda hurts my ML-module-system sensibilities, but maaaybe?

view this post on Zulip Paolo Giarrusso (Dec 10 2021 at 22:15):

what I meant was that replacing functors with “runtime” abstraction produces bigger terms

view this post on Zulip Pierre-Marie Pédrot (Dec 10 2021 at 22:15):

at some point you have to bite the bullet: ML is not MLTT

view this post on Zulip Pierre-Marie Pédrot (Dec 10 2021 at 22:15):

ah, yes

view this post on Zulip Paolo Giarrusso (Dec 10 2021 at 22:15):

I _think_ MLTT has much more modular typechecking, except maybe inductives

view this post on Zulip Pierre-Marie Pédrot (Dec 10 2021 at 22:15):

but then if you had an external metaprogramming feature that looks like modules, tastes like module, but is the canada-dry of statically typed modules you wouldn't see the terms in the abstraction either

view this post on Zulip Pierre-Marie Pédrot (Dec 10 2021 at 22:16):

MLTT has much more modular typechecking

ah, sweet summer child

view this post on Zulip Pierre-Marie Pédrot (Dec 10 2021 at 22:16):

MLTT is catastrophical from the point of view of abstraction

view this post on Zulip Pierre-Marie Pédrot (Dec 10 2021 at 22:16):

you may depend on the computational content of a term without any way to control that

view this post on Zulip Paolo Giarrusso (Dec 10 2021 at 22:16):

at least Agda does not normalize during guardedness checking

view this post on Zulip Paolo Giarrusso (Dec 10 2021 at 22:17):

yes, I understand how translucent definitions work

view this post on Zulip Pierre-Marie Pédrot (Dec 10 2021 at 22:17):

but that's only the beginning

view this post on Zulip Pierre-Marie Pédrot (Dec 10 2021 at 22:17):

then you have universes

view this post on Zulip Pierre-Marie Pédrot (Dec 10 2021 at 22:17):

and as you mention, positivity / guardedness

view this post on Zulip Paolo Giarrusso (Dec 10 2021 at 22:17):

universes and guardedness aren’t a modularity problem in Agda.

view this post on Zulip Pierre-Marie Pédrot (Dec 10 2021 at 22:18):

fair enough, but you pay for it

view this post on Zulip Pierre-Marie Pédrot (Dec 10 2021 at 22:18):

I don't think that people are happy to have to explictly quantify over universes

view this post on Zulip Pierre-Marie Pédrot (Dec 10 2021 at 22:18):

(and it's still non-modular in some sense)

view this post on Zulip Paolo Giarrusso (Dec 10 2021 at 22:19):

agreed, by copy-pasting your map function or having to use (unsafe?) sized types

view this post on Zulip Pierre-Marie Pédrot (Dec 10 2021 at 22:19):

(zomfg: I've written everything using Set but I actually wanted to refer to Set1)

view this post on Zulip Paolo Giarrusso (Dec 10 2021 at 22:19):

I just meant that Agda is (closer to) separate typechecking/compilation in Cardelli’s sense.

view this post on Zulip Paolo Giarrusso (Dec 10 2021 at 22:19):

different set of problems, of course.

view this post on Zulip Pierre-Marie Pédrot (Dec 10 2021 at 22:19):

I hear the complaint

view this post on Zulip Paolo Giarrusso (Dec 10 2021 at 22:21):

re Agda universes, they’re annoying, but idiomatic Agda always works, and I can’t say the same for Coq

view this post on Zulip Paolo Giarrusso (Dec 10 2021 at 22:22):

but I can’t comment on those fairly since I haven’t yet really attempted to understand them in anger, I just call my universe colleagues

view this post on Zulip Pierre-Marie Pédrot (Dec 10 2021 at 22:22):

what do you have in mind?

view this post on Zulip Pierre-Marie Pédrot (Dec 10 2021 at 22:23):

"Agda is a proof assistant designed to prove the strong termination of the simply-typed λ-calculus"

view this post on Zulip Pierre-Marie Pédrot (Dec 10 2021 at 22:23):

I've never seen a convincing proof of scalability for Agda, so you cannot convince me that "idiomatic Agda always works"

view this post on Zulip Pierre-Marie Pédrot (Dec 10 2021 at 22:24):

(relatedly, I am actively looking forward to the WITS talk https://popl22.sigplan.org/details/wits-2022-papers/6/Using-Dependent-Types-at-Scale-Maintaining-the-Agda-Standard-Library)

view this post on Zulip Paolo Giarrusso (Dec 10 2021 at 22:24):

I agree, sorry, pattern matching and definitional equality are not sufficient tactics, and performance isn’t acceptable. but I mean universes in Agda

view this post on Zulip Paolo Giarrusso (Dec 10 2021 at 22:25):

there’s 3-4 rules and everybody understands them (and there’s forcing for datatypes, okay). Contrast with https://gitlab.mpi-sws.org/iris/stdpp/-/issues/80.

view this post on Zulip Pierre-Marie Pédrot (Dec 10 2021 at 22:25):

oh, but that's a problem with Coq stdlib

view this post on Zulip Paolo Giarrusso (Dec 10 2021 at 22:26):

for the rest, you’ll have to ask Janno or Gregory, I just know somebody complains about universes once a week I think

view this post on Zulip Gaëtan Gilbert (Dec 10 2021 at 22:26):

agda universes are pretty smilar to Lean universes right? except for prop predicativity

view this post on Zulip Pierre-Marie Pédrot (Dec 10 2021 at 22:26):

unfortunately I'm part of the people who eat universe poly on a daily-ish basis, and they're hellish

view this post on Zulip Pierre-Marie Pédrot (Dec 10 2021 at 22:27):

but the fully-explicit style of Agda doesn't scale much either

view this post on Zulip Paolo Giarrusso (Dec 10 2021 at 22:27):

explicit universe polymorphism + algebraic universes + no special universe inference (beyond the usual I think?)

view this post on Zulip Pierre-Marie Pédrot (Dec 10 2021 at 22:27):

in Coq you can also be fully explicit (barring the poor implementation) and it's still not usable, even assuming we had support from the system

view this post on Zulip Paolo Giarrusso (Dec 10 2021 at 22:28):

but as I said upfront: I don’t understand the universe problems we ran into Coq. Separation of concerns, you know.

view this post on Zulip Paolo Giarrusso (Dec 10 2021 at 22:29):

oh, forgot: Agda has no implicit cumulativity.

view this post on Zulip Pierre-Marie Pédrot (Dec 10 2021 at 22:30):

(my personal taste about implicit cumulativity depends on the time of the day, at some point I am convinced it's critical, at other points I am convinced this is the worst idea ever)

view this post on Zulip Gaëtan Gilbert (Dec 10 2021 at 22:31):

it would be nice to have a flag to disable it
but we need to be able to put algebraics in instances first I think

view this post on Zulip Pierre-Marie Pédrot (Dec 10 2021 at 22:31):

(my educated guess is that your belief is conditioned on your current hat, i.e. whether you're using type theory or you're implementing it)

view this post on Zulip Gaëtan Gilbert (Dec 10 2021 at 22:31):

which hat has which belief?

view this post on Zulip Pierre-Marie Pédrot (Dec 10 2021 at 22:33):

√2/2 implementor + e^π user

view this post on Zulip Enrico Tassi (Dec 11 2021 at 12:38):

totally irrational

view this post on Zulip Jason Gross (Dec 12 2021 at 20:20):

@Paolo Giarrusso Related feature requests:

view this post on Zulip Paolo Giarrusso (Dec 12 2021 at 20:45):

I'm actually now wondering how close you can get with sharing constraints plus submodules...

view this post on Zulip Paolo Giarrusso (Dec 12 2021 at 20:48):

That is, https://sympa.inria.fr/sympa/arc/coq-club/2021-11/msg00016.html deserves further study.

view this post on Zulip Paolo Giarrusso (Dec 12 2021 at 20:55):

Hm no, neither that nor Include constants is really enough; if you go this way, you might end up with MixML.

view this post on Zulip Paolo Giarrusso (Dec 12 2021 at 21:14):

For instance, in the following (terrible) sketch of a POSIX interface, holes and definitions alternate, so your definitions are an _input_ to the body. (Please ignore the actual spec, I’ve never worked on POSIX specs). Splitting the definitions would be the logical next step.

Module Type posix_interface.
  Parameter page_size : N.

  Definition page_aligned (vaddr : N) : Prop := 
  Definition page_aligned_addr : Type := { va | page_aligned va }.

  Parameter page_mapping : page_aligned_addr -> mpred. (* mpred is the type of propositions of some separation logic. *)

  (* Part-of separation-logic spec for mmap*)
  Definition mmap_spec :=
    \arg{va : page_aligned_addr} (* lots of other args *)
    \post page_mapping va.
End posix_interface.

Module Type posix_interface_x86.
  Include posix_interface(constants).
  (* Define page_size *)
End posix_interface_x86.

Module Type posix_interface_linux.
  Include posix_interface(constants).
  (* Define page_mapping, covering OS state. *)
End Type posix_interface_linux.

Module posix_interface_x86_linux.
  Include posix_interface_x86(constants).
  Include posix_interface_linux(constants).
  (* Making sense of this combination requires mixing linearization; intuitively, it’s sound because the definitions aren’t conflicting, but in fact we can just detect the diamond and remove duplicates. *)
  (* I’m ignoring architecture-specific components of page mappings for simplicity. *)
End posix_interface_x86.

view this post on Zulip Paolo Giarrusso (Dec 12 2021 at 21:15):

the above example is slightly made-up, but I do run into similar (dependent) problems.

view this post on Zulip Paolo Giarrusso (Dec 12 2021 at 21:24):

so, you see, when I joke that I’d want Scala in Coq, I’m not 100% joking. OTOH I have an encoding of the above, and that coq-club post might make it better…

view this post on Zulip Maxime Dénès (Dec 13 2021 at 09:44):

I think I managed to separate the two phases in the module system. Now I have to deal with plugins, to complete the POC.

view this post on Zulip Maxime Dénès (Dec 13 2021 at 10:22):

Wondering why we mark Require in modules as non-export, and then we export on the side (so not storing the action in a libobject): https://github.com/coq/coq/blob/master/vernac/library.ml#L383

@Gaëtan Gilbert do you know?

view this post on Zulip Gaëtan Gilbert (Dec 13 2021 at 10:25):

because Require is Anticipate, so if you put the export in the object it will get reordered

Module M.
Definition x := 0.
Require Export X. (* shadows x *)
End M.
Import M.
(* x should be X.x *)

view this post on Zulip Maxime Dénès (Dec 13 2021 at 10:28):

So why don't we always split in two objects? (i.e. removing Export handling from inRequire)

view this post on Zulip Gaëtan Gilbert (Dec 13 2021 at 10:28):

not sure how it works with end_library though

view this post on Zulip Maxime Dénès (Dec 13 2021 at 10:28):

Would it be correct?

view this post on Zulip Gaëtan Gilbert (Dec 13 2021 at 10:28):

maybe

view this post on Zulip Maxime Dénès (Dec 13 2021 at 10:29):

Ok, thanks, I'll try. Because testing if we are in a module currently depends on the typing env...

view this post on Zulip Maxime Dénès (Dec 13 2021 at 10:29):

I can test it by other means of course, but if we can just remove the branching, it would make the code simpler.

view this post on Zulip Gaëtan Gilbert (Dec 13 2021 at 10:30):

sounds good

view this post on Zulip Maxime Dénès (Dec 13 2021 at 10:44):

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

view this post on Zulip Maxime Dénès (Dec 13 2021 at 10:54):

Btw I wonder how these Anticipate objects deal with commutations with commands changing the loadpath...

view this post on Zulip Gaëtan Gilbert (Dec 13 2021 at 11:06):

it's resolved before adding the object

view this post on Zulip Maxime Dénès (Dec 13 2021 at 11:45):

@Hugo Herbelin Small question about where notations: can they introduce parsing rules? I thought not, but they call syntax extensions: https://github.com/coq/coq/blob/master/vernac/metasyntax.ml#L1688

view this post on Zulip Maxime Dénès (Dec 13 2021 at 12:02):

Removing this line doesn't seem to make stdlib build nor test suite fail.

view this post on Zulip Gaëtan Gilbert (Dec 13 2021 at 12:13):

Maxime Dénès said:

I can test it by other means of course, but if we can just remove the branching, it would make the code simpler.

turns out to fix a bug too ;)

view this post on Zulip Hugo Herbelin (Dec 13 2021 at 13:00):

Maxime Dénès said:

Hugo Herbelin Small question about where notations: can they introduce parsing rules? I thought not, but they call syntax extensions: https://github.com/coq/coq/blob/master/vernac/metasyntax.ml#L1688

They don't introduce new parsing rules (the inSyntaxExtension registration is anyway done after parsing of the declaration and cancelled after interpretation of the declaration). Unfortunately, I don't remember why I added this registration. It seems to be a no-op. You may try to remove the line.

view this post on Zulip Maxime Dénès (Dec 14 2021 at 12:44):

Good news: I have a POC that is able to parse the standard library. In the coming days, I'll sketch a plan with an overview of the required patches.

view this post on Zulip Maxime Dénès (Dec 14 2021 at 12:57):

Pitty that we don't have a globalization phase that is independent from typing, though. It would have been nice for IDEs to be able to quickly know how to resolve references, without fully executing a document.

view this post on Zulip Emilio Jesús Gallego Arias (Dec 14 2021 at 13:19):

Looking forward to the update!

Maxime Dénès said:

Pitty that we don't have a globalization phase that is independent from typing, though. It would have been nice for IDEs to be able to quickly know how to resolve references, without fully executing a document.

Hugo and I were doing some work to that extent, for coq-layout-engine, so certainly we can make things a bit more usable.

view this post on Zulip Maxime Dénès (Dec 14 2021 at 13:42):

Oh! Can you say a bit more about what you were working on?

view this post on Zulip Enrico Tassi (Dec 14 2021 at 15:26):

Maxime Dénès said:

Pitty that we don't have a globalization phase that is independent from typing, though. It would have been nice for IDEs to be able to quickly know how to resolve references, without fully executing a document.

I know two offenders. Notation scopes attached to inferred types; the code for inductive types / records (which mixes both phases).

For the latter one I do have some code in Elpi with does just the globalization. We could see if this can be used to separate the phases (I don't cover all cases in my code, eg mutual inductive or records with notations)

About the scopes, I really don't know how much this is used in practice. IIRC scopes attached to types are not very reliable, since types are compared syntactically. I would not be too surprised if most of mathcomp would work fine without that feature.

view this post on Zulip Paolo Giarrusso (Dec 14 2021 at 16:06):

Re notation scopes for inferred types, that’s used as soon as you write Definition succN n : N := n + 1. … succN 0. In Iris canonical structures, that’s used quite a bit eg by Bind Scopes with bi_car. (where bi_car projects the carrier from a canonical structure) — tho that line is a recent addition.

view this post on Zulip Emilio Jesús Gallego Arias (Dec 14 2021 at 17:42):

Maxime Dénès said:

Oh! Can you say a bit more about what you were working on?

Some time ago I wrote a new printer prototype à la Isabelle [with semantic information] , still on early stages [I did a talk here couple of months ago] , but we have similar needs. Hope I can do a release soon, but workload not looking good

view this post on Zulip Maxime Dénès (Dec 14 2021 at 19:30):

Interesting. Did it not require executing the document?

view this post on Zulip Emilio Jesús Gallego Arias (Dec 14 2021 at 19:47):

Depends on the information, in some cases you can do with parsing, in some cases you need to run full pretyping, but usually you want only a partial run of the whole elaboration as you indicated

view this post on Zulip Enrico Tassi (Dec 14 2021 at 20:43):

How much of this separation did you work out in your project? Did you split elaboration up?

view this post on Zulip Hugo Herbelin (Dec 15 2021 at 12:54):

Enrico Tassi said:

IIRC scopes attached to types are not very reliable, since types are compared syntactically.

Types attached to scopes reuse the mechanism of "classes" used for coercions, and it is not strictly purely syntactic (which in turn means that it requires typing...). I don't know if this is what "not syntactic" would mean for you, but computation of arguments scopes could stepwise unfold head constants until finding a constant which is known, such as, for instance Definition f (a: id nat) := a. assigns nat_scope to a, rather than concluding that id is not bound to a scope and assigning no scope to a? In this case, we could make a PR to support this refinement.

view this post on Zulip Hugo Herbelin (Dec 15 2021 at 12:55):

Otherwise, am I right that to globalize through a notation whose interpretation is unknown (because typing dependent), knowing which ident subterms of the notations are bindings would be enough, or is it too naive? Conversely, what are the typical examples where the interpretation of a notation needs to be known to globalize references?

view this post on Zulip Enrico Tassi (Dec 15 2021 at 13:15):

Being smarter (eg unfold etc) would be possible but both expensive and would definitely make the phases we may want to separate more entangled. What I had in mind when I wrote "unreliable and syntactic" is that in the context of MC Definition f x := x + 1 may infer for x the type ZMod.sort int_ZmodType which is convertible to int but not syntactically equal hence I bet no scope is automatically attached to x. Imo this weakness is a good thing, since we have some hope that globalization and typing can be decoupled.

If we had to touch that code, I'd suggest to attach scopes to arguments only if the type is given by the user and stay purely syntactic (so that we can globalize without typing). So Definition (x : int) := x + 1 would get the scope, because globalization is enough to get your hands on int. Similarly Implicit Type x : int would be taken into account for that (without typing anything).

view this post on Zulip Hugo Herbelin (Dec 15 2021 at 13:37):

Before arbitrating being whether arguments scopes should be more or less syntactic, do you have an example where globalization of references breaks currently?

view this post on Zulip Enrico Tassi (Dec 15 2021 at 13:59):

I don't have a running example because we don't have a PR which tries to just parse and globalize a file, but the example of Jason seems to do it:

Definition f x := x + 0. (* x inferred to be of type nat, hence nat scope *)
Notation "'a" := foo : nat_scope.
Notation "'a" := bar : bool_scope.
Check f 'a. (* without typing `f` there is no scope attached to its argument *)

So, if you use just globalization to provide a user interface the "jump to definition" feature, when you click on 'a do you jump to foo or bar? If the scope was not depending on typing, eg given explicitly via Arguments, then globalization would be enough to pick the right notation interpretation (one would still need to execute some parts of the Arguments command).

view this post on Zulip Enrico Tassi (Dec 15 2021 at 14:03):

Overall the idea is to separate the processing of the document into phases of increasing complexity and cost. Parsing is the first one, and lets you already give useful feedback to the user. Globalization comes next and would give you nice stuff like jump to definition, or semantic syntax highlighting (bound variable x different from global constant x). All the rest (typing, tactic execution, ..) would give you everything, but it is much more expensive.

view this post on Zulip Hugo Herbelin (Dec 15 2021 at 14:35):

Enrico Tassi said:

Overall the idea is to separate the processing of the document into phases of increasing complexity and cost. Parsing is the first one, and lets you already give useful feedback to the user. Globalization comes next and would give you nice stuff like jump to definition, or semantic syntax highlighting (bound variable x different from global constant x). All the rest (typing, tactic execution, ..) would give you everything, but it is much more expensive.

So, in some sense, the example says that the globalization could itself be split into two phases. A phase for global references with relatively low complexity and cost, and a more expensive phase for disambiguation of notations. Am I right?


Last updated: Jun 08 2023 at 04:01 UTC