Makefile 2.56 KB
Newer Older
POTTIER Francois's avatar
POTTIER Francois committed
1
.PHONY: all coqlib generator examples doc clean install uninstall reinstall
charguer's avatar
charguer committed
2

3 4
CFML := $(shell pwd)

charguer's avatar
charguer committed
5

6 7 8 9 10 11 12 13 14 15 16 17
##############################################################################
# Installation destinations.

DEFAULT_PREFIX := $(shell opam config var prefix)
ifeq ($(DEFAULT_PREFIX),)
	DEFAULT_PREFIX := /usr/local
endif

PREFIX ?= $(DEFAULT_PREFIX)
BINDIR ?= $(PREFIX)/bin
LIBDIR ?= $(PREFIX)/lib/cfml

18 19 20
COQ_WHERE   ?= $(shell $(COQBIN)coqc -where)
COQ_CONTRIB := $(COQ_WHERE)/user-contrib

21 22
##############################################################################
# Targets.
charguer's avatar
charguer committed
23

POTTIER Francois's avatar
POTTIER Francois committed
24
all: coqlib generator
25
	$(MAKE) CFMLC=$(CFML)/generator/main.native -C lib/stdlib
charguer's avatar
charguer committed
26

charguer's avatar
charguer committed
27
coqlib:
28
	$(MAKE) CFML=$(CFML) -C lib/coq proof
charguer's avatar
charguer committed
29

POTTIER Francois's avatar
POTTIER Francois committed
30
generator:
31
	rm -f generator/cfml_config.ml
32
	sed -e 's|@@LIBDIR@@|$(LIBDIR)|' \
33
	    generator/cfml_config.ml.in > generator/cfml_config.ml
34
	$(MAKE) -C generator
charguer's avatar
charguer committed
35

POTTIER Francois's avatar
POTTIER Francois committed
36
examples: all
37
	$(MAKE) CFML=$(CFML) -C examples
charguer's avatar
charguer committed
38

39 40
##############################################################################
# Documentation.
charguer's avatar
charguer committed
41

42
DOC := README.html lib/coq/README.html generator/README.html
charguer's avatar
charguer committed
43

44
doc: $(DOC)
charguer's avatar
charguer committed
45 46 47

%.html: %.md
	pandoc -o $@ $<
charguer's avatar
charguer committed
48

49 50 51 52 53 54 55
##############################################################################
# Cleanup.

clean:
	$(MAKE) -C lib/coq $@
	$(MAKE) -C lib/stdlib $@
	$(MAKE) -C generator $@
56
	rm -f generator/cfml_config.ml
57
	rm -f $(DOC)
58 59 60 61

##############################################################################
# Installation.

62 63 64 65 66
# As install depends on all, the file generator/cfml_config.ml is regenerated
# when `make install` is run; this ensures LIBDIR cannot be inconsistent.

install: all
	# Install the generator binary
67
	install -m755 $(CFML)/generator/_build/main.native $(BINDIR)/cfmlc
68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85
#	install -m755 $(CFML)/generator/_build/makecmj.native $(BINDIR)/cfml_cmj

	# Cleanup LIBDIR
	rm -rf $(LIBDIR)

	# Install the stdlib .cmj files
	mkdir -p $(LIBDIR)/stdlib
	install $(CFML)/lib/stdlib/*.cmj $(LIBDIR)/stdlib

	# Install the auxiliary makefiles
	mkdir -p $(LIBDIR)/make
	install $(CFML)/lib/make/Makefile.cfml $(LIBDIR)/make
	install -m755 $(CFML)/lib/make/ocamldep.post $(LIBDIR)/make

	# Cleanup COQ_CONTRIB/CFML
	rm -rf $(COQ_CONTRIB)/CFML

	# Install the CFML core coq library
86 87
	mkdir -p $(COQ_CONTRIB)/CFML
	install $(CFML)/lib/coq/*.vo $(COQ_CONTRIB)/CFML
88 89 90 91 92

	# Install the CFML stdlib coq library
	mkdir -p $(COQ_CONTRIB)/CFML/Stdlib
	install $(CFML)/lib/stdlib/*.vo $(COQ_CONTRIB)/CFML/Stdlib

93 94
	# "Installation completed."

95
uninstall:
96
	rm -f $(BINDIR)/cfmlc
97 98
#	rm -f $(BINDIR)/cfml_cmj
	rm -rf $(LIBDIR)
99
#	rm -rf $(DOCDIR)
100
	rm -rf $(COQ_CONTRIB)/CFML
POTTIER Francois's avatar
POTTIER Francois committed
101 102 103

reinstall: uninstall
	@ $(MAKE) install