diff options
Diffstat (limited to 'Makefile.common')
-rw-r--r-- | Makefile.common | 890 |
1 files changed, 890 insertions, 0 deletions
diff --git a/Makefile.common b/Makefile.common new file mode 100644 index 00000000..509ceedb --- /dev/null +++ b/Makefile.common @@ -0,0 +1,890 @@ +####################################################################### +# v # The Coq Proof Assistant / The Coq Development Team # +# <O___,, # INRIA-Rocquencourt & LRI-CNRS-Orsay # +# \VV/ ############################################################# +# // # This file is distributed under the terms of the # +# # GNU Lesser General Public License Version 2.1 # +####################################################################### + +-include config/Makefile + +########################################################################### +# Executables +########################################################################### + +COQMKTOPBYTE:=bin/coqmktop.byte$(EXE) +COQMKTOPOPT:=bin/coqmktop.opt$(EXE) +BESTCOQMKTOP:=bin/coqmktop.$(BEST)$(EXE) +COQMKTOP:=bin/coqmktop$(EXE) +COQCBYTE:=bin/coqc.byte$(EXE) +COQCOPT:=bin/coqc.opt$(EXE) +BESTCOQC:=bin/coqc.$(BEST)$(EXE) +COQC:=bin/coqc$(EXE) +COQTOPBYTE:=bin/coqtop.byte$(EXE) +COQTOPOPT:=bin/coqtop.opt$(EXE) +BESTCOQTOP:=bin/coqtop.$(BEST)$(EXE) +COQTOP:=bin/coqtop$(EXE) +CHICKENBYTE:=bin/coqchk.byte$(EXE) +CHICKENOPT:=bin/coqchk.opt$(EXE) +BESTCHICKEN:=bin/coqchk.$(BEST)$(EXE) +CHICKEN:=bin/coqchk$(EXE) + +INSTALLBIN:=install +INSTALLLIB:=install -m 644 +MKDIR:=install -d + +COQIDEBYTE:=bin/coqide.byte$(EXE) +COQIDEOPT:=bin/coqide.opt$(EXE) +COQIDE:=bin/coqide$(EXE) + +ifeq ($(BEST),opt) +COQBINARIES:= $(COQMKTOP) $(COQC) \ + $(COQTOPBYTE) $(COQTOPOPT) $(COQTOP) $(CHICKENBYTE) $(CHICKENOPT) $(CHICKEN) +else +COQBINARIES:= $(COQMKTOP) $(COQC) \ + $(COQTOPBYTE) $(COQTOP) $(CHICKENBYTE) $(CHICKEN) +endif +OTHERBINARIES:=$(COQMKTOPBYTE) $(COQCBYTE) + +MINICOQ:=bin/minicoq$(EXE) + +CSDPCERT:=bin/csdpcert$(EXE) + +########################################################################### +# 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) + +########################################################################### +# Documentation +########################################################################### + +LATEX:=latex +BIBTEX:=bibtex -min-crossrefs=10 +MAKEINDEX:=makeindex +PDFLATEX:=pdflatex +HEVEA:=hevea +HEVEAOPTS:=-fix -exec xxdate.exe +HEVEALIB:=/usr/local/lib/hevea:/usr/lib/hevea +export TEXINPUTS:=$(COQSRC)/doc:$(HEVEALIB): +COQTEXOPTS:=-n 72 -image $(COQSRC)/$(COQTOP) -v -sl -small + +DOCCOMMON:=doc/common/version.tex doc/common/title.tex doc/common/macros.tex + +REFMANCOQTEXFILES:=\ + doc/refman/RefMan-gal.v.tex doc/refman/RefMan-ext.v.tex \ + doc/refman/RefMan-mod.v.tex doc/refman/RefMan-tac.v.tex \ + doc/refman/RefMan-cic.v.tex doc/refman/RefMan-lib.v.tex \ + doc/refman/RefMan-tacex.v.tex doc/refman/RefMan-syn.v.tex \ + doc/refman/RefMan-oth.v.tex doc/refman/RefMan-ltac.v.tex \ + doc/refman/RefMan-decl.v.tex \ + doc/refman/Cases.v.tex doc/refman/Coercion.v.tex doc/refman/Extraction.v.tex \ + doc/refman/Program.v.tex doc/refman/Omega.v.tex doc/refman/Polynom.v.tex \ + doc/refman/Setoid.v.tex doc/refman/Helm.tex doc/refman/Classes.v.tex + +REFMANTEXFILES:=\ + doc/refman/headers.sty \ + doc/refman/Reference-Manual.tex doc/refman/RefMan-pre.tex \ + doc/refman/RefMan-int.tex doc/refman/RefMan-pro.tex \ + doc/refman/RefMan-com.tex \ + doc/refman/RefMan-uti.tex doc/refman/RefMan-ide.tex \ + doc/refman/RefMan-add.tex doc/refman/RefMan-modr.tex \ + doc/refman/ExternalProvers.tex \ + $(REFMANCOQTEXFILES) \ + +REFMANEPSFILES:=doc/refman/coqide.eps doc/refman/coqide-queries.eps + +REFMANFILES:=$(REFMANTEXFILES) $(COMMON) $(REFMANEPSFILES) doc/refman/biblio.bib + +REFMANPNGFILES:=$(REFMANEPSFILES:.eps=.png) + + + +########################################################################### +# Object and Source files +########################################################################### + +LIBCOQRUN:=kernel/byterun/libcoqrun.a + +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/bigint.cmo \ + lib/hashcons.cmo lib/dyn.cmo lib/system.cmo lib/flags.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 lib/option.cmo +# Rem: Cygwin already uses variable LIB + +BYTERUN:=\ + kernel/byterun/coq_fix_code.o kernel/byterun/coq_memory.o \ + kernel/byterun/coq_values.o kernel/byterun/coq_interp.o + +KERNEL:=\ + kernel/names.cmo kernel/univ.cmo \ + kernel/esubst.cmo kernel/term.cmo \ + kernel/mod_subst.cmo kernel/sign.cmo \ + kernel/cbytecodes.cmo kernel/copcodes.cmo \ + kernel/cemitcodes.cmo kernel/vm.cmo \ + kernel/declarations.cmo \ + kernel/retroknowledge.cmo kernel/pre_env.cmo \ + kernel/cbytegen.cmo kernel/environ.cmo \ + kernel/csymtable.cmo kernel/conv_oracle.cmo \ + kernel/closure.cmo kernel/reduction.cmo kernel/type_errors.cmo \ + kernel/entries.cmo kernel/modops.cmo \ + kernel/inductive.cmo kernel/vconv.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 \ + library/decls.cmo library/heads.cmo + +PRETYPING:=\ + pretyping/termops.cmo pretyping/evd.cmo \ + pretyping/reductionops.cmo pretyping/vnorm.cmo pretyping/inductiveops.cmo \ + pretyping/retyping.cmo pretyping/cbv.cmo \ + pretyping/pretype_errors.cmo pretyping/recordops.cmo pretyping/typing.cmo \ + pretyping/tacred.cmo pretyping/evarutil.cmo pretyping/evarconv.cmo \ + pretyping/typeclasses_errors.cmo pretyping/typeclasses.cmo \ + pretyping/classops.cmo pretyping/coercion.cmo \ + pretyping/unification.cmo pretyping/clenv.cmo \ + pretyping/rawterm.cmo pretyping/pattern.cmo \ + pretyping/detyping.cmo pretyping/indrec.cmo\ + pretyping/cases.cmo pretyping/pretyping.cmo pretyping/matching.cmo + +INTERP:=\ + parsing/lexer.cmo interp/topconstr.cmo interp/ppextend.cmo \ + interp/notation.cmo \ + interp/genarg.cmo interp/syntax_def.cmo interp/reserve.cmo \ + library/impargs.cmo interp/implicit_quantifiers.cmo interp/constrintern.cmo \ + interp/modintern.cmo interp/constrextern.cmo interp/coqlib.cmo \ + toplevel/discharge.cmo library/declare.cmo + +PROOFS:=\ + proofs/tacexpr.cmo proofs/proof_type.cmo proofs/redexpr.cmo \ + proofs/proof_trees.cmo proofs/logic.cmo \ + proofs/refiner.cmo proofs/evar_refiner.cmo proofs/tacmach.cmo \ + proofs/pfedit.cmo proofs/tactic_debug.cmo \ + proofs/clenvtac.cmo proofs/decl_mode.cmo + +PARSING:=\ + parsing/extend.cmo \ + parsing/pcoq.cmo parsing/egrammar.cmo parsing/g_xml.cmo \ + parsing/ppconstr.cmo parsing/printer.cmo \ + parsing/pptactic.cmo parsing/ppdecl_proof.cmo parsing/tactic_printer.cmo \ + parsing/printmod.cmo parsing/prettyp.cmo parsing/search.cmo + +HIGHPARSING:=\ + parsing/g_constr.cmo parsing/g_vernac.cmo parsing/g_prim.cmo \ + parsing/g_proofs.cmo parsing/g_tactic.cmo parsing/g_ltac.cmo \ + parsing/g_natsyntax.cmo parsing/g_zsyntax.cmo parsing/g_rsyntax.cmo \ + parsing/g_ascii_syntax.cmo parsing/g_string_syntax.cmo \ + parsing/g_decl_mode.cmo parsing/g_intsyntax.cmo + +TACTICS:=\ + tactics/dn.cmo tactics/termdn.cmo tactics/btermdn.cmo \ + tactics/nbtermdn.cmo tactics/tacticals.cmo \ + tactics/hipattern.cmo tactics/tactics.cmo \ + tactics/evar_tactics.cmo \ + tactics/hiddentac.cmo tactics/elim.cmo \ + tactics/dhyp.cmo tactics/auto.cmo \ + toplevel/ind_tables.cmo \ + tactics/setoid_replace.cmo tactics/equality.cmo \ + tactics/contradiction.cmo tactics/inv.cmo tactics/leminv.cmo \ + tactics/tacinterp.cmo tactics/autorewrite.cmo \ + tactics/decl_interp.cmo tactics/decl_proof_instr.cmo + +TOPLEVEL:=\ + toplevel/himsg.cmo toplevel/cerrors.cmo \ + toplevel/class.cmo toplevel/vernacexpr.cmo toplevel/metasyntax.cmo \ + toplevel/auto_ind_decl.cmo \ + toplevel/command.cmo toplevel/record.cmo \ + parsing/ppvernac.cmo toplevel/classes.cmo \ + toplevel/vernacinterp.cmo toplevel/mltop.cmo \ + toplevel/vernacentries.cmo toplevel/whelp.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/refine.cmo tactics/extraargs.cmo \ + tactics/extratactics.cmo tactics/eauto.cmo tactics/class_tactics.cmo \ + tactics/tauto.cmo tactics/eqdecide.cmo + +OMEGACMO:=\ + contrib/omega/omega.cmo contrib/omega/coq_omega.cmo \ + contrib/omega/g_omega.cmo + +ROMEGACMO:=\ + contrib/romega/const_omega.cmo \ + contrib/romega/refl_omega.cmo contrib/romega/g_romega.cmo + +MICROMEGACMO:=\ + contrib/micromega/mutils.cmo contrib/micromega/vector.cmo \ + contrib/micromega/micromega.cmo contrib/micromega/mfourier.cmo \ + contrib/micromega/certificate.cmo \ + contrib/micromega/coq_micromega.cmo contrib/micromega/g_micromega.cmo + +RINGCMO:=\ + contrib/ring/quote.cmo contrib/ring/g_quote.cmo \ + contrib/ring/ring.cmo contrib/ring/g_ring.cmo + +NEWRINGCMO:=\ + contrib/setoid_ring/newring.cmo + +DPCMO:=contrib/dp/dp_why.cmo contrib/dp/dp_zenon.cmo \ + contrib/dp/dp.cmo contrib/dp/dp_gappa.cmo contrib/dp/g_dp.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 contrib/xml/cic2Xml.cmo \ + contrib/xml/dumptree.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/extraction.cmo \ + contrib/extraction/common.cmo \ + contrib/extraction/ocaml.cmo \ + contrib/extraction/haskell.cmo \ + contrib/extraction/scheme.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/indfun_common.cmo contrib/funind/rawtermops.cmo \ + contrib/funind/recdef.cmo \ + contrib/funind/rawterm_to_relation.cmo \ + contrib/funind/functional_principles_proofs.cmo \ + contrib/funind/functional_principles_types.cmo \ + contrib/funind/invfun.cmo contrib/funind/indfun.cmo \ + contrib/funind/merge.cmo contrib/funind/g_indfun.cmo + +FOCMO:=\ + contrib/firstorder/formula.cmo contrib/firstorder/unify.cmo \ + contrib/firstorder/sequent.cmo contrib/firstorder/rules.cmo \ + contrib/firstorder/instances.cmo contrib/firstorder/ground.cmo \ + contrib/firstorder/g_ground.cmo + +CCCMO:=contrib/cc/ccalgo.cmo contrib/cc/ccproof.cmo contrib/cc/cctac.cmo \ + contrib/cc/g_congruence.cmo + +SUBTACCMO:=contrib/subtac/subtac_utils.cmo contrib/subtac/eterm.cmo \ + contrib/subtac/g_eterm.cmo \ + contrib/subtac/subtac_errors.cmo contrib/subtac/subtac_coercion.cmo \ + contrib/subtac/subtac_obligations.cmo contrib/subtac/subtac_cases.cmo \ + contrib/subtac/subtac_pretyping_F.cmo contrib/subtac/subtac_pretyping.cmo \ + contrib/subtac/subtac_command.cmo contrib/subtac/subtac_classes.cmo \ + contrib/subtac/subtac.cmo \ + contrib/subtac/g_subtac.cmo + +RTAUTOCMO:=contrib/rtauto/proof_search.cmo contrib/rtauto/refl_tauto.cmo \ + contrib/rtauto/g_rtauto.cmo + +CONTRIB:=$(OMEGACMO) $(ROMEGACMO) $(MICROMEGACMO) \ + $(RINGCMO) $(NEWRINGCMO) $(DPCMO) $(FIELDCMO) \ + $(FOURIERCMO) $(EXTRACTIONCMO) $(JPROVERCMO) $(XMLCMO) \ + $(CCCMO) $(FOCMO) $(SUBTACCMO) $(RTAUTOCMO) \ + $(FUNINDCMO) + +CMA:=$(CLIBS) $(CAMLP4OBJS) +CMXA:=$(CMA:.cma=.cmxa) + +# LINK ORDER: +# Beware that highparsing.cma should appear before hightactics.cma +# respecting this order is useful for developers that want to load or link +# the libraries directly + +LINKCMO:=$(CONFIG) lib/lib.cma kernel/kernel.cma library/library.cma \ + pretyping/pretyping.cma interp/interp.cma proofs/proofs.cma \ + parsing/parsing.cma tactics/tactics.cma toplevel/toplevel.cma \ + parsing/highparsing.cma tactics/hightactics.cma contrib/contrib.cma +LINKCMOCMXA:=$(LINKCMO:.cma=.cmxa) +LINKCMX:=$(LINKCMOCMXA:.cmo=.cmx) + +# objects known by the toplevel of Coq +OBJSCMO:=$(CONFIG) $(LIBREP) $(KERNEL) $(LIBRARY) $(PRETYPING) $(INTERP) \ + $(PROOFS) $(PARSING) $(TACTICS) $(TOPLEVEL) $(HIGHPARSING) \ + $(HIGHTACTICS) $(CONTRIB) + +COQIDECMO:=ide/utils/okey.cmo ide/utils/config_file.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) + +COQMKTOPCMO:=$(CONFIG) scripts/tolink.cmo scripts/coqmktop.cmo + +COQMKTOPCMX:=config/coq_config.cmx scripts/tolink.cmx scripts/coqmktop.cmx +COQCCMO:=$(CONFIG) toplevel/usage.cmo scripts/coqc.cmo +COQCCMX:=config/coq_config.cmx toplevel/usage.cmx scripts/coqc.cmx + +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/depends.cmo \ + contrib/interface/centaur.cmo + +INTERFACECMX:=$(INTERFACE:.cmo=.cmx) + +PARSERREQUIRES:=$(LINKCMO) $(LIBCOQRUN) # Solution de facilité... +PARSERREQUIRESCMX:=$(LINKCMX) + +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 + +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) + +INTERFACERC:= contrib/interface/vernacrc + +CSDPCERTCMO:= contrib/micromega/mutils.cmo contrib/micromega/micromega.cmo \ + contrib/micromega/vector.cmo contrib/micromega/mfourier.cmo \ + contrib/micromega/certificate.cmo \ + contrib/micromega/sos.cmo contrib/micromega/csdpcert.cmo +CSDPCERTCMX:= $(CSDPCERTCMO:.cmo=.cmx) + +DEBUGPRINTERS:=dev/top_printers.cmo dev/vm_printers.cmo dev/printers.cma + +COQDEPCMO:=config/coq_config.cmo tools/coqdep_lexer.cmo tools/coqdep.cmo +GALLINACMO:=tools/gallina_lexer.cmo tools/gallina.cmo +COQDOCCMO:=$(CONFIG) tools/coqdoc/cdglobals.cmo tools/coqdoc/alpha.cmo \ + tools/coqdoc/index.cmo tools/coqdoc/output.cmo \ + tools/coqdoc/pretty.cmo tools/coqdoc/main.cmo + + +# checker + +MCHECKER:=\ + config/coq_config.cmo \ + lib/pp_control.cmo lib/pp.cmo lib/compat.cmo \ + lib/util.cmo lib/option.cmo lib/hashcons.cmo \ + lib/system.cmo lib/flags.cmo \ + lib/predicate.cmo lib/rtree.cmo \ + kernel/names.cmo kernel/univ.cmo \ + kernel/esubst.cmo checker/term.cmo \ + checker/declarations.cmo checker/environ.cmo \ + checker/closure.cmo checker/reduction.cmo \ + checker/type_errors.cmo \ + checker/modops.cmo \ + checker/inductive.cmo checker/typeops.cmo \ + checker/indtypes.cmo checker/subtyping.cmo checker/mod_checking.cmo \ + checker/validate.cmo \ + checker/safe_typing.cmo checker/check.cmo \ + checker/check_stat.cmo checker/checker.cmo + +# minicoq + +MINICOQCMO:=$(CONFIG) $(LIBREP) $(KERNEL) \ + parsing/lexer.cmo parsing/g_minicoq.cmo \ + toplevel/fhimsg.cmo toplevel/minicoq.cmo + +# grammar modules with camlp4 + +GRAMMARNEEDEDCMO:=\ + lib/pp_control.cmo lib/pp.cmo lib/compat.cmo lib/util.cmo lib/bigint.cmo \ + lib/dyn.cmo lib/flags.cmo lib/hashcons.cmo lib/predicate.cmo \ + lib/rtree.cmo lib/option.cmo \ + kernel/names.cmo kernel/univ.cmo \ + kernel/esubst.cmo kernel/term.cmo kernel/mod_subst.cmo kernel/sign.cmo \ + kernel/cbytecodes.cmo kernel/copcodes.cmo kernel/cemitcodes.cmo \ + kernel/declarations.cmo \ + kernel/retroknowledge.cmo kernel/pre_env.cmo \ + kernel/cbytegen.cmo kernel/conv_oracle.cmo kernel/environ.cmo \ + kernel/closure.cmo kernel/reduction.cmo kernel/type_errors.cmo\ + kernel/entries.cmo \ + kernel/modops.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/nameops.cmo library/libnames.cmo library/summary.cmo \ + library/nametab.cmo library/libobject.cmo library/lib.cmo \ + library/goptions.cmo library/decl_kinds.cmo library/global.cmo \ + pretyping/termops.cmo pretyping/evd.cmo pretyping/reductionops.cmo \ + pretyping/inductiveops.cmo pretyping/rawterm.cmo pretyping/detyping.cmo \ + pretyping/pattern.cmo \ + interp/topconstr.cmo interp/genarg.cmo interp/ppextend.cmo \ + proofs/tacexpr.cmo \ + parsing/lexer.cmo parsing/extend.cmo \ + toplevel/vernacexpr.cmo parsing/pcoq.cmo parsing/q_util.cmo \ + parsing/q_coqast.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 + +GRAMMARCMO:=$(GRAMMARNEEDEDCMO) $(CAMLP4EXTENSIONSCMO) $(GRAMMARSCMO) + +GRAMMARCMA:=parsing/grammar.cma + +GRAMMARML4:=lib/compat.ml4 lib/pp.ml4 parsing/q_util.ml4 parsing/pcoq.ml4 \ + parsing/argextend.ml4 parsing/tacextend.ml4 parsing/vernacextend.ml4 \ + parsing/g_prim.ml4 parsing/g_tactic.ml4 \ + parsing/g_ltac.ml4 parsing/g_constr.ml4 \ + parsing/lexer.ml4 parsing/q_coqast.ml4 + +STAGE1_ML4:=$(GRAMMARML4) parsing/q_constr.ml4 +STAGE1_CMO:=$(GRAMMARCMO) parsing/q_constr.cmo +STAGE1:=parsing/grammar.cma parsing/q_constr.cmo + +PRINTERSCMO:=\ + config/coq_config.cmo lib/lib.cma \ + kernel/names.cmo kernel/univ.cmo kernel/esubst.cmo kernel/term.cmo \ + kernel/mod_subst.cmo kernel/copcodes.cmo kernel/cemitcodes.cmo \ + kernel/sign.cmo kernel/declarations.cmo kernel/retroknowledge.cmo \ + kernel/pre_env.cmo \ + kernel/retroknowledge.cmo kernel/pre_env.cmo \ + kernel/cbytecodes.cmo kernel/cbytegen.cmo kernel/environ.cmo \ + kernel/conv_oracle.cmo kernel/closure.cmo kernel/reduction.cmo \ + kernel/modops.cmo kernel/type_errors.cmo kernel/inductive.cmo \ + kernel/typeops.cmo kernel/subtyping.cmo kernel/indtypes.cmo \ + kernel/cooking.cmo \ + kernel/term_typing.cmo kernel/mod_typing.cmo kernel/safe_typing.cmo \ + library/summary.cmo library/global.cmo library/nameops.cmo \ + library/libnames.cmo library/nametab.cmo library/libobject.cmo \ + library/lib.cmo library/goptions.cmo library/decls.cmo library/heads.cmo \ + pretyping/termops.cmo pretyping/evd.cmo pretyping/rawterm.cmo \ + pretyping/reductionops.cmo pretyping/inductiveops.cmo \ + pretyping/retyping.cmo pretyping/cbv.cmo \ + pretyping/pretype_errors.cmo pretyping/recordops.cmo pretyping/typing.cmo \ + pretyping/evarutil.cmo pretyping/evarconv.cmo pretyping/tacred.cmo \ + pretyping/classops.cmo pretyping/typeclasses_errors.cmo pretyping/typeclasses.cmo \ + pretyping/detyping.cmo pretyping/indrec.cmo pretyping/coercion.cmo \ + pretyping/unification.cmo pretyping/cases.cmo \ + pretyping/pretyping.cmo pretyping/clenv.cmo pretyping/pattern.cmo \ + parsing/lexer.cmo interp/ppextend.cmo interp/genarg.cmo \ + interp/topconstr.cmo interp/notation.cmo interp/reserve.cmo \ + library/impargs.cmo interp/constrextern.cmo \ + interp/syntax_def.cmo interp/implicit_quantifiers.cmo interp/constrintern.cmo \ + proofs/proof_trees.cmo proofs/logic.cmo proofs/refiner.cmo \ + proofs/tacexpr.cmo \ + proofs/evar_refiner.cmo proofs/pfedit.cmo proofs/tactic_debug.cmo \ + proofs/decl_mode.cmo \ + parsing/ppconstr.cmo parsing/extend.cmo parsing/pcoq.cmo \ + parsing/printer.cmo parsing/pptactic.cmo \ + parsing/ppdecl_proof.cmo \ + parsing/tactic_printer.cmo \ + parsing/egrammar.cmo toplevel/himsg.cmo toplevel/cerrors.cmo \ + toplevel/vernacexpr.cmo toplevel/vernacinterp.cmo \ + dev/top_printers.cmo + +########################################################################### +# vo files +########################################################################### + +## Theories + +INITVO:=$(addprefix theories/Init/, \ + Notations.vo Datatypes.vo Peano.vo Logic.vo \ + Specif.vo Logic_Type.vo Wf.vo Tactics.vo \ + Prelude.vo ) + +LOGICVO:=$(addprefix theories/Logic/, \ + Hurkens.vo ProofIrrelevance.vo Classical.vo \ + Classical_Type.vo Classical_Pred_Set.vo Eqdep.vo \ + Classical_Prop.vo Classical_Pred_Type.vo ClassicalFacts.vo \ + ChoiceFacts.vo Berardi.vo Eqdep_dec.vo \ + Decidable.vo JMeq.vo ClassicalChoice.vo \ + ClassicalDescription.vo RelationalChoice.vo Diaconescu.vo \ + EqdepFacts.vo ProofIrrelevanceFacts.vo ClassicalEpsilon.vo \ + ClassicalUniqueChoice.vo DecidableType.vo DecidableTypeEx.vo \ + Epsilon.vo ConstructiveEpsilon.vo Description.vo \ + IndefiniteDescription.vo SetIsType.vo ) + +ARITHVO:=$(addprefix theories/Arith/, \ + Arith.vo Gt.vo Between.vo Le.vo \ + Compare.vo Lt.vo Compare_dec.vo Min.vo \ + Div2.vo Minus.vo Mult.vo Even.vo \ + EqNat.vo Peano_dec.vo Euclid.vo Plus.vo \ + Wf_nat.vo Max.vo Bool_nat.vo Factorial.vo \ + Arith_base.vo ) + +SORTINGVO:=$(addprefix theories/Sorting/, \ + Heap.vo Permutation.vo Sorting.vo PermutSetoid.vo \ + PermutEq.vo ) + +BOOLVO:=$(addprefix theories/Bool/, \ + Bool.vo IfProp.vo Zerob.vo DecBool.vo \ + Sumbool.vo BoolEq.vo Bvector.vo ) + +NARITHVO:=$(addprefix theories/NArith/, \ + BinPos.vo Pnat.vo BinNat.vo NArith.vo \ + Nnat.vo Ndigits.vo Ndec.vo Ndist.vo ) + +ZARITHVO:=$(addprefix theories/ZArith/, \ + BinInt.vo Wf_Z.vo ZArith.vo ZArith_dec.vo \ + auxiliary.vo Zmisc.vo Zcompare.vo Znat.vo \ + Zorder.vo Zabs.vo Zmin.vo Zmax.vo \ + Zminmax.vo Zeven.vo Zhints.vo Zlogarithm.vo \ + Zpower.vo Zcomplements.vo Zdiv.vo Zsqrt.vo \ + Zwf.vo ZArith_base.vo Zbool.vo Zbinary.vo \ + Znumtheory.vo Int.vo Zpow_def.vo Zpow_facts.vo \ + ZOdiv_def.vo ZOdiv.vo Zgcd_alt.vo ) + +QARITHVO:=$(addprefix theories/QArith/, \ + QArith_base.vo Qreduction.vo Qring.vo Qreals.vo \ + QArith.vo Qcanon.vo Qfield.vo Qpower.vo \ + Qabs.vo Qround.vo ) + +LISTSVO:=$(addprefix theories/Lists/, \ + MonoList.vo ListSet.vo Streams.vo StreamMemo.vo \ + TheoryList.vo List.vo SetoidList.vo ListTactics.vo ) + +STRINGSVO:=$(addprefix theories/Strings/, \ + Ascii.vo String.vo ) + +SETSVO:=$(addprefix theories/Sets/, \ + Classical_sets.vo Permut.vo \ + Constructive_sets.vo Powerset.vo \ + Cpo.vo Powerset_Classical_facts.vo \ + Ensembles.vo Powerset_facts.vo \ + Finite_sets.vo Relations_1.vo \ + Finite_sets_facts.vo Relations_1_facts.vo \ + Image.vo Relations_2.vo \ + Infinite_sets.vo Relations_2_facts.vo \ + Integers.vo Relations_3.vo \ + Multiset.vo Relations_3_facts.vo \ + Partial_Order.vo Uniset.vo ) + +FSETSBASEVO:=$(addprefix theories/FSets/, \ + OrderedType.vo OrderedTypeEx.vo OrderedTypeAlt.vo \ + FSetInterface.vo FSetList.vo FSetBridge.vo \ + FSetFacts.vo FSetProperties.vo FSetEqProperties.vo \ + FSetWeakList.vo FSetAVL.vo FSetDecide.vo \ + FSets.vo \ + FMapInterface.vo FMapList.vo FMapFacts.vo \ + FMapWeakList.vo FMapPositive.vo FSetToFiniteSet.vo \ + FMaps.vo ) + +FSETS_basic:= + +FSETS_all:=$(addprefix theories/FSets/, \ + FSetFullAVL.vo FMapAVL.vo FMapFullAVL.vo ) + +FSETSVO:=$(FSETSBASEVO) $(FSETS_$(FSETS)) + +ALLFSETS:=$(FSETSBASEVO) $(FSETS_all) + +RELATIONSVO:=$(addprefix theories/Relations/, \ + Newman.vo Operators_Properties.vo Relation_Definitions.vo \ + Relation_Operators.vo Relations.vo Rstar.vo ) + +WELLFOUNDEDVO:=$(addprefix theories/Wellfounded/, \ + Disjoint_Union.vo Inclusion.vo Inverse_Image.vo \ + Transitive_Closure.vo Union.vo Wellfounded.vo \ + Well_Ordering.vo Lexicographic_Product.vo \ + Lexicographic_Exponentiation.vo ) + +REALSBASEVO:=$(addprefix theories/Reals/, \ + Rdefinitions.vo Raxioms.vo RIneq.vo DiscrR.vo \ + Rbase.vo LegacyRfield.vo Rpow_def.vo ) + +REALS_basic:= + +REALS_all:=$(addprefix theories/Reals/, \ + R_Ifp.vo Rbasic_fun.vo R_sqr.vo SplitAbsolu.vo \ + SplitRmult.vo ArithProp.vo Rfunctions.vo Rseries.vo \ + SeqProp.vo Rcomplete.vo PartSum.vo AltSeries.vo \ + Binomial.vo Rsigma.vo Rprod.vo Cauchy_prod.vo \ + Alembert.vo SeqSeries.vo Rtrigo_fun.vo Rtrigo_def.vo \ + Rtrigo_alt.vo Cos_rel.vo Cos_plus.vo Rtrigo.vo \ + Rlimit.vo Rderiv.vo RList.vo Ranalysis1.vo \ + Ranalysis2.vo Ranalysis3.vo Rtopology.vo MVT.vo \ + PSeries_reg.vo Exp_prop.vo Rtrigo_reg.vo Rsqrt_def.vo \ + R_sqrt.vo Rtrigo_calc.vo Rgeom.vo Sqrt_reg.vo \ + Ranalysis4.vo Rpower.vo Ranalysis.vo NewtonInt.vo \ + RiemannInt_SF.vo RiemannInt.vo Integration.vo \ + Rlogic.vo Reals.vo ) + +REALSVO:=$(REALSBASEVO) $(REALS_$(REALS)) + +ALLREALS:=$(REALSBASEVO) $(REALS_all) + +NUMBERSCOMMONVO:=$(addprefix theories/Numbers/, \ + NaryFunctions.vo NumPrelude.vo BigNumPrelude.vo ) + +CYCLICABSTRACTVO:=$(addprefix theories/Numbers/Cyclic/Abstract/, \ + CyclicAxioms.vo NZCyclic.vo ) + +CYCLICINT31VO:=$(addprefix theories/Numbers/Cyclic/Int31/, \ + Int31.vo Cyclic31.vo ) + +CYCLICDOUBLECYCLICVO:=$(addprefix theories/Numbers/Cyclic/DoubleCyclic/, \ + DoubleType.vo DoubleBase.vo DoubleAdd.vo DoubleSub.vo \ + DoubleMul.vo DoubleDivn1.vo DoubleDiv.vo DoubleSqrt.vo \ + DoubleLift.vo DoubleCyclic.vo ) + +CYCLICZMODULOVO := $(addprefix theories/Numbers/Cyclic/ZModulo/, \ + ZModulo.vo ) + +CYCLICVO:=$(CYCLICABSTRACTVO) $(CYCLICINT31VO) $(CYCLICDOUBLECYCLICVO) \ + $(CYCLICZMODULOVO) + +NATINTVO:=$(addprefix theories/Numbers/NatInt/, \ + NZAxioms.vo NZBase.vo NZAdd.vo NZMul.vo \ + NZOrder.vo NZAddOrder.vo NZMulOrder.vo ) + +NATURALABSTRACTVO:=$(addprefix theories/Numbers/Natural/Abstract/, \ + NAxioms.vo NBase.vo NAdd.vo NMul.vo \ + NOrder.vo NAddOrder.vo NMulOrder.vo NSub.vo \ + NIso.vo ) + +NATURALPEANOVO:=$(addprefix theories/Numbers/Natural/Peano/, \ + NPeano.vo ) + +NATURALBINARYVO:=$(addprefix theories/Numbers/Natural/Binary/, \ + NBinDefs.vo NBinary.vo ) + +NATURALSPECVIAZVO:=$(addprefix theories/Numbers/Natural/SpecViaZ/, \ + NSig.vo NSigNAxioms.vo ) + +NATURALBIGNVO:=$(addprefix theories/Numbers/Natural/BigN/, \ + Nbasic.vo NMake.vo BigN.vo ) + +NATURALVO:=$(NATURALABSTRACTVO) $(NATURALPEANOVO) $(NATURALBINARYVO) \ + $(NATURALSPECVIAZVO) $(NATURALBIGNVO) + +INTEGERABSTRACTVO:=$(addprefix theories/Numbers/Integer/Abstract/, \ + ZAxioms.vo ZBase.vo ZAdd.vo ZMul.vo \ + ZLt.vo ZAddOrder.vo ZMulOrder.vo ) + +INTEGERBINARYVO:=$(addprefix theories/Numbers/Integer/Binary/, \ + ZBinary.vo ) + +INTEGERNATPAIRSVO:=$(addprefix theories/Numbers/Integer/NatPairs/, \ + ZNatPairs.vo ) + +INTEGERSPECVIAZVO:=$(addprefix theories/Numbers/Integer/SpecViaZ/, \ + ZSig.vo ZSigZAxioms.vo ) + +INTEGERBIGZVO:=$(addprefix theories/Numbers/Integer/BigZ/, \ + ZMake.vo BigZ.vo ) + +INTEGERVO:=$(INTEGERABSTRACTVO) $(INTEGERBINARYVO) $(INTEGERNATPAIRSVO) \ + $(INTEGERSPECVIAZVO) $(INTEGERBIGZVO) + +RATIONALSPECVIAQVO:=$(addprefix theories/Numbers/Rational/SpecViaQ/, \ + QSig.vo ) + +RATIONALBIGQVO:=$(addprefix theories/Numbers/Rational/BigQ/, \ + QMake_base.vo QpMake.vo QvMake.vo Q0Make.vo \ + QifMake.vo QbiMake.vo BigQ.vo ) + +RATIONALVO:=$(RATIONALSPECVIAQVO) $(RATIONALBIGQVO) + +NUMBERSVO:= $(NUMBERSCOMMONVO) $(NATURALVO) $(INTEGERVO) $(NATINTVO) $(CYCLICVO) $(RATIONALVO) + +SETOIDSVO:=$(addprefix theories/Setoids/, \ + Setoid.vo ) + +UNICODEVO:=$(addprefix theories/Unicode/, \ + Utf8.vo ) + +CLASSESVO:=$(addprefix theories/Classes/, \ + Init.vo RelationClasses.vo Morphisms.vo Morphisms_Prop.vo \ + Morphisms_Relations.vo Functions.vo Equivalence.vo SetoidTactics.vo \ + SetoidClass.vo SetoidAxioms.vo EquivDec.vo SetoidDec.vo ) + +PROGRAMVO:=$(addprefix theories/Program/, \ + Tactics.vo Equality.vo Subset.vo Utils.vo \ + Wf.vo Basics.vo FunctionalExtensionality.vo \ + Combinators.vo Syntax.vo Program.vo ) + +THEORIESVO:=\ + $(INITVO) $(LOGICVO) $(ARITHVO) $(BOOLVO) $(NARITHVO) $(ZARITHVO) \ + $(SETOIDSVO) $(LISTSVO) $(STRINGSVO) $(SETSVO) $(FSETSVO) \ + $(RELATIONSVO) $(WELLFOUNDEDVO) $(REALSVO) $(SORTINGVO) $(QARITHVO) \ + $(NUMBERSVO) $(UNICODEVO) $(CLASSESVO) $(PROGRAMVO) + +THEORIESLIGHTVO:= $(INITVO) $(LOGICVO) $(ARITHVO) + +## Contribs + +OMEGAVO:=$(addprefix contrib/omega/, \ + PreOmega.vo OmegaLemmas.vo Omega.vo ) + +ROMEGAVO:=$(addprefix contrib/romega/, \ + ReflOmegaCore.vo ROmega.vo ) + +MICROMEGAVO:=$(addprefix contrib/micromega/, \ + CheckerMaker.vo Refl.vo \ + Env.vo RingMicromega.vo \ + EnvRing.vo VarMap.vo \ + OrderedRing.vo ZCoeff.vo \ + Micromegatac.vo ZMicromega.vo \ + QMicromega.vo RMicromega.vo \ + Tauto.vo ) + +RINGVO:=$(addprefix contrib/ring/, \ + LegacyArithRing.vo Ring_normalize.vo \ + LegacyRing_theory.vo LegacyRing.vo \ + LegacyNArithRing.vo \ + LegacyZArithRing.vo Ring_abstract.vo \ + Quote.vo Setoid_ring_normalize.vo \ + Setoid_ring.vo Setoid_ring_theory.vo ) + +FIELDVO:=$(addprefix contrib/field/, \ + LegacyField_Compl.vo LegacyField_Theory.vo \ + LegacyField_Tactic.vo LegacyField.vo ) + +NEWRINGVO:=$(addprefix contrib/setoid_ring/, \ + BinList.vo Ring_theory.vo \ + Ring_polynom.vo Ring_tac.vo \ + Ring_base.vo InitialRing.vo \ + Ring_equiv.vo Ring.vo \ + ArithRing.vo NArithRing.vo \ + ZArithRing.vo \ + Field_theory.vo Field_tac.vo \ + Field.vo RealField.vo ) + +XMLVO:= + +FOURIERVO:=$(addprefix contrib/fourier/, \ + Fourier_util.vo Fourier.vo ) + +FUNINDVO:= + +RECDEFVO:=$(addprefix contrib/funind/, \ + Recdef.vo ) + +JPROVERVO:= + +CCVO:= + +DPVO:=$(addprefix contrib/dp/, \ + Dp.vo ) + +RTAUTOVO:=$(addprefix contrib/rtauto/, \ + Bintree.vo Rtauto.vo ) + +CONTRIBVO:= $(OMEGAVO) $(ROMEGAVO) $(MICROMEGAVO) $(RINGVO) $(FIELDVO) \ + $(XMLVO) $(FOURIERVO) $(JPROVERVO) $(CCVO) $(FUNINDVO) \ + $(RTAUTOVO) $(RECDEFVO) $(NEWRINGVO) $(DPVO) + +ALLVO:= $(INITVO) $(THEORIESVO) $(CONTRIBVO) +VFILES:= $(ALLVO:.vo=.v) + +LIBFILES:=$(THEORIESVO) $(CONTRIBVO) +LIBFILESLIGHT:=$(THEORIESLIGHTVO) + +## Specials + +INTERFACEVO:= + + +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 + +PCOQMANPAGES:=man/coq-interface.1 man/parser.1 + +RECTYPESML:=kernel/term.ml library/nametab.ml proofs/tacexpr.ml \ + parsing/pptactic.ml + + +######################################################### +# .mli files by directory (used for dependencies graphs # +######################################################### + +# We use wildcard to get rid of .cmo that do not have a .mli +KERNELMLI:=$(wildcard $(KERNEL:.cmo=.mli)) +INTERPMLI:=$(wildcard $(INTERP:.cmo=.mli)) +PRETYPINGMLI:=$(wildcard $(PRETYPING:.cmo=.mli)) +TOPLEVELMLI:=$(wildcard $(TOPLEVEL:.cmo=.mli)) +PROOFSMLI:=$(wildcard $(PROOFS:.cmo=.mli)) +LIBRARYMLI:=$(wildcard $(LIBRARY:.cmo=.mli)) +PARSINGMLI:=$(wildcard $(PARSING:.cmo=.mli) $(HIGHPARSING:.cmo=.mli)) +TACTICSMLI:=$(wildcard $(TACTICS:.cmo=.mli) $(HIGHTACTICS:.cmo=.mli)) +COQMLI:=$(KERNELMLI) $(INTERPMLI) $(PRETYPINGMLI) $(TOPLEVELMLI) $(PROOFSMLI) \ + $(LIBRARYMLI) $(PARSINGMLI) $(TACTICSMLI) + + +########################################################################### +# Miscellaneous +########################################################################### + +SOURCEDOCDIR=dev/source-doc + +## Targets forwarded by Makefile to a specific stage +STAGE1_TARGETS:= $(STAGE1) \ + $(filter-out parsing/q_constr.cmo,$(STAGE1_CMO)) \ + $(STAGE1_CMO:.cmo=.cmi) $(STAGE1_CMO:.cmo=.cmx) $(GENFILES) \ + source-doc revision toplevel/mltop.byteml toplevel/mltop.optml \ + $(STAGE1_ML4:.ml4=.ml4.preprocessed) +STAGE2_TARGETS:=$(COQBINARIES) lib kernel byterun library proofs tactics \ + interp parsing pretyping highparsing toplevel hightactics \ + coqide-binaries coqide-byte coqide-opt $(COQIDEOPT) $(COQIDEBYTE) $(COQIDE) \ + pcoq-binaries $(COQINTERFACE) $(CSDPCERT) coqbinaries pcoq $(TOOLS) tools \ + printers $(MINICOQ) debug +VO_TARGETS:=logic arith bool narith zarith qarith lists strings sets \ + fsets allfsets relations wellfounded ints reals allreals \ + setoids sorting natural integer rational numbers noreal \ + omega micromega ring setoid_ring dp xml extraction field fourier jprover \ + funind cc programs subtac rtauto +DOC_TARGETS:=doc doc-html doc-ps doc-pdf stdlib refman tutorial faq rectutorial +STAGE3_TARGETS:=world install coqide coqide-files coq coqlib \ + coqlight states pcoq-files check init theories theories-light contrib \ + $(DOC_TARGETS) $(VO_TARGETS) + + +# For emacs: +# Local Variables: +# mode: makefile +# End: |