#Coqマニュアル [14.3 Creating a Makefile for Coq modules](http://coq.inria.fr/doc/Reference-Manual018.html) の和訳。

## 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

~~~ { .shell }
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]
~~~