Makefile 2.79 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
##############################################################################
# Targets.
charguer's avatar
charguer committed
20

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

charguer's avatar
charguer committed
24
coqlib:
25
	$(MAKE) CFML=$(CFML) -C lib/coq proof
charguer's avatar
charguer committed
26

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

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

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

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

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

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

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

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

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

POTTIER Francois's avatar
POTTIER Francois committed
61 62 63
# If ARTHUR is defined, create a symbolic link from Coq's user-contrib
# directory to this directory (cfml). Otherwise, perform a copy.
# TEMPORARY, this is TODO
64

65 66 67 68 69 70 71 72
COQ_WHERE   := $(shell $(COQBIN)coqc -where)
COQ_CONTRIB := $(COQ_WHERE)/user-contrib

# 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
73
	install -m755 $(CFML)/generator/_build/main.native $(BINDIR)/cfmlc
74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91
#	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
92 93
	mkdir -p $(COQ_CONTRIB)/CFML
	install $(CFML)/lib/coq/*.vo $(COQ_CONTRIB)/CFML
94 95 96 97 98

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

99 100
	# "Installation completed."

101
uninstall:
102
	rm -f $(BINDIR)/cfmlc
103 104 105 106
#	rm -f $(BINDIR)/cfml_cmj
	rm -rf $(LIBDIR)
	rm -rf $(DOCDIR)
	rm -rf $(COQ_CONTRIB)/CFML
POTTIER Francois's avatar
POTTIER Francois committed
107 108 109

reinstall: uninstall
	@ $(MAKE) install