coqchk - 云端在线

程序：

您的姓名

coqchk - Coq Proof Checker 编译库验证器

概要

知乎 [ 选项 ] 模块

商品描述

知乎 是编译库（由 coqc 生成的 .vo 文件）的独立检查器，用于
Coq 证明助手。 有关详细信息，请参阅参考手册。 它返回
如果所有请求的任务都成功，则退出代码 0。 非零返回码意味着
出了点问题：找不到某个库，内容损坏，类型检查
失败等

模块 是要检查的模块列表。 模块可以通过短或
限定名称。

配置

-I 是， - 包括 DIR
添加目录 DIR 在包含路径中

-R DIR 目录
递归映射物理 DIR 合乎逻辑 目录

-无声
使 coqchk 不那么冗长。

-承认 模块
将指定的模块及其所有依赖项标记为受信任，并且不会被
重新检查，除非其他选项明确要求。

-诺雷克 模块
指定应验证给定模块而不要求检查其
依赖性。

-米， - 记忆
显示检查器使用的内存的摘要。

-o， --输出上下文
显示已验证的逻辑内容的摘要：假设和
不可预测性的使用。

- 谓语集
允许检查器接受已使用此标志编译的库。

-v 打印 coqchk 版本并退出。

-coqlib DIR
覆盖标准库的默认位置。

-在哪里 打印 coqchk 标准库位置并退出。

-H， - 帮帮我
打印选项列表

使用 onworks.net 服务在线使用 coqchk