これは、Ubuntu Online、Fedora Online、Windows オンライン エミュレーター、または MAC OS オンライン エミュレーターなどの複数の無料オンライン ワークステーションの XNUMX つを使用して、OnWorks 無料ホスティング プロバイダーで実行できるコマンド coqide です。
プログラム：
NAME
coqide - Coq Proof Assistant グラフィカル インターフェイス
SYNOPSIS
コキド [ オプション ]
DESCRIPTION
コキド Coq 証明アシスタント用の gtk グラフィカル インターフェイスです。
Coq のコマンドライン指向の使用については、を参照してください。 コクトップ(1) ; Coq のバッチ指向の使用については、を参照してください。
コックとします。
OPTIONS
-h で受け入れられるオプションの完全なリストを表示します コキド.
-I DIR, -含める DIR
インクルード パスにディレクトリ dir を追加します。
-R DIR コクディル
物理的なマッピングを再帰的に行う DIR 論理的に コクディル.
-src インクルード パスにソース ディレクトリを追加します。
-です f, -入力状態 f
状態の読み取り元 f.coq.
-ノイズ 空の状態から始めます。
-出力状態 f
状態をファイルに書き込む f.coq.
-load-ml-オブジェクト f
MLオブジェクトファイルの読み込み f.
-load-ml-ソース f
MLファイルをロードする f.
-l f, -load-vernac-ソース f
Coqファイルをロードする f.v (ロード f。）
-lv f, -load-vernac-source-verbose f
Coqファイルをロードする f.v (冗長ロード f。）
-load-vernac-object f
Coqオブジェクトファイルをロードする f.vo.
-必須 f
Coqオブジェクトファイルをロードする f.vo を選択してインポートします (必須 f。）
-コンパイル f
Coq ファイルをコンパイルする f.v (暗黙的に -バッチ).
-コンパイル-冗長 f
Coq ファイルを詳細にコンパイルする f.v (暗黙的に -バッチ).
-選択する Coq または Coq_SearchIsos のネイティブ コード バージョンを実行します。
-バイト Coq または Coq_SearchIsos のバイトコード バージョンを実行します。
-どこ Coq の標準ライブラリの場所を出力して終了します。
-v Coq バージョンを出力して終了します。
-q rcfileのロードをスキップします。
-init-ファイル f
rcfileを次のように設定します f.
-バッチ バッチ モード (引数の解析直後に終了します)。
-ブート ブートモード (暗黙的に -q & -バッチ).
-emacs Emacs で実行されることを Coq に伝えます。
-ダンプグロブ f
グローバリゼーションをファイルにダンプする f (使用するのは コクドック（1））。
-impredicative-set
ソートの設定 述語を設定します。
-ドントロードプルーフ
不透明なプルーフをメモリにロードしないでください。
-xml XML ファイルをディレクトリをルートとする階層にエクスポートします。
COQ_XML_LIBRARY_ROOT (設定されている場合)、または標準出力 (未設定の場合)。
onworks.net サービスを使用してオンラインで coqide を使用する
