diff --git a/Makefile b/Makefile index e610365..e026341 100644 --- a/Makefile +++ b/Makefile @@ -1,14 +1,3 @@ -.PHONY=all clean - -all: Makefile.coq - $(MAKE) -f Makefile.coq - -install: Makefile.coq - $(MAKE) install -f Makefile.coq - -Makefile.coq: _CoqProject - coq_makefile -f _CoqProject -o Makefile.coq - -clean: Makefile.coq - $(MAKE) -f Makefile.coq clean - rm -r Makefile.coq +# -*- Makefile -*- +# Main Makefile +include Makefile.common diff --git a/Makefile.common b/Makefile.common new file mode 100644 index 0000000..3f45682 --- /dev/null +++ b/Makefile.common @@ -0,0 +1,87 @@ +# -*- 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) + +# all: --------------------------------------------------------------- +all: config build + +# Makefile.coq: ------------------------------------------------------ +.PHONY: pre-makefile + +Makefile.coq: pre-makefile 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 $(OTHERCLEAN) + 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$$' Make) + +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) $@