forked from math-comp/analysis
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Makefile.common
128 lines (101 loc) · 3.98 KB
/
Makefile.common
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
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
# -*- Makefile -*-
######################################################################
# USAGE: #
# The rules this-config::, this-build::, this-distclean::, #
# pre-makefile::, this-clean:: and __always__:: may be extended #
# Additionally, the following variables may be customized: #
SUBDIRS?=
COQBIN?=$(dir $(shell which coqtop))
COQMAKEFILE?=$(COQBIN)coq_makefile
COQDEP?=$(COQBIN)coqdep
COQPROJECT?=_CoqProject
COQMAKEOPTIONS?=
COQMAKEFILEOPTIONS?=
V?=
VERBOSE?=V
######################################################################
# local context: -----------------------------------------------------
.PHONY: all config build clean distclean __always__
.SUFFIXES:
H:= $(if $(VERBOSE),,@) # not used yet
TOP = $(dir $(lastword $(MAKEFILE_LIST)))
COQMAKE = $(MAKE) -f Makefile.coq $(COQMAKEOPTIONS)
BRANCH_coq:= $(shell $(COQBIN)coqtop -v | head -1 | grep -E '(trunk|master)' \
| wc -l | sed 's/ *//g')
# coq version:
ifneq "$(BRANCH_coq)" "0"
COQVVV:= dev
else
COQVVV:=$(shell $(COQBIN)coqtop --print-version | cut -d" " -f1)
endif
COQV:= $(shell echo $(COQVVV) | cut -d"." -f1)
COQVV:= $(shell echo $(COQVVV) | cut -d"." -f1-2)
# all: ---------------------------------------------------------------
all: config build
# Makefile.coq: ------------------------------------------------------
.PHONY: pre-makefile
Makefile.coq: pre-makefile $(COQPROJECT) Makefile
$(COQMAKEFILE) $(COQMAKEFILEOPTIONS) -f $(COQPROJECT) -o Makefile.coq
# Global config, build, clean and distclean --------------------------
config: sub-config this-config
build: sub-build this-build
clean: sub-clean this-clean
distclean: sub-distclean this-distclean
# Local config, build, clean and distclean ---------------------------
.PHONY: this-config this-build this-distclean this-clean
this-config:: __always__
this-build:: this-config Makefile.coq
+$(COQMAKE)
this-distclean:: this-clean
rm -f Makefile.coq Makefile.coq.conf Makefile.coq
this-clean:: __always__
@if [ -f Makefile.coq ]; then $(COQMAKE) cleanall; fi
# Install target -----------------------------------------------------
.PHONY: install
install: __always__ Makefile.coq
$(COQMAKE) install
# counting lines of Coq code -----------------------------------------
.PHONY: count
COQFILES = $(shell grep '.v$$' $(COQPROJECT))
count:
@coqwc $(COQFILES) | tail -1 | \
awk '{printf ("%d (spec=%d+proof=%d)\n", $$1+$$2, $$1, $$2)}'
# Additionally cleaning backup (*~) files ----------------------------
this-distclean::
rm -f $(shell find . -name '*~')
# Make in SUBDIRS ----------------------------------------------------
ifdef SUBDIRS
sub-%: __always__
@set -e; for d in $(SUBDIRS); do +$(MAKE) -C $$d $(@:sub-%=%); done
else
sub-%: __always__
@true
endif
# Make of individual .vo ---------------------------------------------
%.vo: __always__ Makefile.coq
+$(COQMAKE) $@
# the doc targets doc and doc-clean are essentially copied from the Mathematical
# Components repository
# we reuse the scripts from the math-comp git repo (which is hard wired)
# modulo one fix: we change builddoc_lib.sh:l.18 to s/\(\*{5,}+\)//g;
MATHCOMP = ../math-comp/
doc: __always__ Makefile.coq
mkdir -p _build_doc/
cp -r $(COQFILES) -t _build_doc/ --parents
cp _CoqProject Makefile* _build_doc
mkdir -p _build_doc/htmldoc
. $(MATHCOMP)etc/utils/builddoc_lib.sh; \
cd _build_doc && mangle_sources $(COQFILES)
+cd _build_doc && $(COQMAKE)
# let's forget about the dependency graph for the time being...
# cd _build_doc && grep -v vio: .Makefile.coq.d > depend
# cd _build_doc && cat depend | $(MATHCOMP)etc/buildlibgraph $(COQFILES) > htmldoc/depend.js
cd _build_doc && $(COQBIN)coqdoc -t "MathComp Analysis" \
-g --utf8 -R classical mathcomp.classical -R theories mathcomp.analysis \
--parse-comments \
--multi-index $(COQFILES) -d htmldoc
. $(MATHCOMP)etc/utils/builddoc_lib.sh; \
cd _build_doc && postprocess_html
cp $(MATHCOMP)etc/artwork/coqdoc.css _build_doc/htmldoc
doc-clean:
rm -rf _build_doc/