Tue Aug 16 14:48:12 GMT 2011

Makefile

############################################################################# ## v # The Coq Proof Assistant ## ## <O___,, # INRIA - CNRS - LIX - LRI - PPS ## ## \VV/ # ## ## // # Makefile automagically generated by coq_makefile V8.3pl2 ## ############################################################################# # 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 -no-install Symbols.v Preface.v Basics.v Lists.v Poly.v Gen.v Prop.v Logic.v Rel.v SfLib.v Imp.v ImpParser.v Equiv.v ImpList.v Hoare.v HoareAsLogic.v Smallstep.v Types.v Stlc.v Typechecking.v MoreStlc.v Records.v References.v Subtyping.v RecordSub.v Norm.v UseTactics.v UseAuto.v LibTactics.v PE.v Postscript.v # # # 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 . 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 . COQDOCLIBS:= ########################## # # # Variables definitions. # # # ########################## ZFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB) OPT:= COQFLAGS:=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML) 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:=Symbols.v\ Preface.v\ Basics.v\ Lists.v\ Poly.v\ Gen.v\ Prop.v\ Logic.v\ Rel.v\ SfLib.v\ Imp.v\ ImpParser.v\ Equiv.v\ ImpList.v\ Hoare.v\ HoareAsLogic.v\ Smallstep.v\ Types.v\ Stlc.v\ Typechecking.v\ MoreStlc.v\ Records.v\ References.v\ Subtyping.v\ RecordSub.v\ Norm.v\ UseTactics.v\ UseAuto.v\ LibTactics.v\ PE.v\ Postscript.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" 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) -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


(google search) (amazon search)
1 2 3 second