これは、Ubuntu Online、Fedora Online、Windows オンライン エミュレーター、MAC OS オンライン エミュレーターなどの複数の無料オンライン ワークステーションの XNUMX つを使用して、OnWorks 無料ホスティング プロバイダーで実行できるコマンド coqchk.opt です。
プログラム：
NAME
coqchk - Coq Proof Checker コンパイル済みライブラリ検証ツール
SYNOPSIS
コックチク [ オプション ] モジュール
DESCRIPTION
コックチク コンパイルされたライブラリ (coqc によって生成された .vo ファイル) のスタンドアロン チェッカーです。
Coq プルーフ アシスタント。 詳細については、リファレンスマニュアルを参照してください。 と返されます
要求されたすべてのタスクが成功した場合は終了コード 0。 ゼロ以外の戻りコードは、次のことを意味します。
何か問題が発生しました: ライブラリが見つからなかったか、コンテンツが破損していたか、型チェックが行われていました
故障等
モジュール チェックするモジュールのリストです。 モジュールは short または
修飾された名前。
OPTIONS
-I 監督、 - 含む DIR
ディレクトリを追加する DIR インクルードパス内
-R DIR コクディル
再帰的に物理的にマップする DIR 論理的に コクディル
-サイレント
coqchk の冗長性を軽減します。
-認める モジュール
指定されたモジュールとそのすべての依存関係を信頼できるものとしてタグ付けします。
他のオプションで明示的に要求されない限り、再チェックされます。
-ノレック モジュール
指定されたモジュールがそのチェックを要求せずに検証されることを指定します。
依存関係。
-NS、 - メモリー
チェッカーが使用するメモリの概要を表示します。
-o、 --出力コンテキスト
検証された論理内容の概要を表示します: 仮定と
予測不可能性の使用法。
-impredicative-set
これにより、チェッカーはこのフラグを使用してコンパイルされたライブラリを受け入れることができます。
-v coqchk のバージョンを出力して終了します。
-coqlib DIR
標準ライブラリのデフォルトの場所をオーバーライドします。
-どこ coqchk 標準ライブラリの場所を出力して終了します。
-NS、 - 助けて
オプションのリストを印刷する
onworks.net サービスを使用してオンラインで coqchk.opt を使用する