Compile before require does not ignore comments

[vbgl]

When there are comments in a Require or Require Import sentence, and when “Compile Before Require” is enabled, Proof-General tries to compile the modules whose names are in comment. This behavior is unexpected and may fail (maybe because the comment is an actual comment, not a list of module names).

Test case:

Require Import (* Hello World *) Logic.

Surprisingly, things work as expected when comments are in Japanese; e.g., the following does not fail.

Require Import (* おはよう、世界！*) Logic.

Tested with current master (a789470) and Coq 8.7.2.

[Matafou]

Thanks for reporting.
@hendriktews can you have a look at it pls?

[hendriktews]

@hendriktews can you have a look at it pls?

Yes, I try. H.

[hendriktews]

Vincent, thanks for reporting and recording this. The problem is that I extract the module names with a simple regular expression from the command string. I just wonder if we could run coqdep on the original require command string and let coqdep struggle with nested comments and strings inside them (instead of correctly parsing them in elisp). I need some more time to think about this.

Surprisingly, things work as expected when comments are in Japanese;

This is because the default regular expression for module names does not match Japanese characters. Hendrik

[RalfJung]

I just ran into this as well -- it took me some time to realize why PG is failing on this line:

From reloc Require Export reloc lib.Y (* for bot *).