Maxime Dénès (Dec 08 2021 at 14:29): 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
Maxime Dénès (Dec 08 2021 at 14:29):@Pierre-Marie Pédrot do you know?
Pierre-Marie Pédrot (Dec 08 2021 at 14:32):Dunno. Do we rely on the name actually?
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.
Maxime Dénès (Dec 08 2021 at 14:38):Hence my question, because this usage seems strange.
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
Gaëtan Gilbert (Dec 08 2021 at 14:43):oh we already have add_anonymous_entry
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?)
Pierre-Marie Pédrot (Dec 08 2021 at 14:45):Ideally we should even enforce this by typing...
Maxime Dénès (Dec 08 2021 at 16:23):I guess there are two changes:
Include an anonymous objectI'll give the first a try, see if we can remove current_mod_id.
Maxime Dénès (Dec 08 2021 at 16:24):(for context, I'm working on the parsing/execution separation)
Maxime Dénès (Dec 08 2021 at 16:36):Ok, of course we do rely on the name for Include :)
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?
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)
Maxime Dénès (Dec 08 2021 at 16:37):But the general idea would be to expose two functions at the vernac level
Emilio Jesús Gallego Arias (Dec 08 2021 at 16:37):Thanks Max, actually I was wondering how far your wanted to go
Maxime Dénès (Dec 08 2021 at 16:37):One for parsing + syntax, the other for interpretation
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 :(
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
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
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
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 :) )
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.
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
Emilio Jesús Gallego Arias (Dec 08 2021 at 16:40):Parsing depends on the parsing state, which is updated by many commands
Emilio Jesús Gallego Arias (Dec 08 2021 at 16:41):Yes the interaction is complex
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.
Maxime Dénès (Dec 08 2021 at 16:42):Or to write a robust and efficient coqdoc, things like that.
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
Maxime Dénès (Dec 08 2021 at 16:42):Reasoning on known ASTs is nice :)
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.
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
Emilio Jesús Gallego Arias (Dec 08 2021 at 16:43):I can't draw a diagram now
Maxime Dénès (Dec 08 2021 at 16:43):There's explicit state passing and state separation.
Emilio Jesús Gallego Arias (Dec 08 2021 at 16:43):Yes, explicit state parsing is IMHO supergood
Maxime Dénès (Dec 08 2021 at 16:43):State separation is what I'd like to make explicit.
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
Emilio Jesús Gallego Arias (Dec 08 2021 at 16:44):yes that'd be great
Maxime Dénès (Dec 08 2021 at 16:44):It is a bit orthogonal to state passing.
Maxime Dénès (Dec 08 2021 at 16:44):But certainly compatible!
Emilio Jesús Gallego Arias (Dec 08 2021 at 16:44):Yes
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
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.
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
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
Maxime Dénès (Dec 08 2021 at 16:46):In short, state and phase separation enables some optimizations (reparsing without reexecuting)
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
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
Emilio Jesús Gallego Arias (Dec 08 2021 at 16:46):you just build the right DAG reflecting the type
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
Emilio Jesús Gallego Arias (Dec 08 2021 at 16:47):IIUC
Emilio Jesús Gallego Arias (Dec 08 2021 at 16:47):by people doing math
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
Emilio Jesús Gallego Arias (Dec 08 2021 at 16:48):I wish I could draw a diagram but I can't right now
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?
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
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
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?
Gaëtan Gilbert (Dec 08 2021 at 18:27):y
Maxime Dénès (Dec 08 2021 at 18:28):Interesting piece of code.
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)
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
Gaëtan Gilbert (Dec 09 2021 at 09:59):result: I can
Maxime Dénès (Dec 09 2021 at 13:16):Did you push a branch?
Gaëtan Gilbert (Dec 09 2021 at 13:37):https://github.com/coq/coq/pull/15317
Last updated: Oct 12 2024 at 12:01 UTC