analysis/Makefile.common at master · mkerjean/analysis · GitHub

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
# -*- 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 command -v coqtop || command -v rocq))
COQMAKEFILE?=$(shell command -v coq_makefile || echo "$(COQBIN)rocq makefile")
COQC?=$(shell command -v coqc || echo "$(COQBIN)rocq c")
COQDEP?=$(shell command -v coqdep || echo "$(COQBIN)rocq dep")
COQDOC?=$(shell command -v coqdoc || echo "$(COQBIN)rocq doc")
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')

# 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) $@

# Html documentation

DOCDIR=html

GIT_HASH := $(shell git describe --tags --exact-match 2>/dev/null || git rev-parse --short HEAD)

$(DOCDIR)/dependency_graph.pre:
	mkdir -p $(DOCDIR)
	coqdep -f _CoqProject | perl etc/builddoc_dependency_dot.pl > $(DOCDIR)/dependency_graph.pre

$(DOCDIR)/dependency_graph.dot: $(DOCDIR)/dependency_graph.pre
	tred $(DOCDIR)/dependency_graph.pre > $(DOCDIR)/dependency_graph.dot

html: build $(DOCDIR)/dependency_graph.dot
	etc/rocqnavi_generate-hierarchy-graph.sh $(DOCDIR)/hierarchy_graph.dot
	find . -name "*.v" -or -name "*.glob" | grep -v "/\." | grep -v "_opam/" | xargs rocqnavi \
	-title "Mathcomp Analysis $(GIT_HASH)" \
	-d $(DOCDIR) -Q theories mathcomp.analysis \
	-Q classical mathcomp.classical \
	-Q reals mathcomp.reals \
	-Q reals_stdlib mathcomp.reals_stdlib \
	-Q experimental_reals mathcomp.experimental_reals \
	-Q analysis_stdlib mathcomp.analysis_stdlib \
	-coqlib https://rocq-prover.org/doc/V9.0.0/stdlib/ \
	-dependency-graph $(DOCDIR)/dependency_graph.dot \
	-hierarchy-graph $(DOCDIR)/hierarchy_graph.dot \
        -index-blacklist etc/rocqnavi_index-blacklist \
        -show-type-information-using-coqtop-process \
	-external https://math-comp.github.io/htmldoc_2_4_0/ mathcomp.ssreflect \
	-external https://math-comp.github.io/htmldoc_2_4_0/ mathcomp.algebra