diff options
Diffstat (limited to 'coqprime-8.5/Makefile')
| -rw-r--r-- | coqprime-8.5/Makefile | 319 |
1 files changed, 319 insertions, 0 deletions
diff --git a/coqprime-8.5/Makefile b/coqprime-8.5/Makefile new file mode 100644 index 000000000..c8e44a658 --- /dev/null +++ b/coqprime-8.5/Makefile @@ -0,0 +1,319 @@ +############################################################################# +## v # The Coq Proof Assistant ## +## <O___,, # INRIA - CNRS - LIX - LRI - PPS ## +## \VV/ # ## +## // # Makefile automagically generated by coq_makefile V8.5pl1 ## +############################################################################# + +# WARNING +# +# This Makefile has been automagically generated +# Edit at your own risks ! +# +# END OF WARNING + +# +# This Makefile was generated by the command line : +# coq_makefile -f _CoqProject -o Makefile +# + +.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. + +# Here is a hack to make $(eval $(shell works: +define donewline + + +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 + +########################## +# # +# Variables definitions. # +# # +########################## + + +OPT?= +COQDEP?="$(COQBIN)coqdep" -c +COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML) +COQCHKFLAGS?=-silent -o +COQDOCFLAGS?=-interpolate -utf8 +COQC?=$(TIMER) "$(COQBIN)coqc" +GALLINA?="$(COQBIN)gallina" +COQDOC?="$(COQBIN)coqdoc" +COQCHK?="$(COQBIN)coqchk" +COQMKTOP?="$(COQBIN)coqmktop" + +################## +# # +# Install Paths. # +# # +################## + +ifdef USERINSTALL +XDG_DATA_HOME?="$(HOME)/.local/share" +COQLIBINSTALL=$(XDG_DATA_HOME)/coq +COQDOCINSTALL=$(XDG_DATA_HOME)/doc/coq +else +COQLIBINSTALL="${COQLIB}user-contrib" +COQDOCINSTALL="${DOCDIR}user-contrib" +COQTOPINSTALL="${COQLIB}toploop" +endif + +###################### +# # +# Files dispatching. # +# # +###################### + +VFILES:=Coqprime/Cyclic.v\ + Coqprime/EGroup.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)) + +VO=vo +VOFILES:=$(VFILES:.v=.$(VO)) +VOFILES1=$(patsubst Coqprime/%,%,$(filter Coqprime/%,$(VOFILES))) +GLOBFILES:=$(VFILES:.v=.glob) +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 +HASNATDYNLINK_OR_EMPTY := +endif + +####################################### +# # +# Definition of the toplevel targets. # +# # +####################################### + +all: $(VOFILES) + +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) + - mkdir -p html + $(COQDOC) -toc $(COQDOCFLAGS) -html $(COQDOCLIBS) -d html $(VFILES) + +gallinahtml: $(GLOBFILES) $(VFILES) + - mkdir -p html + $(COQDOC) -toc $(COQDOCFLAGS) -html -g $(COQDOCLIBS) -d html $(VFILES) + +all.ps: $(VFILES) + $(COQDOC) -toc $(COQDOCFLAGS) -ps $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^` + +all-gal.ps: $(VFILES) + $(COQDOC) -toc $(COQDOCFLAGS) -ps -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^` + +all.pdf: $(VFILES) + $(COQDOC) -toc $(COQDOCFLAGS) -pdf $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^` + +all-gal.pdf: $(VFILES) + $(COQDOC) -toc $(COQDOCFLAGS) -pdf -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^` + +validate: $(VOFILES) + $(COQCHK) $(COQCHKFLAGS) $(COQLIBS) $(notdir $(^:.vo=)) + +beautify: $(VFILES:=.beautified) + for file in $^; do mv $${file%.beautified} $${file%beautified}old && mv $${file} $${file%.beautified}; done + @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 archclean beautify byte clean cleanall gallina gallinahtml html install install-doc install-natdynlink install-toploop opt printenv quick uninstall userinstall validate vio2vo + +#################### +# # +# Special targets. # +# # +#################### + +byte: + $(MAKE) all "OPT:=-byte" + +opt: + $(MAKE) all "OPT:=-opt" + +userinstall: + +$(MAKE) USERINSTALL=true install + +install: + 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 + +install-doc: + install -d "$(DSTROOT)"$(COQDOCINSTALL)/Coqprime/html + for i in html/*; do \ + install -m 0644 $$i "$(DSTROOT)"$(COQDOCINSTALL)/Coqprime/$$i;\ + done + +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 uninstall_me.sh + +cleanall:: clean + rm -f $(patsubst %.v,.%.aux,$(VFILES)) + +archclean:: + rm -f *.cmx *.o + +printenv: + @"$(COQBIN)coqtop" -config + @echo 'CAMLC = $(CAMLC)' + @echo 'CAMLOPTC = $(CAMLOPTC)' + @echo 'PP = $(PP)' + @echo 'COQFLAGS = $(COQFLAGS)' + @echo 'COQLIBINSTALL = $(COQLIBINSTALL)' + @echo 'COQDOCINSTALL = $(COQDOCINSTALL)' + +Makefile: _CoqProject + mv -f $@ $@.bak + "$(COQBIN)coq_makefile" -f $< -o $@ + + +################### +# # +# Implicit rules. # +# # +################### + +$(VOFILES): %.vo: %.v + $(COQC) $(COQDEBUG) $(COQFLAGS) $* + +$(GLOBFILES): %.glob: %.v + $(COQC) $(COQDEBUG) $(COQFLAGS) $* + +$(VFILES:.v=.vio): %.vio: %.v + $(COQC) -quick $(COQDEBUG) $(COQFLAGS) $* + +$(GFILES): %.g: %.v + $(GALLINA) $< + +$(VFILES:.v=.tex): %.tex: %.v + $(COQDOC) $(COQDOCFLAGS) -latex $< -o $@ + +$(HTMLFILES): %.html: %.v %.glob + $(COQDOC) $(COQDOCFLAGS) -html $< -o $@ + +$(VFILES:.v=.g.tex): %.g.tex: %.v + $(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@ + +$(GHTMLFILES): %.g.html: %.v %.glob + $(COQDOC) $(COQDOCFLAGS) -html -g $< -o $@ + +$(addsuffix .d,$(VFILES)): %.v.d: %.v + $(COQDEP) $(COQLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} ) + +$(addsuffix .beautified,$(VFILES)): %.v.beautified: + $(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $* + +# WARNING +# +# This Makefile has been automagically generated +# Edit at your own risks ! +# +# END OF WARNING + |