diff options
Diffstat (limited to 'coqprime/Makefile')
| -rw-r--r-- | coqprime/Makefile | 160 |
1 files changed, 113 insertions, 47 deletions
diff --git a/coqprime/Makefile b/coqprime/Makefile index 8fa838a1e..c8e44a658 100644 --- a/coqprime/Makefile +++ b/coqprime/Makefile @@ -2,7 +2,7 @@ ## v # The Coq Proof Assistant ## ## <O___,, # INRIA - CNRS - LIX - LRI - PPS ## ## \VV/ # ## -## // # Makefile automagically generated by coq_makefile V8.4pl6 ## +## // # Makefile automagically generated by coq_makefile V8.5pl1 ## ############################################################################# # WARNING @@ -19,9 +19,10 @@ .DEFAULT_GOAL := all -# # This Makefile may take arguments passed as environment variables: # COQBIN to specify the directory where Coq binaries resides; +# TIMECMD set a command to log .v compilation time; +# TIMED if non empty, use the default time command as TIMECMD; # ZDEBUG/COQDEBUG to specify debug flags for ocamlc&ocamlopt/coqc; # DSTROOT to specify a prefix to install path. @@ -33,14 +34,25 @@ endef includecmdwithout@ = $(eval $(subst @,$(donewline),$(shell { $(1) | tr -d '\r' | tr '\n' '@'; }))) $(call includecmdwithout@,$(COQBIN)coqtop -config) +TIMED= +TIMECMD= +STDTIME?=/usr/bin/time -f "$* (user: %U mem: %M ko)" +TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD)) + +vo_to_obj = $(addsuffix .o,\ + $(filter-out Warning: Error:,\ + $(shell $(COQBIN)coqtop -q -noinit -batch -quiet -print-mod-uid $(1)))) + ########################## # # # Libraries definitions. # # # ########################## -COQLIBS?= -R Coqprime Coqprime -COQDOCLIBS?=-R Coqprime Coqprime +COQLIBS?=\ + -R "Coqprime" Coqprime +COQDOCLIBS?=\ + -R "Coqprime" Coqprime ########################## # # @@ -54,10 +66,11 @@ COQDEP?="$(COQBIN)coqdep" -c COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML) COQCHKFLAGS?=-silent -o COQDOCFLAGS?=-interpolate -utf8 -COQC?="$(COQBIN)coqc" +COQC?=$(TIMER) "$(COQBIN)coqc" GALLINA?="$(COQBIN)gallina" COQDOC?="$(COQBIN)coqdoc" COQCHK?="$(COQBIN)coqchk" +COQMKTOP?="$(COQBIN)coqmktop" ################## # # @@ -72,6 +85,7 @@ COQDOCINSTALL=$(XDG_DATA_HOME)/doc/coq else COQLIBINSTALL="${COQLIB}user-contrib" COQDOCINSTALL="${DOCDIR}user-contrib" +COQTOPINSTALL="${COQLIB}toploop" endif ###################### @@ -80,40 +94,51 @@ endif # # ###################### -VFILES:=Coqprime/Zp.v\ - Coqprime/ZSum.v\ - Coqprime/ZProgression.v\ - Coqprime/ZCmisc.v\ - Coqprime/ZCAux.v\ - Coqprime/UList.v\ - Coqprime/Tactic.v\ - Coqprime/Root.v\ - Coqprime/PocklingtonCertificat.v\ - Coqprime/Pocklington.v\ - Coqprime/Pmod.v\ - Coqprime/Permutation.v\ - Coqprime/PGroup.v\ - Coqprime/NatAux.v\ - Coqprime/LucasLehmer.v\ - Coqprime/ListAux.v\ - Coqprime/Lagrange.v\ - Coqprime/Iterator.v\ - Coqprime/IGroup.v\ - Coqprime/FGroup.v\ - Coqprime/Euler.v\ +VFILES:=Coqprime/Cyclic.v\ Coqprime/EGroup.v\ - Coqprime/Cyclic.v + Coqprime/Euler.v\ + Coqprime/FGroup.v\ + Coqprime/IGroup.v\ + Coqprime/Iterator.v\ + Coqprime/Lagrange.v\ + Coqprime/ListAux.v\ + Coqprime/LucasLehmer.v\ + Coqprime/NatAux.v\ + Coqprime/PGroup.v\ + Coqprime/Permutation.v\ + Coqprime/Pmod.v\ + Coqprime/Pocklington.v\ + Coqprime/PocklingtonCertificat.v\ + Coqprime/Root.v\ + Coqprime/Tactic.v\ + Coqprime/UList.v\ + Coqprime/ZCAux.v\ + Coqprime/ZCmisc.v\ + Coqprime/ZProgression.v\ + Coqprime/ZSum.v\ + Coqprime/Zp.v +ifneq ($(filter-out archclean clean cleanall printenv,$(MAKECMDGOALS)),) +-include $(addsuffix .d,$(VFILES)) +else +ifeq ($(MAKECMDGOALS),) -include $(addsuffix .d,$(VFILES)) +endif +endif + .SECONDARY: $(addsuffix .d,$(VFILES)) -VOFILES:=$(VFILES:.v=.vo) +VO=vo +VOFILES:=$(VFILES:.v=.$(VO)) VOFILES1=$(patsubst Coqprime/%,%,$(filter Coqprime/%,$(VOFILES))) GLOBFILES:=$(VFILES:.v=.glob) -VIFILES:=$(VFILES:.v=.vi) GFILES:=$(VFILES:.v=.g) HTMLFILES:=$(VFILES:.v=.html) GHTMLFILES:=$(VFILES:.v=.g.html) +OBJFILES=$(call vo_to_obj,$(VOFILES)) +ALLNATIVEFILES=$(OBJFILES:.o=.cmi) $(OBJFILES:.o=.cmo) $(OBJFILES:.o=.cmx) $(OBJFILES:.o=.cmxs) +NATIVEFILES=$(foreach f, $(ALLNATIVEFILES), $(wildcard $f)) +NATIVEFILES1=$(patsubst Coqprime/%,%,$(filter Coqprime/%,$(NATIVEFILES))) ifeq '$(HASNATDYNLINK)' 'true' HASNATDYNLINK_OR_EMPTY := yes else @@ -128,8 +153,12 @@ endif all: $(VOFILES) -spec: $(VIFILES) +quick: $(VOFILES:.vo=.vio) +vio2vo: + $(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio2vo $(J) $(VOFILES:%.vo=%.vio) +checkproofs: + $(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio-checking $(J) $(VOFILES:%.vo=%.vio) gallina: $(GFILES) html: $(GLOBFILES) $(VFILES) @@ -160,7 +189,7 @@ beautify: $(VFILES:=.beautified) @echo 'Do not do "make clean" until you are sure that everything went well!' @echo 'If there were a problem, execute "for file in $$(find . -name \*.v.old -print); do mv $${file} $${file%.old}; done" in your shell/' -.PHONY: all opt byte archclean clean install userinstall depend html validate +.PHONY: all archclean beautify byte clean cleanall gallina gallinahtml html install install-doc install-natdynlink install-toploop opt printenv quick uninstall userinstall validate vio2vo #################### # # @@ -178,7 +207,7 @@ userinstall: +$(MAKE) USERINSTALL=true install install: - cd "Coqprime"; for i in $(VOFILES1); do \ + cd "Coqprime" && for i in $(NATIVEFILES1) $(GLOBFILES1) $(VFILES1) $(VOFILES1); do \ install -d "`dirname "$(DSTROOT)"$(COQLIBINSTALL)/Coqprime/$$i`"; \ install -m 0644 $$i "$(DSTROOT)"$(COQLIBINSTALL)/Coqprime/$$i; \ done @@ -189,12 +218,46 @@ install-doc: install -m 0644 $$i "$(DSTROOT)"$(COQDOCINSTALL)/Coqprime/$$i;\ done -clean: - rm -f $(VOFILES) $(VIFILES) $(GFILES) $(VFILES:.v=.v.d) $(VFILES:=.beautified) $(VFILES:=.old) +uninstall_me.sh: Makefile + echo '#!/bin/sh' > $@ + printf 'cd "$${DSTROOT}"$(COQLIBINSTALL)/Coqprime && rm -f $(NATIVEFILES1) $(GLOBFILES1) $(VFILES1) $(VOFILES1) && find . -type d -and -empty -delete\ncd "$${DSTROOT}"$(COQLIBINSTALL) && find "Coqprime" -maxdepth 0 -and -empty -exec rmdir -p \{\} \;\n' >> "$@" + printf 'cd "$${DSTROOT}"$(COQDOCINSTALL)/Coqprime \\\n' >> "$@" + printf '&& rm -f $(shell find "html" -maxdepth 1 -and -type f -print)\n' >> "$@" + printf 'cd "$${DSTROOT}"$(COQDOCINSTALL) && find Coqprime/html -maxdepth 0 -and -empty -exec rmdir -p \{\} \;\n' >> "$@" + chmod +x $@ + +uninstall: uninstall_me.sh + sh $< + +.merlin: + @echo 'FLG -rectypes' > .merlin + @echo "B $(COQLIB) kernel" >> .merlin + @echo "B $(COQLIB) lib" >> .merlin + @echo "B $(COQLIB) library" >> .merlin + @echo "B $(COQLIB) parsing" >> .merlin + @echo "B $(COQLIB) pretyping" >> .merlin + @echo "B $(COQLIB) interp" >> .merlin + @echo "B $(COQLIB) printing" >> .merlin + @echo "B $(COQLIB) intf" >> .merlin + @echo "B $(COQLIB) proofs" >> .merlin + @echo "B $(COQLIB) tactics" >> .merlin + @echo "B $(COQLIB) tools" >> .merlin + @echo "B $(COQLIB) toplevel" >> .merlin + @echo "B $(COQLIB) stm" >> .merlin + @echo "B $(COQLIB) grammar" >> .merlin + @echo "B $(COQLIB) config" >> .merlin + +clean:: + rm -f $(OBJFILES) $(OBJFILES:.o=.native) $(NATIVEFILES) + find . -name .coq-native -type d -empty -delete + rm -f $(VOFILES) $(VOFILES:.vo=.vio) $(GFILES) $(VFILES:.v=.v.d) $(VFILES:=.beautified) $(VFILES:=.old) rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob $(VFILES:.v=.glob) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) all-mli.tex - - rm -rf html mlihtml + - rm -rf html mlihtml uninstall_me.sh -archclean: +cleanall:: clean + rm -f $(patsubst %.v,.%.aux,$(VFILES)) + +archclean:: rm -f *.cmx *.o printenv: @@ -217,31 +280,34 @@ Makefile: _CoqProject # # ################### -%.vo %.glob: %.v +$(VOFILES): %.vo: %.v + $(COQC) $(COQDEBUG) $(COQFLAGS) $* + +$(GLOBFILES): %.glob: %.v $(COQC) $(COQDEBUG) $(COQFLAGS) $* -%.vi: %.v - $(COQC) -i $(COQDEBUG) $(COQFLAGS) $* +$(VFILES:.v=.vio): %.vio: %.v + $(COQC) -quick $(COQDEBUG) $(COQFLAGS) $* -%.g: %.v +$(GFILES): %.g: %.v $(GALLINA) $< -%.tex: %.v +$(VFILES:.v=.tex): %.tex: %.v $(COQDOC) $(COQDOCFLAGS) -latex $< -o $@ -%.html: %.v %.glob +$(HTMLFILES): %.html: %.v %.glob $(COQDOC) $(COQDOCFLAGS) -html $< -o $@ -%.g.tex: %.v +$(VFILES:.v=.g.tex): %.g.tex: %.v $(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@ -%.g.html: %.v %.glob +$(GHTMLFILES): %.g.html: %.v %.glob $(COQDOC) $(COQDOCFLAGS) -html -g $< -o $@ -%.v.d: %.v - $(COQDEP) -slash $(COQLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} ) +$(addsuffix .d,$(VFILES)): %.v.d: %.v + $(COQDEP) $(COQLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} ) -%.v.beautified: +$(addsuffix .beautified,$(VFILES)): %.v.beautified: $(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $* # WARNING |