Motivations for extensible parsing · Coq devs & plugin devs

The discussion in https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs-.26-plugin-devs/topic/Github.20code.20scanning made me realize I don't exactly know why we need to extend the parser in the middle of building a project in Coq. Sure, we want user-defined notations, and plugins being able to introduce grammar rules. But we could imagine that the grammar extensions and plugin dependencies for a given project are defined in a kind of preamble (a bit like Reserved Notations) used by the build system to initialize the grammar which would then be static.

I imagine this could simplify a lot the handling we have today of plugin loading, syntax extensions, and their undoing. And better reflect the non-modular nature of these. Not to mention that the parsing / execution separation would come for free. I guess this would not be flexible enough for some use cases?

Gaëtan Gilbert (Jan 10 2023 at 09:28):

we can have some notation syntax only active while some module is imported and which needs to be backtracked when the current module/section is closed
ie

Module N. Notation ... End N.
Section UseN.
Import N.
...
End UseN.
(* notation not active here, we can use a notation that would conflict if we want *)

Gaëtan Gilbert (Jan 10 2023 at 09:29):

backtracking plugins I think doesn't happen in coqc but interactive use is a different question

Maxime Dénès (Jan 10 2023 at 09:29):

Sure. My question was whether this is actually used (note that the conflicting notations should have conflicting rules, not just varying interpretation).

Gaëtan Gilbert (Jan 10 2023 at 09:30):

also interactively there is no way we want to have to restart coq to define a new notation

Maxime Dénès (Jan 10 2023 at 09:31):

Well, if the interactive system is smart enough, you add a notation to the preamble, it reparses and if nothing changes, that's it.

Maxime Dénès (Jan 10 2023 at 09:34):

Actually, you may be hinting at why we have all this complexity today. Having a naive user interaction model has shifted a lot of the complexity in vernac.

Matthieu Sozeau (Jan 10 2023 at 10:32):

Plugins could dynamically generate notations too. Doesn't coq-elpi allow this already?

Maxime Dénès (Jan 10 2023 at 10:40):

Emilio Jesús Gallego Arias (Jan 10 2023 at 12:18):

I guess that if we want Coq documents to get close to what a mathematical document is, having a static parser is too restrictive.

The problems with handling of grammar extensions have IMHO little to do with parsing being extensible, but with our parsing engine and its implementation; having the state of the parsing be truly functional would solve most of these problems.

Forbbiding parsing extension would actually not solve the current bugs, as still you would have the current problems when a user updates the preamble.

Gaëtan Gilbert (Jan 10 2023 at 12:22):

I agree. The problem is not quite about extension and is more about our implementation of backtracking across an extension

Maxime Dénès (Jan 10 2023 at 12:49):

Yes, sorry I wasn't clear: I'm not suggesting we can avoid fixing the current bugs. In fact, that's why we discussed with @Gaëtan Gilbert it would be nice to fix https://github.com/coq/coq/issues/12575: all UI-related work is going to need correct behavior there, at some point or another.

Maxime Dénès (Jan 10 2023 at 12:52):

My question was more of a curiosity, trying to see if our technology is more general than what mathematical practice really requires. It seems clear that mathematical documents do introduce specific notations. What is less clear to me is whether they sometimes introduce conflicting notations (in terms of grammar rules) in different parts.

Pierre-Marie Pédrot (Jan 10 2023 at 13:00):

By the mere definition of independent compilation I don't see how it could be any different.

Emilio Jesús Gallego Arias (Jan 10 2023 at 19:19):

@Maxime Dénès I think indeed that different parsing tech is something that is worth exploring yes, there are indeed ways to have something like current Coq tech with a fixed parsing grammar + a macro system for example.

Indeed a good start would try to see if Entry.of_parser could be removed, then you could have a look at what grammars are active; but for example tree-sitter is going to require an automated conversion to GLR as Guillaume mentioned, which not sure it would be possible.

Enrico Tassi (Jan 10 2023 at 21:22):

Maxime Dénès (Jan 10 2023 at 21:59):

@Emilio Jesús Gallego Arias Yes, something like a macro system was what I was wondering about. Of course it would have to be powerful enough to cover the typical use cases in mathematics and computer science. But whether these use cases require something as general as arbitrary extensions of grammar rules in arbitrary places, I don't know. Maybe something a bit more structured would be possible.

Maxime Dénès (Jan 10 2023 at 22:01):

Paolo Giarrusso (Jan 10 2023 at 22:20):

You'd really want scannerless GLR, not just GLR: a modular parser doesn't help if your lexer isn't modular (aka, it exists). As i mentioned in the past, the late Eelco Visser (of Stratego fame) spent quite some effort into scannerless GLR.

Stream: Coq devs & plugin devs

Topic: Motivations for extensible parsing

Maxime Dénès (Jan 10 2023 at 09:24):