Jason Gross (Aug 09 2022 at 10:04): 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)
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.
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?
Gaëtan Gilbert (Aug 09 2022 at 10:58):there is no complete list, for it is extensible
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)?
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)
Pierre Roux (Aug 09 2022 at 11:53):Would that help? https://github.com/coq/coq/pull/11117#discussion_r347032445
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
Maybe the instructions on how to run the debugger could help?
Gaëtan Gilbert (Aug 09 2022 at 12:43):I never understood why we can't statically link that damn .so
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.
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
Gaëtan Gilbert (Aug 09 2022 at 13:55):what's the current status with dune? can dune do -custom?
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
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
Emilio Jesús Gallego Arias (Aug 09 2022 at 13:58):still pain
Last updated: Sep 15 2024 at 12:01 UTC