HoTT/HoTT — pull request #8 by 0x01 (2012-02-03 14:15:28+00:00)
Title: Makefile for Coq/IT

Nothing spectacular, but this is a makefile that recursively compiles the file in Coq/IT (Bas requested me to write this).

Compilation is done by passing -R arguments to coqc/coqide/coqtop. Vladimir's code in place in the "Foundations" namespace and the inductive types code in the "IT" namespace. It generates a .dirlocals file for proofgeneral users and a coqidescript for coq IDE users. These files contain the appropriate -R settings and point to the right coq binary.

I've also slightly modified the way variables are assigned such that you can specifiy the Coq path and coqc binary on the commandline when calling make, like so (for example):

make COQBIN=~/w/htt/coq-8.3pl2/bin/ COQC=coqc.opt

This makefile uses find and sed, unix utilities not available under windows, so MINGW or Cygwin are required to run this under windows.

There is a slight problem with the .depends file (this problem also exists with the other Makefiles in the HoTT repo). The first call to make fails but generates .depends, the second invocation works.

Feel free to pull or not.

Cheers,
Jelle.