这是命令 coqmktop，可以使用我们的多个免费在线工作站之一在 OnWorks 免费托管服务提供商中运行，例如 Ubuntu Online、Fedora Online、Windows 在线模拟器或 MAC OS 在线模拟器
程序：
您的姓名
coqmktop - Coq 证明助手用户策略链接器
概要
科普 [ 选项 ] 档
商品描述
科普 构建一个新的 Coq 顶层扩展用户策略。 档 是目标
Caml 对象或库文件（即后缀为 .cmo、.cmx、.cma 或 .cmxa）以与
考克系统。 链接器生成一个可执行的 Coq 顶层，可以直接调用
或通过 考克(1)、使用 -image 选项。
配置
-h 帮助。 列出可用选项。
-源目录 DIR
指定 Coq 源文件的位置
-o 执行文件
指定生成的顶层的名称
-选择 在本机代码中编译
-充分 链接高级策略
-最佳 在 ocaml 顶层构建 Coq（与 -选择)
-R DIR 为 Ocaml 指定递归目录
-v8 与 V8 语法链接
使用 onworks.net 服务在线使用 coqmktop