Stream: Coq devs & plugin devs

Topic: Printing keywords


view this post on Zulip Jason Gross (Aug 09 2022 at 10:04):

Is there a way to print out all reserved keywords? (In particular, I'm looking to get the list of strings which are nominally identifiers but that cannot be used after Module)

view this post on Zulip Jason Gross (Aug 09 2022 at 10:33):

I can find most of them in Print Grammar constr. Print Grammar tactic. Print Grammar vernac., but Prop and SProp don't occur there, for example.

view this post on Zulip Jason Gross (Aug 09 2022 at 10:56):

By looking at a combination of those grammars and cat coq/doc/tools/docgram/fullGrammar, I found the list ('Axiom', 'CoFixpoint', 'Definition', 'Export', 'Fixpoint', 'Hypothesis', 'Import', 'Parameter', 'Prop', 'SProp', 'Set', 'Theorem', 'Type', 'Variable', '_', 'as', 'at', 'by', 'cofix', 'else', 'end', 'exists', 'exists2', 'fix', 'for', 'forall', 'fun', 'if', 'in', 'let', 'match', 'return', 'then', 'using', 'where', 'with') Is this missing any tokens that cannot be module names?

view this post on Zulip Gaëtan Gilbert (Aug 09 2022 at 10:58):

there is no complete list, for it is extensible

view this post on Zulip Jason Gross (Aug 09 2022 at 11:19):

Is there a way to get Coq to print a complete list (something like Print Grammar constr but it should include keywords like Type and Prop)?

view this post on Zulip Jason Gross (Aug 09 2022 at 11:51):

(I want this for the bug minimizer, to know which intermediate directory names I have to escape when inlining files like Equations.Prop.Equations)

view this post on Zulip Pierre Roux (Aug 09 2022 at 11:53):

Would that help? https://github.com/coq/coq/pull/11117#discussion_r347032445

view this post on Zulip Jason Gross (Aug 09 2022 at 12:04):

It would, except that I cannot run coqtop.byte because I get

Fatal error: cannot load shared library dllcoqrun_stubs
Reason: dllcoqrun_stubs.so: cannot open shared object file: No such file or directory
Aborted

view this post on Zulip Pierre Roux (Aug 09 2022 at 12:12):

Maybe the instructions on how to run the debugger could help?

view this post on Zulip Gaëtan Gilbert (Aug 09 2022 at 12:43):

I never understood why we can't statically link that damn .so

view this post on Zulip Jason Gross (Aug 09 2022 at 13:24):

dev/doc/debugging.md just says "Launch bytecode version of Coq (coqtop.byte)" and does not include any instructions about what to do if this fails.

view this post on Zulip Emilio Jesús Gallego Arias (Aug 09 2022 at 13:40):

Gaëtan Gilbert said:

I never understood why we can't statically link that damn .so

@Gaëtan Gilbert see https://github.com/coq/coq/issues/6475

view this post on Zulip Gaëtan Gilbert (Aug 09 2022 at 13:55):

what's the current status with dune? can dune do -custom?

view this post on Zulip Emilio Jesús Gallego Arias (Aug 09 2022 at 13:57):

I think so, I didn't think of that as Xavier told me (in person) that we must not use it, and anyways we gotta dynlink due to the plugins

view this post on Zulip Emilio Jesús Gallego Arias (Aug 09 2022 at 13:58):

actually dune exec -- will set the right LD_LIBRARY_PATH so pain is a bit lower

view this post on Zulip Emilio Jesús Gallego Arias (Aug 09 2022 at 13:58):

still pain


Last updated: Feb 01 2023 at 15:04 UTC