Stream: Coq devs & plugin devs

Topic: Include libobject


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

I'm probably misinterpreting the code, but why do we put the current module id as the name for Include libobjects? https://github.com/coq/coq/blob/23025455e291654e83d6bf6a892059d17619d871/vernac/declaremods.ml#L953

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

@Pierre-Marie Pédrot do you know?

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

Dunno. Do we rely on the name actually?

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

No idea, but this code is the only client of Lib.current_mod_id, it seems.

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

Hence my question, because this usage seems strange.

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

yeah this should be add_anonymous_leaf, except Lib.add_anonymous_leaf is specialized for AtomicObject
I guess we need to expose a _gen version or some such thing

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

oh we already have add_anonymous_entry

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

(As advocated by @Emilio Jesús Gallego Arias we should simply remove this anonymous name stuff. What's the point of generating crappy useless gensyms?)

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

Ideally we should even enforce this by typing...

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

I guess there are two changes:

  1. Make Include an anonymous object
  2. Make anonymous objects not generate fake names

I'll give the first a try, see if we can remove current_mod_id.

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

(for context, I'm working on the parsing/execution separation)

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

Ok, of course we do rely on the name for Include :)

view this post on Zulip Emilio Jesús Gallego Arias (Dec 08 2021 at 16:36):

Maxime Dénès said:

(for context, I'm working on the parsing/execution separation)

You have some outline on what the plan there is?

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

I don't, because I'm still at the technical exploration phase (i.e. trying to understand if it is feasible or not)

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

But the general idea would be to expose two functions at the vernac level

view this post on Zulip Emilio Jesús Gallego Arias (Dec 08 2021 at 16:37):

Thanks Max, actually I was wondering how far your wanted to go

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

One for parsing + syntax, the other for interpretation

view this post on Zulip Emilio Jesús Gallego Arias (Dec 08 2021 at 16:38):

As discussed some time ago, I think a big help would be to make the parsing state more functional, but that's a lot of hard work it seems to me :(

view this post on Zulip Emilio Jesús Gallego Arias (Dec 08 2021 at 16:38):

Even if parsing needs to do a callback to intepretation doesn't bother me at lot, as long as it is reflected on the types

view this post on Zulip Emilio Jesús Gallego Arias (Dec 08 2021 at 16:38):

so the DAG of the document in terms of dependencies doesn't have "hidden" nodes

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

Well, I think for tooling it would be nice two reflect the stratification in the API

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

I don't think parsing really depends on interpretation today, but not 100% sure (hence the exploration :) )

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

Functional parsing state would be nice, but in fact, this state handling is not the most difficult part. At least to me, most difficult is to understand the interaction between parsing and the module system.

view this post on Zulip Emilio Jesús Gallego Arias (Dec 08 2021 at 16:40):

That's a bit nicer but IMO the advantage is not so large, once you have a DAG you can reflect the computations as edges, you don't care so much IMHO what the actual computations are; it is IMHO a way more pressing issue that we have the hidden state; so you need to add special cases to your engine

view this post on Zulip Emilio Jesús Gallego Arias (Dec 08 2021 at 16:40):

Parsing depends on the parsing state, which is updated by many commands

view this post on Zulip Emilio Jesús Gallego Arias (Dec 08 2021 at 16:41):

Yes the interaction is complex

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

Not having a parsing / interpretation separation is anoying if you want to interpret text edits for example.

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

Or to write a robust and efficient coqdoc, things like that.

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

I'm pretty biased here as when I try to understand this stuff, what I do is remove the parsing global state, so now every place that needs or update the parsing state is explicit about it, but given how the modules are you are in a mess indeed

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

Reasoning on known ASTs is nice :)

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

In fact, it is a bit like what you did on the parser vs vernac state.

view this post on Zulip Emilio Jesús Gallego Arias (Dec 08 2021 at 16:43):

Maxime Dénès said:

Not having a parsing / interpretation separation is anoying if you want to interpret text edits for example.

Why is that a problem? You just have a different DAG, but people do that routinely, for example in NLP

view this post on Zulip Emilio Jesús Gallego Arias (Dec 08 2021 at 16:43):

I can't draw a diagram now

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

There's explicit state passing and state separation.

view this post on Zulip Emilio Jesús Gallego Arias (Dec 08 2021 at 16:43):

Yes, explicit state parsing is IMHO supergood

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

State separation is what I'd like to make explicit.

view this post on Zulip Emilio Jesús Gallego Arias (Dec 08 2021 at 16:44):

because then you can map functions to a DAG, and have an engine that observes nodes of the DAG

view this post on Zulip Emilio Jesús Gallego Arias (Dec 08 2021 at 16:44):

yes that'd be great

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

It is a bit orthogonal to state passing.

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

But certainly compatible!

view this post on Zulip Emilio Jesús Gallego Arias (Dec 08 2021 at 16:44):

Yes

view this post on Zulip Emilio Jesús Gallego Arias (Dec 08 2021 at 16:45):

But you are right we have stuff like Declaremods which is hell for document managers IMHO

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

Emilio Jesús Gallego Arias said:

Maxime Dénès said:

Not having a parsing / interpretation separation is anoying if you want to interpret text edits for example.

Why is that a problem? You just have a different DAG, but people do that routinely, for example in NLP

Well, in theory there's no problem. The real problem is practical: in an environment like Coq where interpretation of commands often takes a long time, you typically want to be able to revalidate the AST quickly.

view this post on Zulip Emilio Jesús Gallego Arias (Dec 08 2021 at 16:45):

But what I mean here is that of course, the more we have interpretation and parsing separte, the better

view this post on Zulip Gaëtan Gilbert (Dec 08 2021 at 16:46):

Maxime Dénès said:

Ok, of course we do rely on the name for Include :)

please explain more

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

In short, state and phase separation enables some optimizations (reparsing without reexecuting)

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

Gaëtan Gilbert said:

Maxime Dénès said:

Ok, of course we do rely on the name for Include :)

please explain more

We pass it to cache_include

view this post on Zulip Emilio Jesús Gallego Arias (Dec 08 2021 at 16:46):

yes, but my point is that you can get this benefit, while still allowing a command to be a barrier for parsing

view this post on Zulip Emilio Jesús Gallego Arias (Dec 08 2021 at 16:46):

you just build the right DAG reflecting the type

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

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

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

IIUC

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

by people doing math

view this post on Zulip Emilio Jesús Gallego Arias (Dec 08 2021 at 16:48):

so what I mean is: for most cases, parsing and interpretation should be separate, but there is not a problem if a dependency on the DAG to a notation state is injected

view this post on Zulip Emilio Jesús Gallego Arias (Dec 08 2021 at 16:48):

I wish I could draw a diagram but I can't right now

view this post on Zulip Gaëtan Gilbert (Dec 08 2021 at 16:48):

We pass it to cache_include

but we don't care about the id part right?

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

Are you sure? Reading the code, I thought the id was the one of the enclosing module, and we did get it back in the result of make_foname

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

but cache_include only uses the oname through

  let obj_dir = Libnames.dirpath sp in
  let obj_mp = KerName.modpath kn in

which discards the id

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

So, in :

Module A.
Include B.

the id for the Include libobject would be A, which would give the non-sensical oname A.A, where the id is then ignored to get back to the A modpath and dirpath?

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

y

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

Interesting piece of code.

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

However as I just found out in

Include X.

(ie directly at toplevel, no surrounding module other than the file)
it gets the id _1
and the oname for CompilingLibrary is (If you see this, it's a bug._1, If you see this, it's a bug._1)

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

I'm making a bit libobject/lib refactor so let's see if I can get rid of the IncludeObject id

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

result: I can

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

Did you push a branch?

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

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


Last updated: Feb 06 2023 at 19:03 UTC