这是可以使用我们的多个免费在线工作站之一在 OnWorks 免费托管服务提供商中运行的命令 coqc，例如 Ubuntu Online、Fedora Online、Windows 在线模拟器或 MAC OS 在线模拟器
程序：
您的姓名
coqc - Coq 证明助手编译器
概要
考克 [ 一般 公鸡 选项 ] 文件
商品描述
考克 是 Coq Proof Assistant 的批处理编译器。 选项基本上是
一样 科克托普（1）。 文件.v 是要编译的白话文件。 文件 必须只形成
包含字符 `a` 到 `Z`、`0`-`9` 或 `_`，并且必须以字母开头。 这
编译器产生一个目标文件 文件.vo.
有关 Coq 的交互式使用，请参阅 科克托普（1）。
配置
考克 是一个简单运行的脚本 科克托普 带选项 -编译 它接受相同的选项
as 科克托普。
-图片 箱子
使用 箱子 作为底层 科克托普 而不是默认的。
-冗长
在标准输出上打印编译后的文件。
使用 onworks.net 服务在线使用 coqc
