diff options
Diffstat (limited to 'coqprime/examples/Makefile')
-rw-r--r-- | coqprime/examples/Makefile | 230 |
1 files changed, 0 insertions, 230 deletions
diff --git a/coqprime/examples/Makefile b/coqprime/examples/Makefile deleted file mode 100644 index eff7d0d99..000000000 --- a/coqprime/examples/Makefile +++ /dev/null @@ -1,230 +0,0 @@ -############################################################################# -## 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 - |