形式化验证编程语言【免费下载链接】coqThe Rocq Prover is an interactive theorem prover, or proof assistant. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.项目地址https://gitcode.com/gh_mirrors/co/coq点击查看免费下载本篇指南解析 Rocq ProverCoq 的继任者开发主线中的一项行为变更About命令查询Abbreviation缩写时输出将新增一行Arguments are in scopes展示缩写每个参数的符号作用域notation scope信息。文章以 changelog 条目 为核心骨架结合 输出测试套件 与 打印实现帮助读者理解变更动机、新输出格式、边界行为以及底层数据流并掌握在交互式顶层中验证该行为的方法。1. 变更速览一条 Changed 类 changelog该变更记录在仓库的 doc/changelog/08-vernac-commands-and-options/22336-abbreviation-argument-scopes-Changed.rst 中原文如下Changed:output ofAbouton anAbbreviationnow display notation scope information of its arguments #22336by Aleksei Rybnikov要点归纳变更类型Changed行为变更而非新增命令或修复缺陷类别目录08-vernac-commands-and-options即影响面限定在vernac 命令与选项层面受影响命令About查询全局引用信息的命令受影响对象Abbreviation语法缩写变更内容输出新增参数argument的 notation scope符号作用域信息来源上游 pull request #22336作者 Aleksei Rybnikov。该条目位于doc/changelog/未发布目录下属于当前开发主线Rocq 后续正式版本的行为变更发布时将由仓库的变更日志流程合入正式的 doc/sphinx/changes.rst。2. 前置知识Abbreviation 与符号作用域2.1 什么是 AbbreviationRocq 中的缩写由Abbreviation命令定义语法为见 doc/sphinx/user-extensions/syntax-extensions.rstAbbreviation ident {* ident__parm } : one_term {? ( {, syntax_modifier } ) }例如Abbreviation Nlist : (list nat). Abbreviation reflexive R : (forall x, R x x). Abbreviation Plus1 B : (Nat.add B 1).缩写具有以下关键语义纯语法展开缩写绑定到一个通常更复杂的表达式是语法层面的syntactic等价于用名字代指一段 term惰性类型检查定义时不检查所代指表达式的类型只有在使用时才做类型检查因此可以绑定含有洞_的表达式绑定绝对名缩写像普通定义一样绑定绝对名可通过限定名qualified name引用无优先级/结合性缩写按普通应用application解析因此不需要指定优先级作用域与隐式参数继承与记号Notation类似若右侧是部分应用的常量缩写会继承该常量的隐式参数与符号作用域打印倾向除非给出(only parsing)修饰符Rocq 打印器会尽可能使用缩写来输出局部性locality支持local、export、global属性区段外默认为export区段内仅支持local。从 interp/abbreviation.ml 的源码结构看每个缩写内部记录为一条包含 locality、模式interpretation、only-parsing 标志、激活状态等字段的数据全局维护在一张以KerName为键的映射表中Summary.ref保证其可随状态存档/回滚。2.2 什么是符号作用域notation scope符号作用域是 Rocq 记法系统中按上下文解释符号的机制同一个记号在不同作用域下可以有不同的含义例如在nat_scope中表示自然数加法在Z_scope中表示整数加法。术语term中通过显式分隔符把子项放入某个作用域深度作用域x%nat%分隔符影响整个子项及其子项的解释浅层临时作用域x%_nat%_分隔符只影响紧随其后的一个子项属于临时性作用域。在实现层面这两个层次分别对应 interp/notation_term.mli 中的类型定义type scope_name string type tmp_scope_name scope_name type subscopes tmp_scope_name list * scope_name list type extended_subscopes Constrexpr.notation_entry_relative_level * subscopessubscopes是一对列表左侧是临时浅层%_作用域右侧是常规深层%作用域。一个记法/缩写的每个参数都可以携带这样一组作用域说明。3. 变更内容About 输出新增Arguments are in scopes行在本次变更之前About查询一个Abbreviation时输出只包含缩写签名Abbreviation ... : ...与展开目标Expands to: ...不会提及每个参数在哪个符号作用域中解释——而这一点对使用者很重要同一个标识符在不同作用域下的含义可能不同。变更后About在缩写签名之后新增一行作用域摘要。以测试套件 test-suite/output/abbreviation_scopes.out 中的期望输出为例Abbreviation double x : (x x) Arguments are in scopes: x%_nat_scope Expands to: Abbreviation abbreviation_scopes.double Declared in library abbreviation_scopes, line 3, characters 0-33新行的格式为Arguments are in scopes: arg1%scope1, arg2%scope2, ...其中每个参数以参数名 作用域标记的形式列出多个参数之间用逗号分隔作用域标记完全镜像 term 语法——浅层临时作用域显示为%_scope常规深层作用域显示为%scope。若某个参数同时带有多种作用域则按顺序拼接列出。4. 官方测试套件实测五类场景全覆盖仓库为本次变更提供了专门的输出对比测试源文件 test-suite/output/abbreviation_scopes.v 与期望输出 test-suite/output/abbreviation_scopes.out 一一对应覆盖了全部关键场景。场景一参数出现在带作用域的算子中Abbreviation double x : (x x). About double.x x中的默认落在nat_scope因此输出Abbreviation double x : (x x) Arguments are in scopes: x%_nat_scope Expands to: Abbreviation abbreviation_scopes.double注意这里显示的是x%_nat_scope浅层%_形式——作用域信息来自参数被解释时的子项位置输出时保留了浅层/深层的区分。场景二多参数各自的作用域Abbreviation add3 x y z : (x y z). About add3.Arguments are in scopes: x%_nat_scope, y%_nat_scope, z%_nat_scope每个参数独立列出自己的作用域逗号分隔。场景三类型参数的作用域同样被识别Abbreviation idp A : (fun a : A a). About idp.Arguments are in scopes: A%_type_scope注释明确指出A scope is also known for a type argument——作用域检测不只针对值参数出现在类型位置的参数此处A落在type_scope同样会显示。场景四无作用域时不输出该行Abbreviation id_unit x : match x with tt tt end. About id_unit.输出中没有Arguments are in scopes行说明没有任何参数处于带作用域的解释之下时整行会被省略保持输出整洁。场景五无参数时不输出该行Abbreviation zero : 0. About zero.输出同样没有作用域行Nothing is printed when there is no argument。0自身的字面量解释虽然涉及作用域解析但该信息属于缩写体内部而非参数因此不属于本行的范畴。5. 源码实现剖析从 interpretation 到输出5.1 核心函数 print_abbreviation_argument_scopes新增输出由 vernac/prettyp.ml 中的print_abbreviation_argument_scopes实现let print_abbreviation_argument_scopes kn let (vars,_) Abbreviation.find_interp kn in (* Print every scope of each argument, not just the first: temporary scopes with the shallow [%_] delimiter and regular scopes with the deep [%] one, mirroring the term syntax (per proux01s review of #22336). *) let scopes_of (_entry,(tmp_scopes,scopes)) List.map (fun sc - %_ ^ sc) tmp_scopes List.map (fun sc - % ^ sc) scopes in let scoped List.filter_map (fun (id,(subscopes,_,_)) - match scopes_of subscopes with | [] - None | l - Some (id, l)) vars in if List.is_empty scoped then mt () else fnl () hov 0 (str Arguments are in scopes: spc () prlist_with_sep pr_comma (fun (id,scs) - Id.print id str (String.concat scs)) scoped)逐段解读取数据Abbreviation.find_interp kninterp/abbreviation.ml从缩写表中取出该缩写的interpretation其首分量vars正是(参数名, 参数属性) list映射标记scopes_of把每个参数属性中的(tmp_scopes, scopes)两列作用域分别映射为%_scope与%scope文本并保持顺序拼接——这正是输出与 term 语法逐字对应的原因源码注释还记录了设计取舍打印每一个作用域而不是只打印第一个源自 #22336 评审意见过滤filter_map只保留至少带一个作用域的参数无作用域参数被丢弃空则省略若所有参数都没有作用域scoped为空列表函数返回空输出mt ()——对应第 4 节的场景四、五组装否则另起一行fnl ()输出Arguments are in scopes:后接逗号分隔的参数名作用域标记列表。5.2 数据流参数属性从哪里来find_interp返回的interpretation类型定义在 interp/notation_term.mlitype a interpretation_gen (Id.t * a) list * notation_constr type interpretation (extended_subscopes * notation_var_binders * notation_var_instance_type) interpretation_gen即每个参数Id.t关联三元组extended_subscopes包含 entry 级别与subscopes、绑定上下文notation_var_binders与实例类型notation_var_instance_type。print_abbreviation_argument_scopes解构的(subscopes,_,_)正是其中的extended_subscopes展开——这些信息在缩写被声明Abbreviation命令或由记号内部化时就已经附着在参数上了。5.3 输出组装顺序About对缩写的完整输出由 vernac/prettyp.ml 的print_about_abbreviation组装顺序为print_abbreviation_body打印Abbreviation ident args : body该函数会临时关闭缩写的打印展开以免缩写体被自身递归打印见 vernac/prettyp.mlprint_abbreviation_argument_scopes新增的作用域行Expands to: ...展开到的限定名Abbreviation knloc_info (Abbrev kn)声明位置信息Declared in library ..., line ...。这一顺序与测试期望输出完全吻合。6. 如何复现与验证在本地验证该行为非常简单——在 Rocq 的交互式顶层rocqtop/coqtop或 RocqIDE中执行Abbreviation double x : (x x). About double.即可看到新增的Arguments are in scopes: x%_nat_scope行。也可以直接运行仓库测试套件中的输出对比测试将 test-suite/output/abbreviation_scopes.v 作为输入其标准输出应与 test-suite/output/abbreviation_scopes.out 逐字一致。需要说明的是该行为属于当前开发主线的变更需使用包含 #22336 的构建版本才能观察到。7. 影响与使用建议对人工查询About现在提供了更完整的信息帮助用户确认缩写参数的解释上下文尤其适合调试为什么在这里不是自然数加法这类作用域歧义问题对脚本与工具任何以文本方式解析About输出的脚本/插件需要注意对Abbreviation的输出可能新增一行Arguments are in scopes: ...建议按该行可能缺失无作用域参数时省略的方式做兼容处理对文档与打印作用域标记%_/%与 term 语法一致可以直接从输出中复制到自己的代码里无学习成本对测试仓库以output型测试.v .out 配对锁定该行为后续若调整输出格式需同步更新 abbreviation_scopes.out这为格式的稳定性提供了保障。总而言之#22336 让About对Abbreviation的查询输出补全了最后一个信息缺口不仅告诉你缩写展开成什么还告诉你每个参数在什么作用域里解释并且通过%_/%的区分忠实保留了浅层与深层作用域的语义使得输出可以直接反哺到实际代码中。赞分享形式化验证编程语言【免费下载链接】coqThe Rocq Prover is an interactive theorem prover, or proof assistant. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.项目地址https://gitcode.com/gh_mirrors/co/coq点击查看免费下载相关推荐CMake function() 命令完全指南作用域、参数变量与宏的差异详解CMake function 命令完全指南作用域、参数变量与宏的差异详解 本篇技术指南围绕 CMake 官方文档 Help/command/function.构建工具开发工具CLImitmproxy2swagger命令行参数详解提升工作效率的10个实用参数mitmproxy2swagger命令行参数详解提升工作效率的10个实用参数 你是否还在为手动编写API文档而烦恼mitmproxy2swagger作为一款开发工具API设计FreeToken ft命令完全参考6大子命令与全部参数详解附实用示例FreeToken ft命令完全参考6大子命令与全部参数详解附实用示例 FreeToken 是一个开源的本地大模型推理服务框架能把数据中心级的模型服务搬人工智能大模型模型推理服务本地部署推理引擎上一篇NocoBase 数据加载方式配置指南自动加载与手动加载auto/manual的原理与实战下一篇3分钟揭秘如何让B站缓存视频重获新生m4s-converter的神奇魔法创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考