diff options
Diffstat (limited to 'coqprime/examples/Makefile')
| -rw-r--r-- | coqprime/examples/Makefile | 230 |
1 files changed, 230 insertions, 0 deletions
diff --git a/coqprime/examples/Makefile b/coqprime/examples/Makefile new file mode 100644 index 000000000..eff7d0d99 --- /dev/null +++ b/coqprime/examples/Makefile @@ -0,0 +1,230 @@ +############################################################################# +## v # The Coq Proof Assistant ## +## <O___,, # INRIA - CNRS - LIX - LRI - PPS ## +## \VV/ # ## +## // # Makefile automagically generated by coq_makefile V8.3pl1 ## +############################################################################# + +# 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 Make -o Makefile +# + +# +# This Makefile may take 3 arguments passed as environment variables: +# - COQBIN to specify the directory where Coq binaries resides; +# - CAMLBIN and CAMLP4BIN to give the path for the OCaml and Camlp4/5 binaries. +COQLIB:=$(shell $(COQBIN)coqtop -where | sed -e 's/\\/\\\\/g') +CAMLP4:="$(shell $(COQBIN)coqtop -config | awk -F = '/CAMLP4=/{print $$2}')" +ifndef CAMLP4BIN + CAMLP4BIN:=$(CAMLBIN) +endif + +CAMLP4LIB:=$(shell $(CAMLP4BIN)$(CAMLP4) -where) + +########################## +# # +# Libraries definitions. # +# # +########################## + +OCAMLLIBS:=-I .\ + -I ../Tactic\ + -I ../N\ + -I ../Z\ + -I ../PrimalityTest\ + -I ../List\ + -I ../elliptic\ + -I ../num +COQSRCLIBS:=-I $(COQLIB)/kernel -I $(COQLIB)/lib \ + -I $(COQLIB)/library -I $(COQLIB)/parsing \ + -I $(COQLIB)/pretyping -I $(COQLIB)/interp \ + -I $(COQLIB)/proofs -I $(COQLIB)/tactics \ + -I $(COQLIB)/toplevel \ + -I $(COQLIB)/plugins/cc \ + -I $(COQLIB)/plugins/dp \ + -I $(COQLIB)/plugins/extraction \ + -I $(COQLIB)/plugins/field \ + -I $(COQLIB)/plugins/firstorder \ + -I $(COQLIB)/plugins/fourier \ + -I $(COQLIB)/plugins/funind \ + -I $(COQLIB)/plugins/groebner \ + -I $(COQLIB)/plugins/interface \ + -I $(COQLIB)/plugins/micromega \ + -I $(COQLIB)/plugins/nsatz \ + -I $(COQLIB)/plugins/omega \ + -I $(COQLIB)/plugins/quote \ + -I $(COQLIB)/plugins/ring \ + -I $(COQLIB)/plugins/romega \ + -I $(COQLIB)/plugins/rtauto \ + -I $(COQLIB)/plugins/setoid_ring \ + -I $(COQLIB)/plugins/subtac \ + -I $(COQLIB)/plugins/subtac/test \ + -I $(COQLIB)/plugins/syntax \ + -I $(COQLIB)/plugins/xml +COQLIBS:=-I .\ + -I ../Tactic\ + -I ../N\ + -I ../Z\ + -I ../PrimalityTest\ + -I ../List\ + -I ../elliptic\ + -I ../num +COQDOCLIBS:= + +########################## +# # +# Variables definitions. # +# # +########################## + +ZFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB) +OPT:= +COQFLAGS:=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML) -verbose +ifdef CAMLBIN + COQMKTOPFLAGS:=-camlbin $(CAMLBIN) -camlp4bin $(CAMLP4BIN) +endif +COQC:=$(COQBIN)coqc +COQDEP:=$(COQBIN)coqdep -c +GALLINA:=$(COQBIN)gallina +COQDOC:=$(COQBIN)coqdoc +COQMKTOP:=$(COQBIN)coqmktop +CAMLLIB:=$(shell $(CAMLBIN)ocamlc.opt -where) +CAMLC:=$(CAMLBIN)ocamlc.opt -c -rectypes +CAMLOPTC:=$(CAMLBIN)ocamlopt.opt -c -rectypes +CAMLLINK:=$(CAMLBIN)ocamlc.opt -rectypes +CAMLOPTLINK:=$(CAMLBIN)ocamlopt.opt -rectypes +GRAMMARS:=grammar.cma +CAMLP4EXTEND:=pa_extend.cmo pa_macro.cmo q_MLast.cmo +CAMLP4OPTIONS:= +PP:=-pp "$(CAMLP4BIN)$(CAMLP4)o -I $(CAMLLIB) -I . $(COQSRCLIBS) $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl" + +################################### +# # +# Definition of the "all" target. # +# # +################################### + +VFILES:=BasePrimes.v\ + PocklingtonRefl.v\ + TestLucas.v\ + prime216656403549020227250327256032933021325435259861468456540459488823774358486649614451547405419273433458932168893949521787.v\ + prime329719147332060395689499.v\ + russell1.v\ + russell2.v +VOFILES:=$(VFILES:.v=.vo) +VOFILES0:=$(filter-out ,$(VOFILES)) +GLOBFILES:=$(VFILES:.v=.glob) +VIFILES:=$(VFILES:.v=.vi) +GFILES:=$(VFILES:.v=.g) +HTMLFILES:=$(VFILES:.v=.html) +GHTMLFILES:=$(VFILES:.v=.g.html) + +all: $(VOFILES) +spec: $(VIFILES) + +gallina: $(GFILES) + +html: $(GLOBFILES) $(VFILES) + - mkdir -p html + $(COQDOC) -toc -html $(COQDOCLIBS) -d html $(VFILES) + +gallinahtml: $(GLOBFILES) $(VFILES) + - mkdir -p html + $(COQDOC) -toc -html -g $(COQDOCLIBS) -d html $(VFILES) + +all.ps: $(VFILES) + $(COQDOC) -toc -ps $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)` + +all-gal.ps: $(VFILES) + $(COQDOC) -toc -ps -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)` + +all.pdf: $(VFILES) + $(COQDOC) -toc -pdf $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)` + +all-gal.pdf: $(VFILES) + $(COQDOC) -toc -pdf -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)` + + + +#################### +# # +# Special targets. # +# # +#################### + +.PHONY: all opt byte archclean clean install depend html + +%.vo %.glob: %.v + $(COQC) $(COQDEBUG) $(COQFLAGS) $* + +%.vi: %.v + $(COQC) -i $(COQDEBUG) $(COQFLAGS) $* + +%.g: %.v + $(GALLINA) $< + +%.tex: %.v + $(COQDOC) -latex $< -o $@ + +%.html: %.v %.glob + $(COQDOC) -html $< -o $@ + +%.g.tex: %.v + $(COQDOC) -latex -g $< -o $@ + +%.g.html: %.v %.glob + $(COQDOC) -html -g $< -o $@ + +%.v.d: %.v + $(COQDEP) -slash $(COQLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} ) + +byte: + $(MAKE) all "OPT:=-byte" + +opt: + $(MAKE) all "OPT:=-opt" + +install: + mkdir -p $(COQLIB)/user-contrib + (for i in $(VOFILES0); do \ + install -d `dirname $(COQLIB)/user-contrib/$(INSTALLDEFAULTROOT)/$$i`; \ + install $$i $(COQLIB)/user-contrib/$(INSTALLDEFAULTROOT)/$$i; \ + done) + +clean: + rm -f $(CMOFILES) $(CMIFILES) $(CMXFILES) $(CMXSFILES) $(OFILES) $(VOFILES) $(VIFILES) $(GFILES) $(MLFILES:.ml=.cmo) $(MLFILES:.ml=.cmx) *~ + rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob $(VFILES:.v=.glob) $(HTMLFILES) $(GHTMLFILES) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) $(VFILES:.v=.v.d) + - rm -rf html + +archclean: + rm -f *.cmx *.o + + +printenv: + @echo CAMLC = $(CAMLC) + @echo CAMLOPTC = $(CAMLOPTC) + @echo CAMLP4LIB = $(CAMLP4LIB) + +Makefile: Make + mv -f Makefile Makefile.bak + $(COQBIN)coq_makefile -f Make -o Makefile + + +-include $(VFILES:.v=.v.d) +.SECONDARY: $(VFILES:.v=.v.d) + +# WARNING +# +# This Makefile has been automagically generated +# Edit at your own risks ! +# +# END OF WARNING + |