これは、Ubuntu Online、Fedora Online、Windows オンライン エミュレーター、または MAC OS オンライン エミュレーターなどの複数の無料オンライン ワークステーションの XNUMX つを使用して、OnWorks 無料ホスティング プロバイダーで実行できるコマンド coqdep です。
プログラム：
NAME
coqdep - Coq および Caml プログラムのモジュール間の依存関係を計算します
SYNOPSIS
コックデプ [ -w ] [ -I ディレクトリにジョブを開始します。 ] [ -coqlib ディレクトリにジョブを開始します。 ] [ -c ] [ -i ] [ -D ] [ -スラッシュ ]
ファイル名 ... ディレクトリにジョブを開始します。 ...
DESCRIPTION
コックデプ Coq および Caml プログラムのモジュール間の依存関係を計算し、
make で読み取り可能な形式の標準出力への依存関係。 ディレクトリが
引数として与えられると、再帰的に調べられます。
Coq モジュールの依存関係は、以下を参照して計算されます。 必要とする コマンド (必須、必須
エクスポート、インポートが必要）、 宣言する ML モジュール コマンドと 負荷 コマンド。 依存関係
Coq ライブラリのモジュールに関連するものは出力されません。
Caml モジュールの依存関係は、以下を参照して計算されます。 開いた ディレクティブとドット
表記法 モジュールの値.
OPTIONS
-c Caml モジュールの依存関係を出力します。 (Caml モジュールでは、動作は次のようになります)
ocamldep とまったく同じです)。
-w Coq コマンドが実行された場合に警告を出力します。 宣言する ML モジュール 間違っています。 （例えば、
「ML モジュール "A" を宣言します。」と書きましたが、モジュール A には #open "B" が含まれています)。 の
正しいコマンドが出力されます (オプション -D を参照)。 警告は標準で印刷されています
エラー。
-D このコマンドはすべてのコマンドを検索します 宣言する ML モジュール として与えられる各 Coq ファイルの
引数を指定し、(必要に応じて) Caml モジュールのリストを完成させます。 新しいコマンドは
標準出力に出力されます。 このオプションでは依存関係は計算されません。
-スラッシュ OS 固有の区切り文字の代わりにスラッシュを使用してパスを出力します。 このオプションは
Cygwin で開発する場合に便利です。
-I ディレクトリにジョブを開始します。
ディレクトリのファイル .v .ml .mli ディレクトリにジョブを開始します。 の際に考慮されます。
依存関係の計算は可能ですが、それ自体の依存関係は出力されません。
-coqlib ディレクトリにジョブを開始します。
Coq ライブラリの場所を示します。 デフォルト値は次のように決定されています。
したがって、このオプションは通常の環境では使用しないでください。
状況。
onworks.net サービスを使用してオンラインで coqdep を使用する
