Stream: Coq devs & plugin devs

Topic: Names used in extraction plugins


view this post on Zulip Julin Shaji (Jan 10 2024 at 05:01):

I was looking at the grammar files of the extraction plugins in the coq repo.
https://github.com/coq/coq/blob/master/plugins/extraction/g_extraction.mlg

There are names like: ne_global_list, preident, identref, etc.

I was wondering what those names signify and where they come from.
Does anyone know?

From the context, one can guess the intention sometimes but not sure how accurate such guesses would be.

view this post on Zulip Julin Shaji (Jan 10 2024 at 05:02):

Tried grep-ing the coq repo for ne_global_list, but could spot only usages, not definition.

view this post on Zulip Julin Shaji (Jan 10 2024 at 05:05):

Does this have something to do with camlp5?

view this post on Zulip Julin Shaji (Jan 10 2024 at 05:10):

Found an identref in pcoq.ml:
https://github.com/coq/coq/blob/master/parsing/pcoq.ml#L315

view this post on Zulip Julin Shaji (Jan 10 2024 at 05:10):

What could ne_ stand for in ne_global_list?

view this post on Zulip Julin Shaji (Jan 10 2024 at 06:45):

Could this be related?
https://coq.inria.fr/doc/v8.10/api/coq/Stdarg/index.html

view this post on Zulip Gaëtan Gilbert (Jan 10 2024 at 07:10):

ne_ and _list are magic modifiers, it means nonempty list of (whatever's in the middle in this case global)
after removing the modifiers the names are regular ocaml names like https://github.com/coq/coq/blob/50ca6d51cffb28e23a4890d7cb3b254677866f3f/parsing/pcoq.mli#L152 (but I think they have to be from open modules, you can't qualify them)

view this post on Zulip Julin Shaji (Jan 11 2024 at 17:03):

And what does the wit_ prefix in the variable names of stdarg.ml stand for?

view this post on Zulip Gaëtan Gilbert (Jan 11 2024 at 17:05):

argument extend uses genarg instead of entry, so when you write identrefit looks up wit_identref

view this post on Zulip Julin Shaji (Jan 12 2024 at 06:24):

What does entry mean in coq?

Have heard of custom entries in notations, but never really knew what the name 'entry' meant there.

view this post on Zulip Gaëtan Gilbert (Jan 12 2024 at 08:46):

kernel entry is unrelated to grammar entry

kernel entry is the input type of the kernel, functions to have the kernel check and add a definition / inductive / etc to the environment look like entry -> safe_env -> safe_env (in safe_typing.mli)

view this post on Zulip Paolo Giarrusso (Jan 12 2024 at 12:49):

and AFAICT, a "grammar entry" is what everybody else calls nonterminal; Coq's grammar has entries/nonterminals like constr for terms, but custom entries let you add _new_ nonterminals, while other term notations only add rules to constr.


Last updated: Oct 13 2024 at 01:02 UTC