Coq项目中`rocq dep`命令处理空字符串属性时出现异常

在Coq项目的最新版本(9.0及master分支)中，当使用rocq dep命令处理包含空字符串值的属性时，会出现一个异常错误。这个问题在8.20版本中并不存在，属于新引入的回归问题。

问题现象

当Coq文件中出现如下形式的代码时：

#[x=""] Redirect "log" Require Import Init.

执行rocq dep命令会报错：

*** Error: Anomaly "Uncaught exception Failure("lexing: empty token")."

技术分析

这个问题源于Coq依赖分析工具(coqdep)中的词法分析器(lexer)实现。具体来说，在处理属性(attribute)时，词法分析器无法正确处理空字符串值的情况。

在tools/coqdep/lib/lexer.mll文件中，原始的正则表达式模式'"' [^ '"']+ '"'要求字符串内容必须至少包含一个非引号字符。这意味着空字符串""无法被正确匹配，从而导致词法分析失败。

解决方案

修复方法相对简单，只需将正则表达式中的+量词(表示"一个或多个")改为*量词(表示"零个或多个")：

-  | '"' [^ '"']+ '"'
+  | '"' [^ '"']* '"'

这样修改后，词法分析器就能正确处理空字符串作为属性值的情况。这个修改在技术上被认为是正确的，因为它更准确地反映了字符串属性值的可能情况——既可以是包含内容的字符串，也可以是空字符串。

影响范围

这个问题影响：

• Coq 9.0版本
• master分支
• 使用rocq dep命令的场景
• 包含空字符串属性值的Coq文件

在Coq 8.20及更早版本中不存在此问题。

总结

这个bug展示了在词法分析器设计中考虑边界情况的重要性。即使是看似简单的字符串匹配规则，也需要考虑所有可能的输入情况，包括空字符串这种特殊情况。对于开发类似工具的程序员来说，这是一个很好的教训：在设计模式匹配规则时，应该仔细考虑所有可能的输入边界条件。