形式化验证编程语言【免费下载链接】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 证明助手中change及一批“转换类conversion策略”的一次错误信息改进展开过去这些策略失败时只会给出光秃秃的Not convertible不可转换现在则会明确指出到底是哪两个项不满足转换关系。本文将以 变更记录原文 为骨架结合tactics/、pretyping/等目录下的真实源码与test-suite/中的回归测试讲清楚这一行为的来龙去脉、底层实现机制以及它对日常证明脚本、Ltac 自动化与插件开发者各自的影响。读完本文你将能看懂转换失败错误信息的含义、定位其背后的调用链并学会用测试用例验证该行为。一、变更概要从一句空话到两个具体项1.1 变更记录原文仓库 doc/changelog/04-tactics/22335-not-convertible-terms-Changed.rst 收录了本次变更类别为Changed即行为改变而非新增功能Changed:change策略以及其他转换conversion策略现在会报告到底是哪些项不可转换而不再只是给出一个光秃秃的Not convertible消息。对应 PR 为#22335修复了#20944问题作者为 Aleksei Rybnikov。这段记录虽短却代表了一次用户可感知的错误诊断能力提升错误信息从“状态码”变成了“诊断报告”。1.2 为什么值得关注在交互式定理证明中change是使用频率极高的“按定义等价改写”策略。当它失败时旧版只输出Not convertible用户往往要自己猜测是目标类型不匹配、某个假设类型写错还是定义展开后存在细微差异。改进后系统直接把发生冲突的两个项打印出来定位问题的成本大幅下降也方便在.v脚本与 CI 输出中直接比对。二、背景什么是“可转换”convertible与change策略2.1 转换关系的含义Rocq 的每一项判断都建立在定义相等definitional equality之上两个项只要经过归约reduction后变得一致就称它们可转换convertible。与之相关还有一个更弱的累积关系cumulativity用于处理宇宙层级universe的包含。官方文档 doc/sphinx/proofs/writing-proofs/equality.rst 在 “Rewriting with definitional equality” 一节中这样描述changechange {? one_term__from {? at occs_nums } with } one_term__to {? occurrences }若不指定one_term__from则用one_term__to替换结论以及指定的假设若指定one_term__from则把结论/指定假设中匹配到的one_term__from出现替换为one_term__to前提是两者可转换one_term__from中可以出现?x这类模式变量其取值会替换进one_term__to例如change (f ?x ?y) with (g (x, y))。2.2 “其他转换策略”包括哪些“转换类策略”指依赖同一套可转换性检查基础设施的策略。从源码看至少包括change对结论使用累积规则对假设使用转换规则以exact为代表的“项类型必须与目标可转换”的检查路径以及底层 APIconvert/convert_leq分别检查转换与累积见 tactics/tactics.mli。它们的共同点是失败时最终都会抛出同一个NotConvertible异常因此本次改进是“一处修改、全局受益”。三、错误信息的具体变化改造前后对比3.1 旧行为bare Not convertible改造前所有转换失败都统一报Not convertible.用户得不到任何关于“哪两个项”的信息。3.2 新行为带具体项的完整报告改造后错误消息形如Not convertible: True with False.即系统会把参与转换检查的两个项分别用引号打印出来直观展示冲突双方。3.3 官方回归测试给出的精确输出仓库测试套件 test-suite/output/change_not_convertible.v 专门覆盖了该行为文件首行注释即写着 “The Not convertible error should say which terms are not convertible.”其 对应期望输出 精确记录了三种典型失败场景Goal True. Proof. Fail change False. Fail change (1 1). Fail change ?x with (x - x). Abort.期望输出为The command has indeed failed with message: Not convertible: True with False. The command has indeed failed with message: Not convertible: True with 1 1. The command has indeed failed with message: Not convertible: True with True - True.三个用例分别覆盖了直接换目标change False、换成虽同类型但不可转换的命题change (1 1)True与1 1都是Prop却互不转换、以及带模式变量的替换change ?x with (x - x)此时?x被实例化为TrueTrue与True - True不转换。由此可见新消息中的两个项正是“当前被替换的对象”与“替换后想要得到的项”。四、源码级原理错误从产生到打印的完整调用链4.1 异常的载荷化改造NotConvertible携带两个项核心改动位于 tactics/tacticErrors.ml。异常NotConvertible从一个“裸异常”变为携带可选载荷的异常exception NotConvertible of (env * evar_map * constr * constr) optionoption的意义在于兼容两套路径None无法提供具体项的老路径保留向后兼容Some (env, sigma, t1, t2)携带环境、evar 映射以及发生冲突的两个项用于打印诊断信息。4.2 打印逻辑两个项如何进入错误消息错误消息的渲染位于 tactics/tacticErrors.ml| NotConvertible None - str Not convertible. | NotConvertible (Some (env, sigma, t1, t2)) - str Not convertible: spc () quote (Termops.Internal.print_constr_env env sigma t1) spc () str with spc () quote (Termops.Internal.print_constr_env env sigma t2) str .注意这里通过print_constr_env env sigma打印说明打印时充分利用了当前环境与 evar 映射——即使项中包含未决元变量evar也能得到可读的输出。打印出的格式正是测试期望中的Not convertible: t1 with t2.。配套的抛出函数定义在 tactics/tacticErrors.mllet not_convertible ?loc () Loc.raise ?loc (NotConvertible None) let not_convertible_terms ?loc env sigma x y Loc.raise ?loc (NotConvertible (Some (env, sigma, x, y)))其中not_convertible保留旧行为not_convertible_terms是新增的“带项版本”。其接口文档在 tactics/tacticErrors.mli 中明确写道not_convertible_terms与not_convertible相同但会报告未能转换的两个项。4.3 检查发生在哪里infer_conv与convert_gen转换检查本身并不在 tactics 层完成而是由pretyping/reductionops.ml中的infer_conv_gen驱动pretyping/reductionops.ml参数pb决定检查的是累积关系Conversion.CUMUL还是严格转换Conversion.CONV内部先尝试在 evar 存在的前提下做带宇宙约束的可转换性判断失败时再退回带局部宇宙检查的归约比较返回None表示“无法使两个项转换”这正是策略层抛出NotConvertible的触发条件。在策略层tactics/tactics.ml的convert_gen统一封装了这一判断tactics/tactics.mllet convert_gen pb x y Proofview.Goal.enter begin fun gl - let env Proofview.Goal.env gl in let sigma Proofview.Goal.sigma gl in match Reductionops.infer_conv ~pb env sigma x y with | Some sigma - Proofview.Unsafe.tclEVARS sigma | None - TacticErrors.not_convertible_terms env sigma x y | exception e when CErrors.noncritical e - let _, info Exninfo.capture e in TacticErrors.not_convertible_terms ?loc:(Loc.get_loc info) env sigma x y end let convert x y convert_gen Conversion.CONV x y let convert_leq x y convert_gen Conversion.CUMUL x y值得注意的细节当infer_conv本身抛出非致命异常例如转换过程中遇到 anomaly时代码会捕获该异常、提取位置信息并同样通过not_convertible_terms报告两个项保证诊断信息在所有失败路径上的一致性。4.4change策略的具体接入点change策略经过change_on_subterm进入change_and_checktactics/tactics.mllet change_and_check cv_pb mayneedglobalcheck deep t env sigma c match t env sigma with | NoChange - NoChange | Changed (sigma, t) - let sigma check_types env sigma mayneedglobalcheck deep t c in match infer_conv ~pb:cv_pb env sigma t c with | None - TacticErrors.not_convertible_terms env sigma c t | Some sigma - Changed (sigma, t)这里两个项分别是c当前结论/假设中的原始项与t替换后的新项并且顺序为c在前、t在后——即先打印“被替换者”再打印“替换者”。这也解释了测试输出中Not convertible: True with False.的项序来源。change对结论使用累积规则Conversion.CUMUL、对假设使用严格转换Conversion.CONV见change_in_concl/change_in_hyptactics/tactics.ml这一设计也沿用到新错误消息中。4.5 其他转换策略的共享收益exact_check是“其他转换策略”的典型代表tactics/tactics.ml它先对候选证明项c做类型推导再用convert_leq ct concl检查c的类型与目标concl是否满足累积关系失败时同样经由convert_gen → not_convertible_terms输出带两个项的错误。因此所有复用convert/convert_leq/convert_concl的策略包括change内部对结论的convert_concl路径见 tactics/tactics.ml都自动获得了改进后的诊断信息。五、对证明脚本与开发者的影响5.1 对普通用户的体验提升日常使用中遇到change失败时现在可以直接从错误信息里读出冲突双方例如看到Not convertible: True with 1 1立刻知道问题在于目标与期望项在定义上不等价而无需逐项排查。该行为同样适用于now_showchange的同义词以及文档中标注exn:: Not convertible.的所有场景doc/sphinx/proofs/writing-proofs/equality.rst。5.2 对 Ltac / 插件开发者的兼容性说明在 OCaml 插件层面需要注意兼容性变化旧接口Tactics.NotConvertible不带载荷在 tactics/tactics.mli 中已标注自 9.2 起弃用建议改用TacticErrors.not_convertible ()新增的TacticErrors.not_convertible_terms env sigma x y允许插件在需要时主动抛出带两个项的诊断错误NotConvertible异常现在是(env * evar_map * constr * constr) option载荷的异常插件中若自行匹配该异常需要适配None/Some两种形态。5.3 与change_no_check的区别需要澄清一个常见误解change_no_check并不会触发该错误。文档明确指出doc/sphinx/proofs/writing-proofs/equality.rstchange_no_check会跳过可转换性检查作为性能优化因此它不会报Not convertible但代价是可能产生病态项最终由Qed阶段的内核重检兜底。换句话说改进后的详细错误信息只出现在执行检查的策略路径上。六、如何验证与回归如果你在本地构建了该仓库可以通过输出测试output test机制验证此行为# 在 test-suite 目录下运行针对性的输出测试 make output.test # 具体目标名以当前构建系统为准测试用例 test-suite/output/change_not_convertible.v 与其期望输出 test-suite/output/change_not_convertible.out 一一对应任何一行消息格式的改动比如引号样式、项序、措辞都会导致输出测试失败从而保证该诊断格式长期稳定。历史上同一错误信息在旧测试如test-suite/bugs/bug_3387.v中的change x with y at -1. (* Error: Not convertible. *)中的断言也证明了这项改进是向后兼容的升级。七、小结本次#22335变更修复#20944的本质是把转换类策略的失败从“状态码式”的裸异常升级为“诊断式”的结构化异常NotConvertible异常携带了环境、evar 映射与发生冲突的两个项错误消息从Not convertible.进化为Not convertible: t1 with t2.。从 tactics/tacticErrors.ml 的渲染逻辑到 tactics/tactics.ml 的检查点再到 test-suite/output/change_not_convertible.out 的回归断言整条链路清晰可查。对使用者而言这意味着一行更可读、更可定位的错误信息对插件开发者而言这是一次接口层面的兼容性演进——新入口not_convertible_terms让自定义策略也能输出同样专业的诊断。赞分享形式化验证编程语言【免费下载链接】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点击查看免费下载相关推荐ffsubsync日志级别管理从调试信息到错误报告的分级策略ffsubsync日志级别管理从调试信息到错误报告的分级策略 在使用ffsubsync进行字幕同步时日志系统是排查问题的重要工具。本文将详细介绍如何通过日志音视频音频处理视频处理CLIMaybe数据迁移系统升级的数据转换策略Maybe数据迁移系统升级的数据转换策略 你是否曾在系统升级后遇到数据错乱Maybe财务系统作为个人财务操作系统其数据结构升级需要谨慎处理历史财务数据。本后端前端金融科技curl_easy_strerror 详解将 libcurl CURLcode 错误码转换为可读错误信息curl_easy_strerror 详解将 libcurl CURLcode 错误码转换为可读错误信息 curl_easy_strerror 是 libcuCLI网络通信上一篇BRCA1基因功能注释下一篇qm革命性多人协作智能代理平台彻底改变团队工作方式创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考