diff options
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 1605 |
1 files changed, 1605 insertions, 0 deletions
diff --git a/Makefile b/Makefile new file mode 100644 index 00000000..af8a8c07 --- /dev/null +++ b/Makefile @@ -0,0 +1,1605 @@ +######################################################################## +# v # The Coq Proof Assistant / The Coq Development Team # +# <O___,, # CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud # +# \VV/ ############################################################## +# // # This file is distributed under the terms of the # +# # GNU Lesser General Public License Version 2.1 # +######################################################################## + +# $Id: Makefile,v 1.459.2.10 2004/07/19 09:37:31 herbelin Exp $ + + +# Makefile for Coq +# +# To be used with GNU Make. +# +# This is the only Makefile. You won't find Makefiles in sub-directories +# and this is done on purpose. If you are not yet convinced of the advantages +# of a single Makefile, please read +# http://www.pcug.org.au/~millerp/rmch/recu-make-cons-harm.html +# before complaining. +# +# When you are working in a subdir, you can compile without moving to the +# upper directory using "make -C ..", and the output is still understood +# by Emacs' next-error. +########################################################################### + +include config/Makefile + +noargument: + @echo "Please use either" + @echo " ./configure" + @echo " make world" + @echo " make install" + @echo " make clean" + @echo "or make archclean" + @echo + @echo "For make to be verbose, add VERBOSE=1" + +# build and install the three subsystems: coq, coqide, pcoq +world: coq coqide pcoq +world8: coq8 coqide pcoq +world7: coq7 coqide pcoq + +install: install-coq install-coqide install-pcoq +install8: install-coq8 install-coqide install-pcoq +install7: install-coq7 install-coqide install-pcoq +#install-manpages: install-coq-manpages install-pcoq-manpages + +########################################################################### +# Compilation options +########################################################################### + +# The SHOW and HIDE variables control whether make will echo complete commands +# or only abbreviated versions. +# Quiet mode is ON by default except if VERBOSE=1 option is given to make + +ifeq ($(VERBOSE),1) + SHOW = @true "" + HIDE = +else + SHOW = @echo "" + HIDE = @ +endif + +LOCALINCLUDES=-I config -I tools -I tools/coqdoc \ + -I scripts -I lib -I kernel -I library \ + -I proofs -I tactics -I pretyping \ + -I interp -I toplevel -I parsing -I ide/utils \ + -I ide -I translate \ + -I contrib/omega -I contrib/romega \ + -I contrib/ring -I contrib/xml \ + -I contrib/extraction \ + -I contrib/interface -I contrib/fourier \ + -I contrib/jprover -I contrib/cc \ + -I contrib/funind -I contrib/first-order \ + -I contrib/field + +MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB) + +BYTEFLAGS=$(MLINCLUDES) $(CAMLDEBUG) +OPTFLAGS=$(MLINCLUDES) $(CAMLTIMEPROF) +OCAMLDEP=ocamldep +DEPFLAGS=$(LOCALINCLUDES) + +OCAMLC_P4O=$(OCAMLC) -pp $(CAMLP4O) $(BYTEFLAGS) +OCAMLOPT_P4O=$(OCAMLOPT) -pp $(CAMLP4O) $(OPTFLAGS) +CAMLP4EXTENDFLAGS=-I . pa_extend.cmo pa_extend_m.cmo pa_ifdef.cmo q_MLast.cmo +CAMLP4DEPS=sed -n -e 's|^(\*.*camlp4deps: "\(.*\)".*\*)$$|\1|p' + +COQINCLUDES= # coqtop includes itself the needed paths +GLOB= # is "-dump-glob file" when making the doc +COQ_XML= # is "-xml" when building XML library +COQOPTS=$(GLOB) $(COQ_XML) +TRANSLATE=-translate -strict-implicit + +BOOTCOQTOP=$(BESTCOQTOP) -boot $(COQOPTS) + +########################################################################### +# Objects files +########################################################################### + +CLIBS=unix.cma + +CAMLP4OBJS=gramlib.cma + +CONFIG=\ + config/coq_config.cmo + +LIBREP=\ + lib/pp_control.cmo lib/pp.cmo lib/compat.cmo lib/util.cmo lib/bignat.cmo \ + lib/hashcons.cmo lib/dyn.cmo lib/system.cmo lib/options.cmo \ + lib/bstack.cmo lib/edit.cmo lib/gset.cmo lib/gmap.cmo \ + lib/tlm.cmo lib/gmapl.cmo lib/profile.cmo lib/explore.cmo \ + lib/predicate.cmo lib/rtree.cmo lib/heap.cmo +# Rem: Cygwin already uses variable LIB + +KERNEL=\ + kernel/names.cmo kernel/univ.cmo \ + kernel/esubst.cmo kernel/term.cmo kernel/sign.cmo \ + kernel/declarations.cmo kernel/environ.cmo kernel/closure.cmo \ + kernel/conv_oracle.cmo kernel/reduction.cmo kernel/entries.cmo \ + kernel/modops.cmo \ + kernel/type_errors.cmo kernel/inductive.cmo kernel/typeops.cmo \ + kernel/indtypes.cmo kernel/cooking.cmo kernel/term_typing.cmo \ + kernel/subtyping.cmo kernel/mod_typing.cmo kernel/safe_typing.cmo + +LIBRARY=\ + library/nameops.cmo library/libnames.cmo library/libobject.cmo \ + library/summary.cmo library/nametab.cmo library/global.cmo library/lib.cmo \ + library/declaremods.cmo library/library.cmo library/states.cmo \ + library/decl_kinds.cmo library/dischargedhypsmap.cmo library/goptions.cmo + +PRETYPING=\ + pretyping/termops.cmo pretyping/evd.cmo pretyping/instantiate.cmo \ + pretyping/reductionops.cmo pretyping/inductiveops.cmo \ + pretyping/rawterm.cmo pretyping/pattern.cmo \ + pretyping/detyping.cmo pretyping/retyping.cmo \ + pretyping/cbv.cmo pretyping/tacred.cmo \ + pretyping/pretype_errors.cmo pretyping/typing.cmo \ + pretyping/classops.cmo pretyping/recordops.cmo pretyping/indrec.cmo \ + pretyping/evarutil.cmo pretyping/evarconv.cmo \ + pretyping/coercion.cmo pretyping/cases.cmo pretyping/pretyping.cmo \ + pretyping/matching.cmo + +INTERP=\ + parsing/lexer.cmo interp/topconstr.cmo interp/ppextend.cmo interp/symbols.cmo \ + interp/genarg.cmo interp/syntax_def.cmo interp/reserve.cmo \ + library/impargs.cmo interp/constrintern.cmo \ + interp/modintern.cmo interp/constrextern.cmo interp/coqlib.cmo \ + library/declare.cmo + +PARSING=\ + parsing/coqast.cmo parsing/ast.cmo \ + parsing/termast.cmo parsing/extend.cmo parsing/esyntax.cmo \ + parsing/pcoq.cmo parsing/egrammar.cmo \ + parsing/ppconstr.cmo translate/ppconstrnew.cmo parsing/printer.cmo \ + parsing/pptactic.cmo translate/pptacticnew.cmo \ + parsing/printmod.cmo parsing/prettyp.cmo parsing/search.cmo + +HIGHPARSING=\ + parsing/g_prim.cmo parsing/g_proofs.cmo parsing/g_basevernac.cmo \ + parsing/g_vernac.cmo parsing/g_tactic.cmo \ + parsing/g_ltac.cmo parsing/g_constr.cmo parsing/g_cases.cmo \ + parsing/g_module.cmo \ + parsing/g_natsyntax.cmo parsing/g_zsyntax.cmo parsing/g_rsyntax.cmo + +HIGHPARSINGNEW=\ + parsing/g_primnew.cmo parsing/g_constrnew.cmo parsing/g_tacticnew.cmo \ + parsing/g_ltacnew.cmo parsing/g_vernacnew.cmo parsing/g_proofsnew.cmo + +ARITHSYNTAX=\ + parsing/g_natsyntax.cmo parsing/g_zsyntax.cmo parsing/g_rsyntax.cmo + +PROOFS=\ + proofs/tacexpr.cmo proofs/proof_type.cmo \ + proofs/proof_trees.cmo proofs/logic.cmo \ + proofs/refiner.cmo proofs/evar_refiner.cmo proofs/tacmach.cmo \ + proofs/clenv.cmo proofs/pfedit.cmo proofs/tactic_debug.cmo + +TACTICS=\ + tactics/dn.cmo tactics/termdn.cmo tactics/btermdn.cmo \ + tactics/nbtermdn.cmo tactics/tacticals.cmo \ + tactics/hipattern.cmo tactics/tactics.cmo \ + tactics/hiddentac.cmo tactics/elim.cmo \ + tactics/dhyp.cmo tactics/auto.cmo \ + tactics/setoid_replace.cmo tactics/equality.cmo \ + tactics/contradiction.cmo tactics/inv.cmo tactics/leminv.cmo \ + tactics/tacinterp.cmo \ + +TOPLEVEL=\ + toplevel/himsg.cmo toplevel/cerrors.cmo toplevel/class.cmo \ + toplevel/vernacexpr.cmo toplevel/metasyntax.cmo \ + toplevel/command.cmo \ + toplevel/record.cmo toplevel/recordobj.cmo \ + toplevel/discharge.cmo translate/ppvernacnew.cmo \ + toplevel/vernacinterp.cmo toplevel/mltop.cmo \ + toplevel/vernacentries.cmo toplevel/vernac.cmo \ + toplevel/line_oriented_parser.cmo toplevel/protectedtoplevel.cmo \ + toplevel/toplevel.cmo toplevel/usage.cmo \ + toplevel/coqinit.cmo toplevel/coqtop.cmo + +HIGHTACTICS=\ + tactics/autorewrite.cmo tactics/refine.cmo \ + tactics/extraargs.cmo tactics/extratactics.cmo tactics/eauto.cmo + +SPECTAC= tactics/tauto.ml4 tactics/eqdecide.ml4 +USERTAC = $(SPECTAC) +ML4FILES += $(USERTAC) tactics/extraargs.ml4 tactics/extratactics.ml4 \ + tactics/eauto.ml4 + +USERTACCMO=$(USERTAC:.ml4=.cmo) +USERTACCMX=$(USERTAC:.ml4=.cmx) + +ML4FILES +=\ + contrib/omega/g_omega.ml4 \ + contrib/romega/g_romega.ml4 contrib/ring/g_quote.ml4 \ + contrib/ring/g_ring.ml4 \ + contrib/field/field.ml4 contrib/fourier/g_fourier.ml4 \ + contrib/extraction/g_extraction.ml4 contrib/xml/xmlentries.ml4 + +OMEGACMO=\ + contrib/omega/omega.cmo contrib/omega/coq_omega.cmo \ + contrib/omega/g_omega.cmo + +ROMEGACMO=\ + contrib/romega/omega2.cmo contrib/romega/const_omega.cmo \ + contrib/romega/refl_omega.cmo contrib/romega/g_romega.cmo + +RINGCMO=\ + contrib/ring/quote.cmo contrib/ring/g_quote.cmo \ + contrib/ring/ring.cmo contrib/ring/g_ring.cmo + +FIELDCMO=\ + contrib/field/field.cmo + +XMLCMO=\ + contrib/xml/unshare.cmo contrib/xml/xml.cmo contrib/xml/acic.cmo \ + contrib/xml/doubleTypeInference.cmo \ + contrib/xml/cic2acic.cmo contrib/xml/acic2Xml.cmo \ + contrib/xml/proof2aproof.cmo \ + contrib/xml/xmlcommand.cmo contrib/xml/proofTree2Xml.cmo \ + contrib/xml/xmlentries.cmo + +FOURIERCMO=\ + contrib/fourier/fourier.cmo contrib/fourier/fourierR.cmo \ + contrib/fourier/g_fourier.cmo + +EXTRACTIONCMO=\ + contrib/extraction/table.cmo\ + contrib/extraction/mlutil.cmo\ + contrib/extraction/modutil.cmo \ + contrib/extraction/ocaml.cmo \ + contrib/extraction/haskell.cmo \ + contrib/extraction/scheme.cmo \ + contrib/extraction/extraction.cmo \ + contrib/extraction/common.cmo \ + contrib/extraction/extract_env.cmo \ + contrib/extraction/g_extraction.cmo + +JPROVERCMO=\ + contrib/jprover/opname.cmo \ + contrib/jprover/jterm.cmo contrib/jprover/jlogic.cmo \ + contrib/jprover/jtunify.cmo contrib/jprover/jall.cmo \ + contrib/jprover/jprover.cmo + +FUNINDCMO=\ + contrib/funind/tacinvutils.cmo contrib/funind/tacinv.cmo + +FOCMO=\ + contrib/first-order/formula.cmo contrib/first-order/unify.cmo \ + contrib/first-order/sequent.cmo contrib/first-order/rules.cmo \ + contrib/first-order/instances.cmo contrib/first-order/ground.cmo \ + contrib/first-order/g_ground.cmo + +CCCMO=contrib/cc/ccalgo.cmo contrib/cc/ccproof.cmo contrib/cc/cctac.cmo + +ML4FILES += contrib/jprover/jprover.ml4 contrib/cc/cctac.ml4 \ + contrib/funind/tacinv.ml4 contrib/first-order/g_ground.ml4 + +CONTRIB=$(OMEGACMO) $(ROMEGACMO) $(RINGCMO) $(FIELDCMO) \ + $(FOURIERCMO) $(EXTRACTIONCMO) $(JPROVERCMO) $(XMLCMO) \ + $(CCCMO) $(FUNINDCMO) $(FOCMO) + +CMA=$(CLIBS) $(CAMLP4OBJS) +CMXA=$(CMA:.cma=.cmxa) + +# Beware that highparsingnew.cma should appear before hightactics.cma +# respecting this order is useful for developers that want to load or link +# the libraries directly +CMO=$(CONFIG) lib/lib.cma kernel/kernel.cma library/library.cma \ + pretyping/pretyping.cma interp/interp.cma parsing/parsing.cma \ + proofs/proofs.cma tactics/tactics.cma toplevel/toplevel.cma \ + parsing/highparsing.cma parsing/highparsingnew.cma tactics/hightactics.cma \ + contrib/contrib.cma +CMOCMXA=$(CMO:.cma=.cmxa) +CMX=$(CMOCMXA:.cmo=.cmx) + +########################################################################### +# Main targets (coqmktop, coqtop.opt, coqtop.byte) +########################################################################### + +COQMKTOP=bin/coqmktop$(EXE) +COQC=bin/coqc$(EXE) +COQTOPBYTE=bin/coqtop.byte$(EXE) +COQTOPOPT=bin/coqtop.opt$(EXE) +BESTCOQTOP=bin/coqtop.$(BEST)$(EXE) +COQTOP=bin/coqtop$(EXE) + +COQBINARIES= $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(BESTCOQTOP) $(COQTOP) + +coqbinaries:: ${COQBINARIES} + +coq: coqlib tools coqbinaries coqlib7 +coq8: coqlib tools coqbinaries +coq7: coqlib7 tools coqbinaries + +coqlib:: newtheories newcontrib + +coqlib7: theories7 contrib7 + +coqlight: theories-light tools coqbinaries + +states7:: states7/initial.coq + +states:: states/initial.coq + +$(COQTOPOPT): $(COQMKTOP) $(CMX) $(USERTACCMX) + $(SHOW)'COQMKTOP -o $@' + $(HIDE)$(COQMKTOP) -opt $(OPTFLAGS) -o $@ + $(STRIP) $@ + +$(COQTOPBYTE): $(COQMKTOP) $(CMO) $(USERTACCMO) + $(SHOW)'COQMKTOP -o $@' + $(HIDE)$(COQMKTOP) -top $(LOCALINCLUDES) $(CAMLDEBUG) -o $@ + +$(COQTOP): + cd bin; ln -sf coqtop.$(BEST)$(EXE) coqtop$(EXE) + +# coqmktop + +COQMKTOPCMO=$(CONFIG) scripts/tolink.cmo scripts/coqmktop.cmo + +$(COQMKTOP): $(COQMKTOPCMO) + $(SHOW)'OCAMLC -o $@' + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ -custom str.cma unix.cma \ + $(COQMKTOPCMO) $(OSDEPLIBS) + +scripts/tolink.ml: Makefile + $(SHOW)"ECHO... >" $@ + $(HIDE)echo "let lib = \""$(LIBREP)"\"" > $@ + $(HIDE)echo "let kernel = \""$(KERNEL)"\"" >> $@ + $(HIDE)echo "let library = \""$(LIBRARY)"\"" >> $@ + $(HIDE)echo "let pretyping = \""$(PRETYPING)"\"" >> $@ + $(HIDE)echo "let proofs = \""$(PROOFS)"\"" >> $@ + $(HIDE)echo "let tactics = \""$(TACTICS)"\"" >> $@ + $(HIDE)echo "let interp = \""$(INTERP)"\"" >> $@ + $(HIDE)echo "let parsing = \""$(PARSING)"\"" >> $@ + $(HIDE)echo "let toplevel = \""$(TOPLEVEL)"\"" >> $@ + $(HIDE)echo "let highparsing = \""$(HIGHPARSING)"\"" >> $@ + $(HIDE)echo "let highparsingnew = \""$(HIGHPARSINGNEW)"\"" >> $@ + $(HIDE)echo "let hightactics = \""$(HIGHTACTICS)" "$(USERTACCMO)"\"" >> $@ + $(HIDE)echo "let contrib = \""$(CONTRIB)"\"" >> $@ + $(HIDE)echo "let ide = \""$(COQIDECMO)"\"" >> $@ + +beforedepend:: scripts/tolink.ml + +# coqc + +COQCCMO=$(CONFIG) toplevel/usage.cmo scripts/coqc.cmo + +$(COQC): $(COQCCMO) $(COQTOPBYTE) $(BESTCOQTOP) + $(SHOW)'OCAMLC -o $@' + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ -custom unix.cma $(COQCCMO) $(OSDEPLIBS) + +clean:: + rm -f scripts/tolink.ml + +archclean:: + rm -f $(COQTOPBYTE) $(COQTOPOPT) $(BESTCOQTOP) $(COQC) $(COQMKTOP) + rm -f $(COQTOP) + +# we provide targets for each subdirectory + +lib: $(LIBREP) +kernel: $(KERNEL) +library: $(LIBRARY) +proofs: $(PROOFS) +tactics: $(TACTICS) +interp: $(INTERP) +parsing: $(PARSING) +pretyping: $(PRETYPING) +highparsing: $(HIGHPARSING) +highparsingnew: $(HIGHPARSINGNEW) +toplevel: $(TOPLEVEL) +hightactics: $(HIGHTACTICS) + +# target for libraries + +lib/lib.cma: $(LIBREP) + $(SHOW)'OCAMLC -a -o $@' + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $(LIBREP) + +lib/lib.cmxa: $(LIBREP:.cmo=.cmx) + $(SHOW)'OCAMLOPT -a -o $@' + $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(LIBREP:.cmo=.cmx) + +kernel/kernel.cma: $(KERNEL) + $(SHOW)'OCAMLC -a -o $@' + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $(KERNEL) + +kernel/kernel.cmxa: $(KERNEL:.cmo=.cmx) + $(SHOW)'OCAMLOPT -a -o $@' + $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(KERNEL:.cmo=.cmx) + +library/library.cma: $(LIBRARY) + $(SHOW)'OCAMLC -a -o $@' + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $(LIBRARY) + +library/library.cmxa: $(LIBRARY:.cmo=.cmx) + $(SHOW)'OCAMLOPT -a -o $@' + $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(LIBRARY:.cmo=.cmx) + +pretyping/pretyping.cma: $(PRETYPING) + $(SHOW)'OCAMLC -a -o $@' + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $(PRETYPING) + +pretyping/pretyping.cmxa: $(PRETYPING:.cmo=.cmx) + $(SHOW)'OCAMLOPT -a -o $@' + $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(PRETYPING:.cmo=.cmx) + +interp/interp.cma: $(INTERP) + $(SHOW)'OCAMLC -a -o $@' + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $(INTERP) + +interp/interp.cmxa: $(INTERP:.cmo=.cmx) + $(SHOW)'OCAMLOPT -a -o $@' + $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(INTERP:.cmo=.cmx) + +parsing/parsing.cma: $(PARSING) + $(SHOW)'OCAMLC -a -o $@' + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $(PARSING) + +parsing/parsing.cmxa: $(PARSING:.cmo=.cmx) + $(SHOW)'OCAMLOPT -a -o $@' + $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(PARSING:.cmo=.cmx) + +proofs/proofs.cma: $(PROOFS) + $(SHOW)'OCAMLC -a -o $@' + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $(PROOFS) + +proofs/proofs.cmxa: $(PROOFS:.cmo=.cmx) + $(SHOW)'OCAMLOPT -a -o $@' + $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(PROOFS:.cmo=.cmx) + +tactics/tactics.cma: $(TACTICS) + $(SHOW)'OCAMLC -a -o $@' + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $(TACTICS) + +tactics/tactics.cmxa: $(TACTICS:.cmo=.cmx) + $(SHOW)'OCAMLOPT -a -o $@' + $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(TACTICS:.cmo=.cmx) + +toplevel/toplevel.cma: $(TOPLEVEL) + $(SHOW)'OCAMLC -a -o $@' + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $(TOPLEVEL) + +toplevel/toplevel.cmxa: $(TOPLEVEL:.cmo=.cmx) + $(SHOW)'OCAMLOPT -a -o $@' + $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(TOPLEVEL:.cmo=.cmx) + +parsing/highparsing.cma: $(HIGHPARSING) + $(SHOW)'OCAMLC -a -o $@' + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $(HIGHPARSING) + +parsing/highparsing.cmxa: $(HIGHPARSING:.cmo=.cmx) + $(SHOW)'OCAMLOPT -a -o $@' + $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(HIGHPARSING:.cmo=.cmx) + +tactics/hightactics.cma: $(HIGHTACTICS) $(USERTACCMO) + $(SHOW)'OCAMLC -a -o $@' + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $(HIGHTACTICS) $(USERTACCMO) + +tactics/hightactics.cmxa: $(HIGHTACTICS:.cmo=.cmx) $(USERTACCMO:.cmo=.cmx) + $(SHOW)'OCAMLOPT -a -o $@' + $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(HIGHTACTICS:.cmo=.cmx) \ + $(USERTACCMO:.cmo=.cmx) + +contrib/contrib.cma: $(CONTRIB) + $(SHOW)'OCAMLC -a -o $@' + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $(CONTRIB) + +contrib/contrib.cmxa: $(CONTRIB:.cmo=.cmx) + $(SHOW)'OCAMLOPT -a -o $@' + $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(CONTRIB:.cmo=.cmx) + +parsing/highparsingnew.cma: $(HIGHPARSINGNEW) + $(SHOW)'OCAMLC -a -o $@' + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $(HIGHPARSINGNEW) + +parsing/highparsingnew.cmxa: $(HIGHPARSINGNEW:.cmo=.cmx) + $(SHOW)'OCAMLOPT -a -o $@' + $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(HIGHPARSINGNEW:.cmo=.cmx) + +########################################################################### +# CoqIde special targets +########################################################################### + +# target to build CoqIde +coqide:: coqide-files coqide-binaries states + +COQIDEBYTE=bin/coqide.byte$(EXE) +COQIDEOPT=bin/coqide.opt$(EXE) +COQIDE=bin/coqide$(EXE) + +COQIDECMO=ide/utils/okey.cmo ide/utils/uoptions.cmo \ + ide/utils/configwin_keys.cmo ide/utils/configwin_types.cmo \ + ide/utils/configwin_messages.cmo ide/utils/configwin_ihm.cmo \ + ide/utils/configwin.cmo \ + ide/utils/editable_cells.cmo ide/config_parser.cmo \ + ide/config_lexer.cmo ide/utf8_convert.cmo ide/preferences.cmo \ + ide/ideutils.cmo ide/blaster_window.cmo ide/undo.cmo \ + ide/find_phrase.cmo \ + ide/highlight.cmo ide/coq.cmo ide/coq_commands.cmo \ + ide/coq_tactics.cmo ide/command_windows.cmo ide/coqide.cmo + +COQIDECMX=$(COQIDECMO:.cmo=.cmx) +COQIDEFLAGS=-thread -I +lablgtk2 +beforedepend:: ide/config_lexer.ml ide/find_phrase.ml ide/highlight.ml +beforedepend:: ide/config_parser.mli ide/config_parser.ml +beforedepend:: ide/utf8_convert.ml + +COQIDEVO=ide/utf8.vo + +$(COQIDEVO): states/initial.coq + $(BOOTCOQTOP) -compile $* + +IDEFILES=$(COQIDEVO) ide/utf8.v ide/coq.png ide/.coqide-gtk2rc + +coqide-binaries: coqide-$(HASCOQIDE) +coqide-no: +coqide-byte: $(COQIDEBYTE) $(COQIDE) +coqide-opt: $(COQIDEBYTE) $(COQIDEOPT) $(COQIDE) +coqide-files: $(IDEFILES) + +clean-ide: + rm -f $(COQIDEVO) $(COQIDECMO) $(COQIDECMX) $(COQIDECMO:.cmo=.cmi) $(COQIDEBYTE) $(COQIDEOPT) $(COQIDE) + rm -f ide/extract_index.ml ide/find_phrase.ml ide/highlight.ml + rm -f ide/config_lexer.ml ide/config_parser.mli ide/config_parser.ml + rm -f ide/utf8_convert.ml + +$(COQIDEOPT): $(COQMKTOP) $(CMX) $(USERTACCMX) ide/ide.cmxa + $(SHOW)'COQMKTOP -o $@' + $(HIDE)$(COQMKTOP) -ide -opt $(OPTFLAGS) -o $@ + $(STRIP) $@ + +$(COQIDEBYTE): $(COQMKTOP) $(CMO) $(USERTACCMO) ide/ide.cma + $(SHOW)'COQMKTOP -o $@' + $(HIDE)$(COQMKTOP) -g -ide -top $(LOCALINCLUDES) $(CAMLDEBUG) -o $@ + +$(COQIDE): + cd bin; ln -sf coqide.$(HASCOQIDE)$(EXE) coqide$(EXE) + +ide/%.cmo: ide/%.ml + $(SHOW)'OCAMLC $<' + $(HIDE)$(OCAMLC) -g $(COQIDEFLAGS) $(BYTEFLAGS) -c $< + +ide/%.cmi: ide/%.mli + $(SHOW)'OCAMLC $<' + $(HIDE)$(OCAMLC) -g $(COQIDEFLAGS) $(BYTEFLAGS) -c $< + +ide/%.cmx: ide/%.ml + $(SHOW)'OCAMLOPT $<' + $(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -c $< + +ide/utils/%.cmo: ide/%.ml + $(SHOW)'OCAMLC $<' + $(HIDE)$(OCAMLC) -g $(COQIDEFLAGS) $(BYTEFLAGS) -c $< + +ide/utils/%.cmi: ide/%.mli + $(SHOW)'OCAMLC $<' + $(HIDE)$(OCAMLC) -g $(COQIDEFLAGS) $(BYTEFLAGS) -c $< + +ide/utils/%.cmx: ide/%.ml + $(SHOW)'OCAMLOPT $<' + $(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -c $< + +clean:: + rm -f ide/extract_index.ml ide/find_phrase.ml ide/highlight.ml + rm -f ide/config_lexer.ml ide/config_parser.mli ide/config_parser.ml + rm -f ide/utf8_convert.ml + rm -f $(COQIDEVO) $(COQIDECMO) $(COQIDECMX) $(COQIDECMO:.cmo=.cmi) + rm -f $(COQIDEBYTE) $(COQIDEOPT) $(COQIDE) + +ide/ide.cma: $(COQIDECMO) + $(SHOW)'OCAMLC -a -o $@' + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $(COQIDECMO) + +ide/ide.cmxa: $(COQIDECMO:.cmo=.cmx) + $(SHOW)'OCAMLOPT -a -o $@' + $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(COQIDECMO:.cmo=.cmx) + +# install targets + +FULLIDELIB=$(FULLCOQLIB)/ide + +install-coqide:: install-ide-$(HASCOQIDE) install-ide-files install-ide-info + +install-ide-no: + +install-ide-byte: + $(MKDIR) $(FULLBINDIR) + cp $(COQIDEBYTE) $(FULLBINDIR) + cd $(FULLBINDIR); ln -sf coqide.byte$(EXE) coqide$(EXE) + +install-ide-opt: + $(MKDIR) $(FULLBINDIR) + cp $(COQIDEBYTE) $(COQIDEOPT) $(FULLBINDIR) + cd $(FULLBINDIR); ln -sf coqide.opt$(EXE) coqide$(EXE) + +install-ide-files: + $(MKDIR) $(FULLIDELIB) + cp $(IDEFILES) $(FULLIDELIB) + +install-ide-info: + $(MKDIR) $(FULLIDELIB) + cp ide/FAQ $(FULLIDELIB) + +########################################################################### +# Pcoq: special binaries for debugging (coq-interface, parser) +########################################################################### + +# target to build Pcoq +pcoq: pcoq-binaries pcoq-files + +INTERFACE=\ + contrib/interface/vtp.cmo contrib/interface/xlate.cmo \ + contrib/interface/paths.cmo contrib/interface/translate.cmo \ + contrib/interface/pbp.cmo \ + contrib/interface/dad.cmo \ + contrib/interface/history.cmo \ + contrib/interface/name_to_ast.cmo contrib/interface/debug_tac.cmo \ + contrib/interface/showproof_ct.cmo contrib/interface/showproof.cmo \ + contrib/interface/blast.cmo contrib/interface/centaur.cmo +INTERFACECMX=$(INTERFACE:.cmo=.cmx) + +ML4FILES += contrib/interface/debug_tac.ml4 contrib/interface/centaur.ml4 + +PARSERREQUIRES=$(CMO) # Solution de facilité... +PARSERREQUIRESCMX=$(CMX) + +ifeq ($(BEST),opt) + COQINTERFACE=bin/coq-interface$(EXE) bin/coq-interface.opt$(EXE) bin/parser$(EXE) bin/parser.opt$(EXE) +else + COQINTERFACE=bin/coq-interface$(EXE) bin/parser$(EXE) +endif + +pcoq-binaries:: $(COQINTERFACE) + +bin/coq-interface$(EXE): $(COQMKTOP) $(CMO) $(USERTACCMO) $(INTERFACE) + $(SHOW)'COQMKTOP -o $@' + $(HIDE)$(COQMKTOP) -top $(BYTEFLAGS) -o $@ $(INTERFACE) + +bin/coq-interface.opt$(EXE): $(COQMKTOP) $(CMX) $(USERTACCMX) $(INTERFACECMX) + $(SHOW)'COQMKTOP -o $@' + $(HIDE)$(COQMKTOP) -opt $(OPTFLAGS) -o $@ $(INTERFACECMX) + +PARSERCODE=contrib/interface/line_parser.cmo contrib/interface/vtp.cmo \ + contrib/interface/xlate.cmo contrib/interface/parse.cmo +PARSERCMO=$(PARSERREQUIRES) $(PARSERCODE) +PARSERCMX= $(PARSERREQUIRESCMX) $(PARSERCODE:.cmo=.cmx) + +bin/parser$(EXE): $(PARSERCMO) + $(SHOW)'OCAMLC -o $@' + $(HIDE)$(OCAMLC) -linkall -custom -cclib -lunix $(OPTFLAGS) -o $@ \ + dynlink.cma $(CMA) $(PARSERCMO) + +bin/parser.opt$(EXE): $(PARSERCMX) + $(SHOW)'OCAMLOPT -o $@' + $(HIDE)$(OCAMLOPT) -linkall -cclib -lunix $(OPTFLAGS) -o $@ \ + $(CMXA) $(PARSERCMX) + +INTERFACEVO= + +INTERFACERC= contrib/interface/vernacrc + +pcoq-files:: $(INTERFACEVO) $(INTERFACERC) + +# Centaur grammar rules now in centaur.ml4 +contrib7/interface/Centaur.vo: contrib7/interface/Centaur.v $(INTERFACE) + $(BESTCOQTOP) $(TRANSLATE) -boot -byte $(COQOPTS) -compile $* + +# Move the grammar rules to dad.ml ? +contrib7/interface/AddDad.vo: contrib7/interface/AddDad.v $(INTERFACE) states7/initial.coq + $(BESTCOQTOP) $(TRANSLATE) -boot -byte $(COQOPTS) -compile $* + +clean:: + rm -f bin/parser$(EXE) bin/coq-interface$(EXE) bin/coq-interface.opt$(EXE) + +# install targets +install-pcoq:: install-pcoq-binaries install-pcoq-files install-pcoq-manpages + +install-pcoq-binaries:: + $(MKDIR) $(FULLBINDIR) + cp $(COQINTERFACE) $(FULLBINDIR) + +install-pcoq-files:: + $(MKDIR) $(FULLCOQLIB)/contrib/interface + cp $(INTERFACERC) $(FULLCOQLIB)/contrib/interface + +PCOQMANPAGES=man/coq-interface.1 man/parser.1 + +install-pcoq-manpages: + $(MKDIR) $(FULLMANDIR)/man1 + cp $(PCOQMANPAGES) $(FULLMANDIR)/man1 + +########################################################################### +# tests +########################################################################### + +check:: world pcoq + cd test-suite; \ + env COQBIN=../bin COQLIB=.. ./check -$(BEST) | tee check.log + if grep -F 'Error!' test-suite/check.log ; then false; fi + +########################################################################### +# theories and contrib files +########################################################################### + +INITVO=\ + theories/Init/Notations.vo \ + theories/Init/Datatypes.vo theories/Init/Peano.vo \ + theories/Init/Logic.vo theories/Init/Specif.vo \ + theories/Init/Logic_Type.vo theories/Init/Wf.vo \ + theories/Init/Prelude.vo + +init: $(INITVO) + +LOGICVO=\ + theories/Logic/Hurkens.vo theories/Logic/ProofIrrelevance.vo\ + theories/Logic/Classical.vo theories/Logic/Classical_Type.vo \ + theories/Logic/Classical_Pred_Set.vo theories/Logic/Eqdep.vo \ + theories/Logic/Classical_Pred_Type.vo theories/Logic/Classical_Prop.vo \ + theories/Logic/ClassicalFacts.vo theories/Logic/ChoiceFacts.vo \ + theories/Logic/Berardi.vo theories/Logic/Eqdep_dec.vo \ + theories/Logic/Decidable.vo theories/Logic/JMeq.vo \ + theories/Logic/ClassicalDescription.vo theories/Logic/ClassicalChoice.vo \ + theories/Logic/RelationalChoice.vo theories/Logic/Diaconescu.vo + +ARITHVO=\ + theories/Arith/Arith.vo theories/Arith/Gt.vo \ + theories/Arith/Between.vo theories/Arith/Le.vo \ + theories/Arith/Compare.vo theories/Arith/Lt.vo \ + theories/Arith/Compare_dec.vo theories/Arith/Min.vo \ + theories/Arith/Div2.vo theories/Arith/Minus.vo \ + theories/Arith/Mult.vo theories/Arith/Even.vo \ + theories/Arith/EqNat.vo theories/Arith/Peano_dec.vo \ + theories/Arith/Euclid.vo theories/Arith/Plus.vo \ + theories/Arith/Wf_nat.vo theories/Arith/Max.vo \ + theories/Arith/Bool_nat.vo theories/Arith/Factorial.vo \ +# theories/Arith/Div.vo + +SORTINGVO=\ + theories/Sorting/Heap.vo theories/Sorting/Permutation.vo \ + theories/Sorting/Sorting.vo + +BOOLVO=\ + theories/Bool/Bool.vo theories/Bool/IfProp.vo \ + theories/Bool/Zerob.vo theories/Bool/DecBool.vo \ + theories/Bool/Sumbool.vo theories/Bool/BoolEq.vo \ + theories/Bool/Bvector.vo + +NARITHVO=\ + theories/NArith/BinPos.vo theories/NArith/Pnat.vo \ + theories/NArith/BinNat.vo theories/NArith/NArith.vo + +ZARITHVO=\ + theories/ZArith/BinInt.vo theories/ZArith/Wf_Z.vo \ + theories/ZArith/ZArith.vo theories/ZArith/ZArith_dec.vo \ + theories/ZArith/auxiliary.vo theories/ZArith/Zmisc.vo \ + theories/ZArith/Zcompare.vo theories/ZArith/Znat.vo \ + theories/ZArith/Zorder.vo theories/ZArith/Zabs.vo \ + theories/ZArith/Zmin.vo theories/ZArith/Zeven.vo \ + theories/ZArith/Zhints.vo theories/ZArith/Zlogarithm.vo \ + theories/ZArith/Zpower.vo theories/ZArith/Zcomplements.vo \ + theories/ZArith/Zdiv.vo theories/ZArith/Zsqrt.vo \ + theories/ZArith/Zwf.vo theories/ZArith/ZArith_base.vo \ + theories/ZArith/Zbool.vo theories/ZArith/Zbinary.vo \ + theories/ZArith/Znumtheory.vo + +LISTSVO=\ + theories/Lists/MonoList.vo \ + theories/Lists/ListSet.vo theories/Lists/Streams.vo \ + theories/Lists/TheoryList.vo theories/Lists/List.vo + +SETSVO=\ + theories/Sets/Classical_sets.vo theories/Sets/Permut.vo \ + theories/Sets/Constructive_sets.vo theories/Sets/Powerset.vo \ + theories/Sets/Cpo.vo theories/Sets/Powerset_Classical_facts.vo \ + theories/Sets/Ensembles.vo theories/Sets/Powerset_facts.vo \ + theories/Sets/Finite_sets.vo theories/Sets/Relations_1.vo \ + theories/Sets/Finite_sets_facts.vo theories/Sets/Relations_1_facts.vo \ + theories/Sets/Image.vo theories/Sets/Relations_2.vo \ + theories/Sets/Infinite_sets.vo theories/Sets/Relations_2_facts.vo \ + theories/Sets/Integers.vo theories/Sets/Relations_3.vo \ + theories/Sets/Multiset.vo theories/Sets/Relations_3_facts.vo \ + theories/Sets/Partial_Order.vo theories/Sets/Uniset.vo + +INTMAPVO=\ + theories/IntMap/Adalloc.vo theories/IntMap/Mapcanon.vo \ + theories/IntMap/Addec.vo theories/IntMap/Mapcard.vo \ + theories/IntMap/Addr.vo theories/IntMap/Mapc.vo \ + theories/IntMap/Adist.vo theories/IntMap/Mapfold.vo \ + theories/IntMap/Allmaps.vo theories/IntMap/Mapiter.vo \ + theories/IntMap/Fset.vo theories/IntMap/Maplists.vo \ + theories/IntMap/Lsort.vo theories/IntMap/Mapsubset.vo \ + theories/IntMap/Mapaxioms.vo theories/IntMap/Map.vo \ + +RELATIONSVO=\ + theories/Relations/Newman.vo \ + theories/Relations/Operators_Properties.vo \ + theories/Relations/Relation_Definitions.vo \ + theories/Relations/Relation_Operators.vo \ + theories/Relations/Relations.vo \ + theories/Relations/Rstar.vo + +WELLFOUNDEDVO=\ + theories/Wellfounded/Disjoint_Union.vo \ + theories/Wellfounded/Inclusion.vo \ + theories/Wellfounded/Inverse_Image.vo \ + theories/Wellfounded/Lexicographic_Exponentiation.vo \ + theories/Wellfounded/Transitive_Closure.vo \ + theories/Wellfounded/Union.vo \ + theories/Wellfounded/Wellfounded.vo \ + theories/Wellfounded/Well_Ordering.vo \ + theories/Wellfounded/Lexicographic_Product.vo + +REALSBASEVO=\ + theories/Reals/Rdefinitions.vo \ + theories/Reals/Raxioms.vo theories/Reals/RIneq.vo \ + theories/Reals/DiscrR.vo theories/Reals/Rbase.vo \ + +REALS_basic= + +REALS_all=\ + theories/Reals/R_Ifp.vo \ + theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo \ + theories/Reals/SplitAbsolu.vo theories/Reals/SplitRmult.vo \ + theories/Reals/ArithProp.vo theories/Reals/Rfunctions.vo \ + theories/Reals/Rseries.vo theories/Reals/SeqProp.vo \ + theories/Reals/Rcomplete.vo theories/Reals/PartSum.vo \ + theories/Reals/AltSeries.vo theories/Reals/Binomial.vo \ + theories/Reals/Rsigma.vo theories/Reals/Rprod.vo \ + theories/Reals/Cauchy_prod.vo theories/Reals/Alembert.vo \ + theories/Reals/SeqSeries.vo theories/Reals/Rtrigo_fun.vo \ + theories/Reals/Rtrigo_def.vo theories/Reals/Rtrigo_alt.vo \ + theories/Reals/Cos_rel.vo theories/Reals/Cos_plus.vo \ + theories/Reals/Rtrigo.vo theories/Reals/Rlimit.vo \ + theories/Reals/Rderiv.vo theories/Reals/RList.vo \ + theories/Reals/Ranalysis1.vo theories/Reals/Ranalysis2.vo \ + theories/Reals/Ranalysis3.vo theories/Reals/Rtopology.vo \ + theories/Reals/MVT.vo theories/Reals/PSeries_reg.vo \ + theories/Reals/Exp_prop.vo theories/Reals/Rtrigo_reg.vo \ + theories/Reals/Rsqrt_def.vo theories/Reals/R_sqrt.vo \ + theories/Reals/Rtrigo_calc.vo theories/Reals/Rgeom.vo \ + theories/Reals/Sqrt_reg.vo theories/Reals/Ranalysis4.vo \ + theories/Reals/Rpower.vo theories/Reals/Ranalysis.vo \ + theories/Reals/NewtonInt.vo theories/Reals/RiemannInt_SF.vo \ + theories/Reals/RiemannInt.vo theories/Reals/Integration.vo \ + theories/Reals/Reals.vo + +REALSVO=$(REALSBASEVO) $(REALS_$(REALS)) + +ALLREALS=$(REALSBASEVO) $(REALS_all) +ALLOLDREALS=$(REALSBASEVO:theories%.vo:theories7%.vo) $(REALS_all:theories%.vo:theories7%.vo) + +SETOIDSVO=theories/Setoids/Setoid.vo + +THEORIESVO =\ + $(INITVO) $(LOGICVO) $(ARITHVO) $(BOOLVO) $(NARITHVO) $(ZARITHVO) \ + $(LISTSVO) $(SETSVO) $(INTMAPVO) $(RELATIONSVO) $(WELLFOUNDEDVO) \ + $(REALSVO) $(SETOIDSVO) $(SORTINGVO) + +NEWTHEORIESLIGHTVO = $(INITVO) $(LOGICVO) $(ARITHVO) +OLDTHEORIESLIGHTVO = $(NEWTHEORIESLIGHTVO:theories%.vo:theories7%.vo) + +theories: $(THEORIESVO) +theories-light: $(NEWTHEORIESLIGHTVO) + +logic: $(LOGICVO) +arith: $(ARITHVO) +bool: $(BOOLVO) +narith: $(NARITHVO) +zarith: $(ZARITHVO) +lists: $(LISTVO) $(LISTSVO) +sets: $(SETSVO) +intmap: $(INTMAPVO) +relations: $(RELATIONSVO) +wellfounded: $(WELLFOUNDEDVO) +# reals +reals: $(REALSVO) +allreals: $(ALLREALS) +setoids: $(SETOIDSVO) +sorting: $(SORTINGVO) + +noreal: logic arith bool zarith lists sets intmap relations wellfounded \ + setoids sorting + +########################################################################### +# contribs (interface not included) +########################################################################### + +OMEGAVO=\ + contrib/omega/OmegaLemmas.vo contrib/omega/Omega.vo + +ROMEGAVO=\ + contrib/romega/ReflOmegaCore.vo contrib/romega/ROmega.vo + +RINGVO=\ + contrib/ring/ArithRing.vo contrib/ring/Ring_normalize.vo \ + contrib/ring/Ring_theory.vo contrib/ring/Ring.vo \ + contrib/ring/NArithRing.vo \ + contrib/ring/ZArithRing.vo contrib/ring/Ring_abstract.vo \ + contrib/ring/Quote.vo contrib/ring/Setoid_ring_normalize.vo \ + contrib/ring/Setoid_ring.vo contrib/ring/Setoid_ring_theory.vo + +FIELDVO=\ + contrib/field/Field_Compl.vo contrib/field/Field_Theory.vo \ + contrib/field/Field_Tactic.vo contrib/field/Field.vo + +XMLVO= + +FOURIERVO=\ + contrib/fourier/Fourier_util.vo contrib/fourier/Fourier.vo + +FUNINDVO= + +JPROVERVO= + +CCVO=\ + contrib/cc/CCSolve.vo + +CONTRIBVO = $(OMEGAVO) $(ROMEGAVO) $(RINGVO) $(FIELDVO) $(XMLVO) \ + $(FOURIERVO) $(JPROVERVO) $(CCVO) $(FUNINDVO) + +$(CONTRIBVO): states/initial.coq + +contrib: $(CONTRIBVO) $(CONTRIBCMO) +omega: $(OMEGAVO) $(OMEGACMO) $(ROMEGAVO) $(ROMEGACMO) +ring: $(RINGVO) $(RINGCMO) +xml: $(XMLVO) $(XMLCMO) +extraction: $(EXTRACTIONCMO) +field: $(FIELDVO) $(FIELDCMO) +fourier: $(FOURIERVO) $(FOURIERCMO) +jprover: $(JPROVERVO) $(JPROVERCMO) +funind: $(FUNINDCMO) $(FUNINDVO) +cc: $(CCVO) $(CCCMO) + +NEWINITVO=$(INITVO) +NEWTHEORIESVO=$(THEORIESVO) +NEWCONTRIBVO=$(CONTRIBVO) + +OBSOLETETHEORIESVO=\ + theories7/Lists/PolyList.vo theories7/Lists/PolyListSyntax.vo \ + theories7/ZArith/Zsyntax.vo \ + theories7/ZArith/zarith_aux.vo theories7/ZArith/fast_integer.vo \ + theories7/Reals/Rsyntax.vo + +OLDINITVO=$(INITVO:theories%.vo=theories7%.vo) +OLDTHEORIESVO=$(THEORIESVO:theories%.vo=theories7%.vo) $(OBSOLETETHEORIESVO) +OLDCONTRIBVO=$(CONTRIBVO:contrib%.vo=contrib7%.vo) + +$(OLDCONTRIBVO): states7/initial.coq + +NEWINITV=$(INITVO:%.vo=%.v) +NEWTHEORIESV=$(THEORIESVO:%.vo=%.v) +NEWCONTRIBV=$(CONTRIBVO:%.vo=%.v) + +# Made *.vo and new*.v targets explicit, otherwise "make" +# either removes them after use or don't do them (e.g. List.vo) +newinit:: $(NEWINITV) $(NEWINITVO) +newtheories:: $(NEWTHEORIESV) $(NEWTHEORIESVO) +newcontrib:: $(NEWCONTRIBV) $(NEWCONTRIBVO) $(CONTRIBCMO) + +theories7:: $(OLDTHEORIESVO) +contrib7:: $(OLDCONTRIBVO) + +translation:: $(NEWTHEORIESV) $(NEWCONTRIBV) + +ALLNEWVO = $(INITVO) $(THEORIESVO) $(CONTRIBVO) +ALLOLDVO = $(OLDINITVO) $(OLDTHEORIESVO) $(OLDCONTRIBVO) + +########################################################################### +# rules to make theories, contrib and states +########################################################################### + +SYNTAXPP=syntax/PPConstr.v syntax/PPCases.v + +states7/barestate.coq: $(SYNTAXPP) $(BESTCOQTOP) + $(BESTCOQTOP) -v7 -boot -batch -silent -nois -I syntax -load-vernac-source syntax/MakeBare.v -outputstate $@ + +states7/initial.coq: states7/barestate.coq states7/MakeInitial.v $(OLDINITVO) $(BESTCOQTOP) + $(BOOTCOQTOP) -v7 -batch -silent -is states7/barestate.coq -load-vernac-source states7/MakeInitial.v -outputstate states7/initial.coq + +states/initial.coq: states/MakeInitial.v $(NEWINITVO) + $(BOOTCOQTOP) -batch -silent -nois -load-vernac-source states/MakeInitial.v -outputstate states/initial.coq + +theories7/Init/%.vo: $(BESTCOQTOP) theories7/Init/%.v + $(BOOTCOQTOP) $(TRANSLATE) -nois -compile theories7/Init/$* + +theories7/%.vo: theories7/%.v states7/initial.coq + $(BOOTCOQTOP) $(TRANSLATE) -compile theories7/$* + +contrib7/%.vo: contrib7/%.v states7/initial.coq + $(BOOTCOQTOP) $(TRANSLATE) -compile contrib7/$* + +theories/Init/%.vo: $(BESTCOQTOP) theories/Init/%.v + $(BOOTCOQTOP) -nois -compile theories/Init/$* + +theories/%.vo: theories/%.v states/initial.coq + $(BOOTCOQTOP) -compile theories/$* + +contrib/%.vo: contrib/%.v + $(BOOTCOQTOP) -compile contrib/$* + +contrib/extraction/%.vo: contrib/extraction/%.v states/barestate.coq $(COQC) + $(BOOTCOQTOP) -is states/barestate.coq -compile $* + +contrib7/extraction/%.vo: contrib7/extraction/%.v states/barestate.coq $(COQC) + $(BOOTCOQTOP) $(TRANSLATE) -is states7/barestate.coq -compile $* + +clean:: + rm -f states/*.coq states7/*.coq + rm -f theories/*/*.vo theories7/*/*.vo + rm -f contrib/*/*.cm[io] contrib/*.cma contrib/*/*.vo contrib7/*/*.vo + +archclean:: + rm -f contrib/*/*.cmx contrib/*.cmxa contrib/*.a contrib/*/*.[so] + +# globalizations (for coqdoc) + +glob.dump:: + rm -f glob.dump + rm -f theories/*/*.vo + $(MAKE) GLOB="-dump-glob glob.dump" world + +########################################################################### +# tools +########################################################################### + +COQDEP=bin/coqdep$(EXE) +COQMAKEFILE=bin/coq_makefile$(EXE) +GALLINA=bin/gallina$(EXE) +COQTEX=bin/coq-tex$(EXE) +COQWC=bin/coqwc$(EXE) +COQDOC=bin/coqdoc$(EXE) + +TOOLS=$(COQDEP) $(COQMAKEFILE) $(GALLINA) $(COQTEX) \ + $(COQWC) $(COQDOC) + +tools:: $(TOOLS) dev/top_printers.cmo + +COQDEPCMO=config/coq_config.cmo tools/coqdep_lexer.cmo tools/coqdep.cmo + +$(COQDEP): $(COQDEPCMO) + $(SHOW)'OCAMLC -o $@' + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -custom -o $@ unix.cma $(COQDEPCMO) $(OSDEPLIBS) + +beforedepend:: tools/coqdep_lexer.ml $(COQDEP) + +GALLINACMO=tools/gallina_lexer.cmo tools/gallina.cmo + +$(GALLINA): $(GALLINACMO) + $(SHOW)'OCAMLC -o $@' + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -custom -o $@ $(GALLINACMO) + +beforedepend:: tools/gallina_lexer.ml + +$(COQMAKEFILE): tools/coq_makefile.cmo + $(SHOW)'OCAMLC -o $@' + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -custom -o $@ tools/coq_makefile.cmo + +$(COQTEX): tools/coq-tex.cmo + $(SHOW)'OCAMLC -o $@' + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -custom -o $@ str.cma tools/coq-tex.cmo + +beforedepend:: tools/coqwc.ml + +$(COQWC): tools/coqwc.cmo + $(SHOW)'OCAMLC -o $@' + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -custom -o $@ tools/coqwc.cmo + +beforedepend:: tools/coqdoc/pretty.ml tools/coqdoc/index.ml + +COQDOCCMO=$(CONFIG) tools/coqdoc/alpha.cmo tools/coqdoc/index.cmo \ + tools/coqdoc/output.cmo tools/coqdoc/pretty.cmo \ + tools/coqdoc/main.cmo + +$(COQDOC): $(COQDOCCMO) + $(SHOW)'OCAMLC -o $@' + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -custom -o $@ str.cma unix.cma $(COQDOCCMO) + +clean:: + rm -f tools/coqdep_lexer.ml tools/gallina_lexer.ml + rm -f tools/coqwc.ml + rm -f tools/coqdoc/pretty.ml tools/coqdoc/index.ml + +archclean:: + rm -f $(TOOLS) + +########################################################################### +# minicoq +########################################################################### + +MINICOQCMO=$(CONFIG) $(LIBREP) $(KERNEL) \ + parsing/lexer.cmo parsing/g_minicoq.cmo \ + toplevel/fhimsg.cmo toplevel/minicoq.cmo + +MINICOQ=bin/minicoq$(EXE) + +$(MINICOQ): $(MINICOQCMO) + $(SHOW)'OCAMLC -o $@' + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ -custom $(CMA) $(MINICOQCMO) $(OSDEPLIBS) + +archclean:: + rm -f $(MINICOQ) + +########################################################################### +# Installation +########################################################################### + +COQINSTALLPREFIX= + # Can be changed for a local installation (to make packages). + # You must NOT put a "/" at the end (Cygnus for win32 does not like "//"). + +FULLBINDIR=$(COQINSTALLPREFIX)$(BINDIR) +FULLCOQLIB=$(COQINSTALLPREFIX)$(COQLIB) +FULLMANDIR=$(COQINSTALLPREFIX)$(MANDIR) +FULLEMACSLIB=$(COQINSTALLPREFIX)$(EMACSLIB) +FULLCOQDOCDIR=$(COQINSTALLPREFIX)$(COQDOCDIR) + +install-coq: install-binaries install-library install-coq-info +install-coq8: install-binaries install-library8 install-coq-info +install-coq7: install-binaries install-library7 install-coq-info +install-coqlight: install-binaries install-library-light + +install-binaries:: install-$(BEST) install-tools + +install-byte:: + $(MKDIR) $(FULLBINDIR) + cp $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(FULLBINDIR) + cd $(FULLBINDIR); ln -sf coqtop.byte$(EXE) coqtop$(EXE) + +install-opt:: + $(MKDIR) $(FULLBINDIR) + cp $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(COQTOPOPT) $(FULLBINDIR) + cd $(FULLBINDIR); ln -sf coqtop.opt$(EXE) coqtop$(EXE) + +install-tools:: + $(MKDIR) $(FULLBINDIR) + cp $(TOOLS) $(FULLBINDIR) + +LIBFILES=$(OLDTHEORIESVO) $(OLDCONTRIBVO) +LIBFILESLIGHT=$(OLDTHEORIESLIGHTVO) + +NEWLIBFILES=$(NEWTHEORIESVO) $(NEWCONTRIBVO) +NEWLIBFILESLIGHT=$(NEWTHEORIESLIGHTVO) + +install-library: install-library7 install-library8 + +install-library8: + $(MKDIR) $(FULLCOQLIB) + for f in $(NEWLIBFILES); do \ + $(MKDIR) $(FULLCOQLIB)/`dirname $$f`; \ + cp $$f $(FULLCOQLIB)/`dirname $$f`; \ + done + $(MKDIR) $(FULLCOQLIB)/states + cp states/*.coq $(FULLCOQLIB)/states + +install-library7: + $(MKDIR) $(FULLCOQLIB) + for f in $(LIBFILES); do \ + $(MKDIR) $(FULLCOQLIB)/`dirname $$f`; \ + cp $$f $(FULLCOQLIB)/`dirname $$f`; \ + done + $(MKDIR) $(FULLCOQLIB)/states7 + cp states7/*.coq $(FULLCOQLIB)/states7 + +install-library-light: + $(MKDIR) $(FULLCOQLIB) + for f in $(LIBFILESLIGHT) $(NEWLIBFILESLIGHT); do \ + $(MKDIR) $(FULLCOQLIB)/`dirname $$f`; \ + cp $$f $(FULLCOQLIB)/`dirname $$f`; \ + done + $(MKDIR) $(FULLCOQLIB)/states + cp states/*.coq $(FULLCOQLIB)/states + $(MKDIR) $(FULLCOQLIB)/states7 + cp states7/*.coq $(FULLCOQLIB)/states7 + +install-allreals:: + for f in $(ALLREALS); do \ + $(MKDIR) $(FULLCOQLIB)/`dirname $$f`; \ + cp $$f $(FULLCOQLIB)/`dirname $$f`; \ + done + +install-coq-info: install-coq-manpages install-emacs install-latex + +MANPAGES=man/coq-tex.1 man/coqdep.1 man/gallina.1 \ + man/coqc.1 man/coqtop.1 man/coqtop.byte.1 man/coqtop.opt.1 \ + man/coqwc.1 man/coqdoc.1 \ + man/coq_makefile.1 man/coqmktop.1 + +install-coq-manpages: + $(MKDIR) $(FULLMANDIR)/man1 + cp $(MANPAGES) $(FULLMANDIR)/man1 + +install-emacs: + $(MKDIR) $(FULLEMACSLIB) + cp tools/coq.el tools/coq-inferior.el $(FULLEMACSLIB) + +# command to update TeX' kpathsea database +#UPDATETEX = $(MKTEXLSR) /usr/share/texmf /var/spool/texmf $(BASETEXDIR) > /dev/null + +install-latex: + $(MKDIR) $(FULLCOQDOCDIR) + cp tools/coqdoc/coqdoc.sty $(FULLCOQDOCDIR) +# -$(UPDATETEX) + +########################################################################### +# Documentation +# Literate programming (with ocamlweb) +########################################################################### + +.PHONY: doc + +doc: doc/coq.tex + $(MAKE) -C doc coq.ps minicoq.dvi + +LPLIB = lib/doc.tex $(LIBREP:.cmo=.mli) +LPKERNEL = kernel/doc.tex $(KERNEL:.cmo=.mli) +LPLIBRARY = library/doc.tex $(LIBRARY:.cmo=.mli) +LPPRETYPING = pretyping/doc.tex pretyping/rawterm.mli $(PRETYPING:.cmo=.mli) +LPINTERP = $(INTERP:.cmo=.mli) +LPPARSING = $(PARSING:.cmo=.mli) $(HIGHPARSING:.cmo=.mli) +LPPROOFS = proofs/doc.tex $(PROOFS:.cmo=.mli) +LPTACTICS = tactics/doc.tex $(TACTICS:.cmo=.mli) $(HIGHTACTICS:.cmo=.mli) +LPTOPLEVEL = toplevel/doc.tex $(TOPLEVEL:.cmo=.mli) +LPFILES = doc/macros.tex doc/intro.tex $(LPLIB) $(LPKERNEL) $(LPLIBRARY) \ + $(LPPRETYPING) $(LPPROOFS) $(LPTACTICS) $(LPTOPLEVEL) + +doc/coq.tex: $(LPFILES) + ocamlweb -p "\usepackage{epsfig}" $(LPFILES) -o doc/coq.tex +# ocamlweb $(LPFILES) -o doc/coq.tex + +clean:: + rm -f doc/coq.tex + +########################################################################### +# Emacs tags +########################################################################### + +# NB: the -maxdepth 3 is for excluding files from contrib/extraction/test + +tags: + find . -maxdepth 3 -regex ".*\.ml[i4]?" | sort -r | xargs \ + etags --language=none\ + "--regex=/let[ \t]+\([^ \t]+\)/\1/" \ + "--regex=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \ + "--regex=/and[ \t]+\([^ \t]+\)/\1/" \ + "--regex=/type[ \t]+\([^ \t]+\)/\1/" \ + "--regex=/exception[ \t]+\([^ \t]+\)/\1/" \ + "--regex=/val[ \t]+\([^ \t]+\)/\1/" \ + "--regex=/module[ \t]+\([^ \t]+\)/\1/" + +otags: + find . -maxdepth 3 -name "*.ml" -o -name "*.mli" \ + | sort -r | xargs otags + find . -maxdepth 3 -name "*.ml4" | sort -r | xargs \ + etags --append --language=none\ + "--regex=/let[ \t]+\([^ \t]+\)/\1/" \ + "--regex=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \ + "--regex=/and[ \t]+\([^ \t]+\)/\1/" \ + "--regex=/type[ \t]+\([^ \t]+\)/\1/" \ + "--regex=/exception[ \t]+\([^ \t]+\)/\1/" \ + "--regex=/val[ \t]+\([^ \t]+\)/\1/" \ + "--regex=/module[ \t]+\([^ \t]+\)/\1/" + + +########################################################################### +### Special rules +########################################################################### + +# grammar modules with camlp4 + +ML4FILES += parsing/lexer.ml4 parsing/q_util.ml4 parsing/q_coqast.ml4 \ + parsing/g_prim.ml4 parsing/pcoq.ml4 + +GRAMMARNEEDEDCMO=\ + lib/pp_control.cmo lib/pp.cmo lib/compat.cmo lib/util.cmo lib/bignat.cmo \ + lib/dyn.cmo lib/options.cmo \ + lib/hashcons.cmo lib/predicate.cmo lib/rtree.cmo \ + kernel/names.cmo kernel/univ.cmo kernel/esubst.cmo kernel/term.cmo \ + kernel/sign.cmo kernel/declarations.cmo kernel/environ.cmo\ + library/nameops.cmo library/libnames.cmo library/summary.cmo \ + library/nametab.cmo library/libobject.cmo library/lib.cmo \ + library/goptions.cmo library/decl_kinds.cmo \ + pretyping/rawterm.cmo pretyping/pattern.cmo pretyping/evd.cmo \ + interp/topconstr.cmo interp/genarg.cmo \ + interp/ppextend.cmo parsing/coqast.cmo parsing/ast.cmo \ + proofs/tacexpr.cmo parsing/ast.cmo \ + parsing/lexer.cmo parsing/q_util.cmo parsing/extend.cmo \ + toplevel/vernacexpr.cmo parsing/pcoq.cmo parsing/q_coqast.cmo \ + parsing/egrammar.cmo + +CAMLP4EXTENSIONSCMO=\ + parsing/argextend.cmo parsing/tacextend.cmo parsing/vernacextend.cmo + +GRAMMARSCMO=\ + parsing/g_prim.cmo parsing/g_tactic.cmo \ + parsing/g_ltac.cmo parsing/g_constr.cmo \ + parsing/g_primnew.cmo parsing/g_tacticnew.cmo \ + parsing/g_ltacnew.cmo parsing/g_constrnew.cmo + +GRAMMARCMO=$(GRAMMARNEEDEDCMO) $(CAMLP4EXTENSIONSCMO) $(GRAMMARSCMO) + +parsing/grammar.cma: $(GRAMMARCMO) + $(SHOW)'OCAMLC -a $@' + $(HIDE)$(OCAMLC) $(BYTEFLAGS) $(GRAMMARCMO) -linkall -a -o $@ + +clean:: + rm -f parsing/grammar.cma + +ML4FILES +=parsing/g_basevernac.ml4 parsing/g_minicoq.ml4 \ + parsing/g_vernac.ml4 parsing/g_proofs.ml4 \ + parsing/g_cases.ml4 \ + parsing/g_constr.ml4 parsing/g_module.ml4 \ + parsing/g_tactic.ml4 parsing/g_ltac.ml4 \ + parsing/argextend.ml4 parsing/tacextend.ml4 \ + parsing/vernacextend.ml4 \ + parsing/g_primnew.ml4 \ + parsing/g_vernacnew.ml4 parsing/g_proofsnew.ml4 \ + parsing/g_constrnew.ml4 \ + parsing/g_tacticnew.ml4 parsing/g_ltacnew.ml4 \ + +# beforedepend:: $(GRAMMARCMO) + +# beforedepend:: parsing/pcoq.ml parsing/extend.ml + +# toplevel/mltop.ml4 (ifdef Byte) + +toplevel/mltop.cmo: toplevel/mltop.byteml + $(SHOW)'OCAMLC $<' + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -c -impl $< -o $@ + +toplevel/mltop.cmx: toplevel/mltop.optml + $(SHOW)'OCAMLOPT $<' + $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -c -impl $< -o $@ + +toplevel/mltop.byteml: toplevel/mltop.ml4 + $(SHOW)'CAMLP4O $<' + $(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pr_o.cmo -DByte -impl $< > $@ || rm -f $@ + +toplevel/mltop.optml: toplevel/mltop.ml4 + $(SHOW)'CAMLP4O $<' + $(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pr_o.cmo -impl $< > $@ || rm -f $@ + +ML4FILES += toplevel/mltop.ml4 + +clean:: + rm -f toplevel/mltop.byteml toplevel/mltop.optml + +# files compiled with -rectypes + +kernel/term.cmo: kernel/term.ml + $(SHOW)'OCAMLC -rectypes $<' + $(HIDE)$(OCAMLC) -rectypes $(BYTEFLAGS) -c $< + +kernel/term.cmx: kernel/term.ml + $(SHOW)'OCAMLOPT -rectypes $<' + $(HIDE)$(OCAMLOPT) -rectypes $(OPTFLAGS) -c $< + +library/nametab.cmo: library/nametab.ml + $(SHOW)'OCAMLC -rectypes $<' + $(HIDE)$(OCAMLC) -rectypes $(BYTEFLAGS) -c $< + +library/nametab.cmx: library/nametab.ml + $(SHOW)'OCAMLOPT -rectypes $<' + $(HIDE)$(OCAMLOPT) -rectypes $(OPTFLAGS) -c $< + +proofs/tacexpr.cmo: proofs/tacexpr.ml + $(SHOW)'OCAMLC -rectypes $<' + $(HIDE)$(OCAMLC) -rectypes $(BYTEFLAGS) -c $< + +proofs/tacexpr.cmx: proofs/tacexpr.ml + $(SHOW)'OCAMLOPT -rectypes $<' + $(HIDE)$(OCAMLOPT) -rectypes $(OPTFLAGS) -c $< + +# files compiled with camlp4 because of macros + +lib/compat.cmo: lib/compat.ml4 + $(SHOW)'OCAMLC4 $<' + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) -D$(CAMLVERSION) -impl" -c -impl $< + +lib/compat.cmx: lib/compat.ml4 + $(SHOW)'OCAMLOPT $<' + $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) -D$(CAMLVERSION) -impl" -c -impl $< + +# files compiled with camlp4 because of streams syntax + +ML4FILES += lib/pp.ml4 \ + lib/compat.ml4 \ + contrib/xml/xml.ml4 \ + contrib/xml/acic2Xml.ml4 \ + contrib/xml/proofTree2Xml.ml4 \ + contrib/interface/line_parser.ml4 \ + tools/coq_makefile.ml4 \ + tools/coq-tex.ml4 + +# Add pr_o.cmo to circumvent a useless-warning bug when preprocessed with +# ast-based camlp4 + +#parsing/lexer.cmx: parsing/lexer.ml4 +# $(SHOW)'OCAMLOPT4 $<' +# $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4DEPS) $<` pr_o.cmo -impl" -c -impl $< + +#parsing/lexer.cmo: parsing/lexer.ml4 +# $(SHOW)'OCAMLC4 $<' +# $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4DEPS) $<` pr_o.cmo -impl" -c -impl $< + + + +########################################################################### +# Default rules +########################################################################### + +.SUFFIXES: .ml .mli .cmo .cmi .cmx .mll .mly .ml4 .v .vo .el .elc + +.ml.cmo: + $(SHOW)'OCAMLC $<' + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -c $< + +.mli.cmi: + $(SHOW)'OCAMLC $<' + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -c $< + +.ml.cmx: + $(SHOW)'OCAMLOPT $<' + $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -c $< + +.mll.ml: + $(SHOW)'OCAMLLEX $<' + $(HIDE)ocamllex $< + +.mly.ml: + $(SHOW)'OCAMLYACC $<' + $(HIDE)ocamlyacc $< + +.mly.mli: + $(SHOW)'OCAMLYACC $<' + $(HIDE)ocamlyacc $< + +.ml4.cmx: + $(SHOW)'OCAMLOPT4 $<' + $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4DEPS) $<` -impl" -c -impl $< + +.ml4.cmo: + $(SHOW)'OCAMLC4 $<' + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4DEPS) $<` -impl" -c -impl $< + +#.v.vo: +# $(BOOTCOQTOP) -compile $* + +.el.elc: + echo "(setq load-path (cons \".\" load-path))" > $*.compile + echo "(byte-compile-file \"$<\")" >> $*.compile + - $(EMACS) -batch -l $*.compile + rm -f $*.compile + +########################################################################### +# Cleaning +########################################################################### + +archclean:: + rm -f config/*.cmx* config/*.[soa] + rm -f lib/*.cmx* lib/*.[soa] + rm -f kernel/*.cmx* kernel/*.[soa] + rm -f library/*.cmx* library/*.[soa] + rm -f proofs/*.cmx* proofs/*.[soa] + rm -f tactics/*.cmx* tactics/*.[soa] + rm -f interp/*.cmx* interp/*.[soa] + rm -f parsing/*.cmx* parsing/*.[soa] + rm -f pretyping/*.cmx* pretyping/*.[soa] + rm -f toplevel/*.cmx* toplevel/*.[soa] + rm -f ide/*.cmx* ide/*.[soa] + rm -f ide/utils/*.cmx* ide/utils/*.[soa] + rm -f translate/*.cmx* translate/*.[soa] + rm -f tools/*.cmx* tools/*.[soa] + rm -f tools/*/*.cmx* tools/*/*.[soa] + rm -f scripts/*.cmx* scripts/*.[soa] + rm -f dev/*.cmx* dev/*.[soa] + +clean:: archclean + rm -f *~ */*~ */*/*~ + rm -f gmon.out core + rm -f config/*.cm[ioa] + rm -f lib/*.cm[ioa] + rm -f kernel/*.cm[ioa] + rm -f library/*.cm[ioa] + rm -f proofs/*.cm[ioa] + rm -f tactics/*.cm[ioa] + rm -f interp/*.cm[ioa] + rm -f parsing/*.cm[ioa] parsing/*.ppo + rm -f pretyping/*.cm[ioa] + rm -f toplevel/*.cm[ioa] + rm -f ide/*.cm[ioa] + rm -f ide/utils/*.cm[ioa] + rm -f translate/*.cm[ioa] + rm -f tools/*.cm[ioa] + rm -f tools/*/*.cm[ioa] + rm -f scripts/*.cm[ioa] + rm -f dev/*.cm[ioa] + rm -f */*.pp[iox] contrib/*/*.pp[iox] + +cleanconfig:: + rm -f config/Makefile config/coq_config.ml dev/ocamldebug-v7 + +########################################################################### +# Dependencies +########################################################################### + +alldepend: depend dependcoq + +dependcoq:: beforedepend + $(COQDEP) -coqlib . -R theories Coq -R contrib Coq $(COQINCLUDES) \ + $(ALLREALS:.vo=.v) $(ALLNEWVO:.vo=.v) > .depend.coq + $(COQDEP) -coqlib . -R theories7 Coq -R contrib7 Coq $(COQINCLUDES) \ + $(ALLOLDREALS:.vo=.v) $(ALLOLDVO:.vo=.v) > .depend.coq7 + +# Build dependencies ignoring failures in building ml files from ml4 files +# This is useful to rebuild dependencies when they are strongly corrupted: +# by making scratchdepend, one gets dependencies OK for .ml files and +# .ml4 files not using fancy parsers. This is sufficient to get beforedepend +# and depend targets successfully built +scratchdepend:: dependp4 + -$(MAKE) -k -f Makefile.dep $(ML4FILESML) + $(OCAMLDEP) $(DEPFLAGS) */*.mli */*/*.mli */*.ml */*/*.ml > .depend + $(MAKE) depend + + +# Computing the dependencies in camlp4 files is tricky. +# We proceed in several steps: + +ML4FILESML = $(ML4FILES:.ml4=.ml) + +# Expresses dependencies of the .ml4 files w.r.t their grammars +dependp4:: + rm -f .depend.camlp4 + for f in $(ML4FILES); do \ + printf "%s" `dirname $$f`/`basename $$f .ml4`".ml: " >> .depend.camlp4; \ + echo `$(CAMLP4DEPS) $$f` >> .depend.camlp4; \ + done + +# Produce the .ml files using Makefile.dep +ml4filesml:: .depend.camlp4 + $(MAKE) -f Makefile.dep $(ML4FILESML) + +depend: beforedepend dependp4 ml4filesml +# 1. We express dependencies of the .ml files w.r.t their grammars +# 2. Then we are able to produce the .ml files using Makefile.dep +# 3. We compute the dependencies inside the .ml files using ocamldep + $(OCAMLDEP) $(DEPFLAGS) */*.mli */*/*.mli */*.ml */*/*.ml > .depend +# 4. We express dependencies of .cmo and .cmx files w.r.t their grammars + for f in $(ML4FILES); do \ + printf "%s" `dirname $$f`/`basename $$f .ml4`".cmo: " >> .depend; \ + echo `$(CAMLP4DEPS) $$f` >> .depend; \ + printf "%s" `dirname $$f`/`basename $$f .ml4`".cmx: " >> .depend; \ + echo `$(CAMLP4DEPS) $$f` >> .depend; \ + done +# 5. Finally, we erase the generated .ml files + rm -f $(ML4FILESML) +# 6. Since .depend contains correct dependencies .depend.devel can be deleted +# (see dev/Makefile.dir for details about this file) + if [ -e makefile ]; then >.depend.devel; else rm -f .depend.devel; fi + +ml4clean:: + rm -f $(ML4FILESML) + +clean:: + rm -f $(ML4FILESML) + +# this sets up developper supporting stuff +devel: + touch .depend.devel + $(MAKE) -f dev/Makefile.devel setup-devel + $(MAKE) dev/top_printers.cmo + +include .depend +include .depend.coq +include .depend.coq7 + +clean:: + rm -fr *.v8 syntax/*.v8 ide/*.v8 theories7/*/*.v8 contrib7/*/*.v8 + find . -name "\.#*" -exec rm -f {} \; + find . -name "*~" -exec rm -f {} \; + +########################################################################### |