diff options
| author | Cyril Cohen | 2018-07-31 10:37:25 +0200 |
|---|---|---|
| committer | Cyril Cohen | 2018-07-31 11:38:53 +0200 |
| commit | 4199c23da311e612cb1ae45cf5519b5f3947c3b3 (patch) | |
| tree | 4e887d501dd9d1f5d983ca236cbadcd803c8a091 /mathcomp/all/Makefile | |
| parent | 6c6c907438f4179ac335e7daa9f1ed030c0c8259 (diff) | |
Rework the whole Makefile architecture
- Cleanup, refactoring and generalize the makefile architecture
- Reuses @strub math-comp/analysis Makefile / Makefile.common organization
- As #174, this fixes #88, but looks more stable than trying to fix the use of the MAKEFLAGS internal variable
Diffstat (limited to 'mathcomp/all/Makefile')
| -rw-r--r-- | mathcomp/all/Makefile | 35 |
1 files changed, 19 insertions, 16 deletions
diff --git a/mathcomp/all/Makefile b/mathcomp/all/Makefile index a58be7b..30204d2 100644 --- a/mathcomp/all/Makefile +++ b/mathcomp/all/Makefile @@ -1,22 +1,25 @@ -H=@ +# -*- Makefile -*- -ifeq "$(COQBIN)" "" -COQBIN=$(dir $(shell which coqtop))/ -endif +COQPROJECT="Make" -OLD_MAKEFLAGS:=$(MAKEFLAGS) -MAKEFLAGS+=-B +# -------------------------------------------------------------------- +include Makefile.common -.DEFAULT_GOAL := all +# -------------------------------------------------------------------- +COQMAKEOPTIONS=--no-print-directory -%: - $(H)[ -e Makefile.coq ] || $(COQBIN)/coq_makefile -f Make -o Makefile.coq - $(H)MAKEFLAGS="$(OLD_MAKEFLAGS)" $(MAKE) --no-print-directory \ - -f Makefile.coq $* +# -------------------------------------------------------------------- +.PHONY: install -.PHONY: clean -clean: - $(H)MAKEFLAGS="$(OLD_MAKEFLAGS)" $(MAKE) --no-print-directory \ - -f Makefile.coq clean - $(H)rm -f Makefile.coq +install: + $(MAKE) -f Makefile.coq install + +# -------------------------------------------------------------------- +.PHONY: count + +COQFILES := $(shell grep '.v$$' Make) + +count: + @coqwc $(COQFILES) | tail -1 | \ + awk '{printf ("%d (spec=%d+proof=%d)\n", $$1+$$2, $$1, $$2)}' |