Skip to content
This repository

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Fetching contributors…

Cannot retrieve contributors at this time

file 50 lines (37 sloc) 1.622 kb
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50
ACLOCAL_AMFLAGS = -I etc
bin_SCRIPTS = hoqtop hoqc
hottdir=$(datarootdir)/hott
EXTRA_DIST = coq theories etc LICENSE.txt CREDITS.txt INSTALL.txt README.markdown

# The list of files that comprise the library
VFILES=$(shell find $(srcdir)/theories -name "*.v")
VOFILES:=$(VFILES:.v=.vo)
GLOBFILES:=$(VFILES:.v=.glob)

# The list of files that comprise the alternative standard library
STDVFILES=$(shell find $(srcdir)/coq -name "*.v")
STDVOFILES:=$(STDVFILES:.v=.vo)
STDGLOBFILES:=$(STDVFILES:.v=.glob)

nobase_hott_DATA = $(VOFILES) $(STDVOFILES) $(shell find $(srcdir)/coq/theories -name "README.txt")

# The Coq compiler, adapted to HoTT
HOQC=$(srcdir)/hoqc

# Which files should be cleaned
CLEANFILES = $(VOFILES) $(GLOBFILES) $(STDVOFILES) $(STDGLOBFILES)

.PHONY: .depend

.depend:
$(COQDEP) -nois -coqlib $(srcdir)/coq -I theories -R coq/theories Coq $(VFILES) $(STDVFILES) > .depend

install-data-local:
$(mkdir_p) $(hottdir)/coq
rm -f $(hottdir)/coq/dev $(hottdir)/coq/plugins
ln -s $(COQLIB)/dev $(hottdir)/coq
ln -s $(COQLIB)/plugins $(hottdir)/coq

# The standard library files must be compiled in a special way
$(STDVOFILES) : %.vo : %.v
$(COQTOP) -boot -nois -R $(srcdir)/coq/theories Coq -compile $(basename $<)

# The standard library files must be compiled in a special way
$(STDGLOBFILES) : %.glob : %.v
$(COQTOP) -boot -nois -R $(srcdir)/coq/theories Coq -compile $(basename $<)

# The HoTT files depend on the new standard library, but coqdep will not figure that out.
$(VOFILES) : $(STDVOFILES)

# A rule for compiling the HoTT libary files
$(VOFILES) : %.vo : %.v
$(HOQC) $<

-include .depend
Something went wrong with that request. Please try again.