#Coqマニュアル 14.3 Creating a Makefile for Coq modules の和訳。

Coqモジュールのための Makefile をつくる

ソースコードの規模がでかくなって、ファイルがいくつかあるときは make とかを使うのが重要です。 でも、一般的で完全なMakefileを書くのは面倒なので、 それを自動で生成するツール coq_makefile を提供します。 コンパイルしたいファイルを与えるとcoq_makefileコマンドはMakefileを標準出力に出力します。

ちょうど次のように使うことが出来ます。

 $ coq_makefile file1.v … filen.v > Makefile

出力されるMakefileにはdependターゲットがあり、それは依存関係を計算して別のファイル“.depend”に保存します。 なので、makeの最初の実施の前にそのファイルを作らなければなりません。 例えば次のコマンドをしてください。

 $ touch .depend

初期化、または依存関係の更新のために次をタイプしてください。

 $ make depend

file 1からfile nまでをすべてコンパイルするターゲットallがあります。そして.vファイルに対応する一般的なターゲット.voもあります。(make file.voと打つとfile.vがコンパイルされるのです。) coq_makefileはMLファイルやサブディレクトリをハンドルする事も出来ます。

詳細のオプションは次を打ってください。

 $ coq_makefile --help

coq_makefile –help

Usage summary:

coq_makefile [subdirectory] .... [file.v] ... [file.ml] ... [-custom
  command dependencies file] ... [-I dir] ... [-R physicalpath logicalpath]
  ... [VARIABLE = value] ...  [-opt|-byte] [-impredicative-set] [-no-install]
  [-f file] [-o file] [-h] [--help]

[file.v]: Coq file to be compiled
[file.ml]: Objective Caml file to be compiled
[subdirectory] : subdirectory that should be "made"
[-custom command dependencies file]: add target "file" with command
  "command" and dependencies "dependencies"
[-I dir]: look for dependencies in "dir"
[-R physicalpath logicalpath]: look for dependencies resursively starting from
 "physicalpath". The logical path associated to the physical path is
 "logicalpath".
[VARIABLE = value]: Add the variable definition "VARIABLE=value"
[-byte]: compile with byte-code version of coq
[-opt]: compile with native-code version of coq
[-impredicative-set]: compile with option -impredicative-set of coq
[-no-install]: build a makefile with no install target
[-f file]: take the contents of file as arguments
[-o file]: output should go in file file
[-h]: print this usage summary
[--help]: equivalent to [-h]