これは、Ubuntu Online、Fedora Online、Windows オンライン エミュレーター、MAC OS オンライン エミュレーターなどの複数の無料オンライン ワークステーションの XNUMX つを使用して、OnWorks 無料ホスティング プロバイダーで実行できるコマンド coqmktop です。
プログラム：
NAME
coqmktop - Coq Proof Assistant ユーザー戦術リンカー
SYNOPSIS
コクムクトップ [ オプション ] ファイル
DESCRIPTION
コクムクトップ ユーザー戦術で拡張された新しい Coq トップレベルを構築します。 ファイル が目的です
Caml オブジェクトまたはライブラリ ファイル (つまり、拡張子 .cmo、.cmx、.cma、または .cmxa が付いているもの) とリンクします。
コックシステム。 リンカーは、直接呼び出すことができる実行可能な Coq トップレベルを生成します。
またはを通じて コック(1) -image オプションを使用します。
OPTIONS
-h ヘルプ。 利用可能なオプションをリストします。
-srcdir DIR
Coq ソース ファイルの場所を指定する
-o execファイル
結果のトップレベルの名前を指定します
-選択する ネイティブコードでコンパイルする
-フル 高度な戦術をリンクする
-上 ocaml トップレベルで Coq をビルドします (ocaml と互換性がありません) -選択する)
-R DIR Ocaml のディレクトリを再帰的に指定する
-v8 V8 文法とのリンク
onworks.net サービスを使用してオンラインで coqmktop を使用する