-
Notifications
You must be signed in to change notification settings - Fork 2
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
1 parent
038075c
commit 51e2b08
Showing
1 changed file
with
142 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,142 @@ | ||
# -*- 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/ | ||
|
||
coq2html: | ||
../coq2html/coq2html \ | ||
-fragile-mathcomp-break \ | ||
-title "Mathcomp Analysis" \ | ||
-d html/ -base mathcomp -Q theories analysis \ | ||
-coqlib https://coq.inria.fr/doc/V8.18.0/stdlib/ \ | ||
-external https://math-comp.github.io/htmldoc/ mathcomp.ssreflect \ | ||
-external https://math-comp.github.io/htmldoc/ mathcomp.algebra \ | ||
classical/*.v classical/*.glob \ | ||
theories/*.v theories/*.glob | ||
|
||
coq2html-clean: | ||
rm -f */*.glob |