diff options
Diffstat (limited to 'coqprime-8.4/Makefile')
| -rw-r--r-- | coqprime-8.4/Makefile | 253 |
1 files changed, 0 insertions, 253 deletions
diff --git a/coqprime-8.4/Makefile b/coqprime-8.4/Makefile deleted file mode 100644 index 8fa838a1e..000000000 --- a/coqprime-8.4/Makefile +++ /dev/null @@ -1,253 +0,0 @@ -############################################################################# -## v # The Coq Proof Assistant ## -## <O___,, # INRIA - CNRS - LIX - LRI - PPS ## -## \VV/ # ## -## // # Makefile automagically generated by coq_makefile V8.4pl6 ## -############################################################################# - -# 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; -# 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) - -########################## -# # -# 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?="$(COQBIN)coqc" -GALLINA?="$(COQBIN)gallina" -COQDOC?="$(COQBIN)coqdoc" -COQCHK?="$(COQBIN)coqchk" - -################## -# # -# 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" -endif - -###################### -# # -# Files dispatching. # -# # -###################### - -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\ - Coqprime/EGroup.v\ - Coqprime/Cyclic.v - --include $(addsuffix .d,$(VFILES)) -.SECONDARY: $(addsuffix .d,$(VFILES)) - -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) -ifeq '$(HASNATDYNLINK)' 'true' -HASNATDYNLINK_OR_EMPTY := yes -else -HASNATDYNLINK_OR_EMPTY := -endif - -####################################### -# # -# Definition of the toplevel targets. # -# # -####################################### - -all: $(VOFILES) - -spec: $(VIFILES) - -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 opt byte archclean clean install userinstall depend html validate - -#################### -# # -# Special targets. # -# # -#################### - -byte: - $(MAKE) all "OPT:=-byte" - -opt: - $(MAKE) all "OPT:=-opt" - -userinstall: - +$(MAKE) USERINSTALL=true install - -install: - cd "Coqprime"; for i in $(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 - -clean: - rm -f $(VOFILES) $(VIFILES) $(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 - -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. # -# # -################### - -%.vo %.glob: %.v - $(COQC) $(COQDEBUG) $(COQFLAGS) $* - -%.vi: %.v - $(COQC) -i $(COQDEBUG) $(COQFLAGS) $* - -%.g: %.v - $(GALLINA) $< - -%.tex: %.v - $(COQDOC) $(COQDOCFLAGS) -latex $< -o $@ - -%.html: %.v %.glob - $(COQDOC) $(COQDOCFLAGS) -html $< -o $@ - -%.g.tex: %.v - $(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@ - -%.g.html: %.v %.glob - $(COQDOC) $(COQDOCFLAGS) -html -g $< -o $@ - -%.v.d: %.v - $(COQDEP) -slash $(COQLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} ) - -%.v.beautified: - $(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $* - -# WARNING -# -# This Makefile has been automagically generated -# Edit at your own risks ! -# -# END OF WARNING - |