Makefile.common

# -*- 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 -Q classical mathcomp.classical -Q 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/

coq2html:
	coqdep -f _CoqProject > depend.d
	../coq2html/ocamldot/ocamldot depend.d > depend.dot
	gsed -i 's/Classical/mathcomp\.classical/' depend.dot
	gsed -i 's/Theories/mathcomp\.analysis/' depend.dot
	gsed -i 's/Reals_stdlib/mathcomp\.reals_stdlib/' depend.dot
	gsed -i 's/Experimental_reals/mathcomp\.experimental_reals/' depend.dot
	gsed -i 's/Reals/mathcomp\.reals/' depend.dot
	gsed -i 's/Analysis_stdlib/mathcomp\.analysis_stdlib/' depend.dot
	gsed -i 's/\//\./g' depend.dot
	../coq2html/tools/generate-hierarchy-graph.sh
	find . -not -path '*/.*' -name "*.v" -or -name "*.glob" | xargs ../coq2html/coq2html \
  -hierarchy-graph hierarchy-graph.dot \
  -dependency-graph depend.dot \
  -title "Mathcomp Analysis" \
  -d html/ -base mathcomp -Q theories analysis \
  -coqlib https://coq.inria.fr/doc/V8.19.2/stdlib/ \
  -external https://math-comp.github.io/htmldoc/ mathcomp.ssreflect \
  -external https://math-comp.github.io/htmldoc/ mathcomp.algebra

coq2html-clean:
	rm -f */*.glob