Hatena::Groupcoq

mzpの日記

 | 

2009-12-05

Coq + omake =さいきょう

coqcで複数ファイルをコンパイルするのって面倒ですよね。依存関係も考慮しないといけないし。

そんなときは、omakeですね!

というわけで、Coqのソースコードをコンパイルするのに必要なルールをいくつか書きました。

A.v、B.v、C.vからなる証明をコンパイルしたいときは

.DEFAULT: $(Proof A B C)

とするだけでOKです。ちゃんとA.v、B.v、C.vの間の依存関係も解析してます。

あと、omakeなので当然omake -Pで継続ビルドもできちゃいます。

ソースコード

s# ------------------------------------------------------------
# ルール部
# ------------------------------------------------------------
# コンパイル
%.vo %.glob: %.v
	coqc $<

# 依存関係の解析
# パスは適宜変更してください
.SCANNER: %.vo: %.v
	coqdep -w -coqlib /opt/local/lib/coq/ -I . $<

# 便利関数
public.Proof(files) =
	vo=$(addsuffix .vo,$(files))
	value $(vo)

# ------------------------------------------------------------
# 利用例:
# A.v B.v C.vをコンパイルしたい場合
# ------------------------------------------------------------
FILES[] =
	A
	B
	C

.DEFAULT: $(Proof $(FILES))

.PHONY: clean
clean:
	rm -f *.vo *.glob *~ *.omc .omakedb .omakedb.lock *.html

参考

The OMake build system

ゲスト



トラックバック - http://coq.g.hatena.ne.jp/mzp/20091205
 |