diff options
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 1843 |
1 files changed, 148 insertions, 1695 deletions
@@ -6,7 +6,7 @@ # # GNU Lesser General Public License Version 2.1 # ####################################################################### -# $Id: Makefile 10314 2007-11-12 15:10:25Z notin $ +# $Id: Makefile 11029 2008-06-01 19:39:44Z herbelin $ # Makefile for Coq @@ -24,12 +24,37 @@ # by Emacs' next-error. ########################################################################### -include config/Makefile +FIND_VCS_CLAUSE:='(' -name '{arch}' -or -name '.svn' -or -name '_darcs' -or -name '.git' -or -name "$${GIT_DIR}" ')' -prune -or +FIND_PRINTF_P:=-print | sed 's|^\./||' -.PHONY: NOARG +export YACCFILES:=$(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.mly' ')' $(FIND_PRINTF_P)) +export LEXFILES := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.mll' ')' $(FIND_PRINTF_P)) +export GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) \ + scripts/tolink.ml kernel/copcodes.ml +export GENMLIFILES:=$(YACCFILES:.mly=.mli) +export GENHFILES:=kernel/byterun/coq_jumptbl.h +export GENVFILES:=theories/Numbers/Natural/BigN/NMake.v +export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) $(GENVFILES) +export MLFILES := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.ml' ')' $(FIND_PRINTF_P) | \ + while read f; do if ! [ -e "$${f}4" ]; then echo "$$f"; fi; done) \ + $(GENMLFILES) +export MLIFILES := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.mli' ')' $(FIND_PRINTF_P)) \ + $(GENMLIFILES) +export ML4FILES := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.ml4' ')' $(FIND_PRINTF_P)) +#export VFILES := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.v' ')' $(FIND_PRINTF_P)) \ +# $(GENVFILES) +export CFILES := $(shell find kernel/byterun -name '*.c') + +export ML4FILESML:= $(ML4FILES:.ml4=.ml) + +include Makefile.common NOARG: world +.PHONY: NOARG help always tags otags + +always: ; + help: @echo "Please use either" @echo " ./configure" @@ -40,1330 +65,156 @@ help: @echo @echo "For make to be verbose, add VERBOSE=1" - -# build and install the three subsystems: coq, coqide, pcoq -world: depend dependcoq - $(MAKE) worldnodep - -worldnodep: revision coq coqide pcoq - -install: install-coq 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 = @ +ifdef COQ_CONFIGURED +define stage-template + @echo '*****************************************************' + @echo '*****************************************************' + @echo '****************** Entering stage$(1) ******************' + @echo '*****************************************************' + @echo '*****************************************************' + +$(MAKE) -f Makefile.stage$(1) "$@" +endef +else +define stage-template + @echo "Please run ./configure first" >&2; exit 1 +endef endif -LOCALINCLUDES=-I config -I tools -I tools/coqdoc \ - -I scripts -I lib -I kernel -I kernel/byterun -I library \ - -I proofs -I tactics -I pretyping \ - -I interp -I toplevel -I parsing -I ide/utils -I ide \ - -I contrib/omega -I contrib/romega \ - -I contrib/ring -I contrib/dp -I contrib/setoid_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 -I contrib/subtac -I contrib/rtauto \ - -I contrib/recdef - -MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB) $(COQIDEINCLUDES) - -OCAMLC += $(CAMLFLAGS) -OCAMLOPT += $(CAMLFLAGS) - -BYTEFLAGS=$(MLINCLUDES) $(CAMLDEBUG) $(USERFLAGS) -OPTFLAGS=$(MLINCLUDES) $(CAMLTIMEPROF) $(INLINEFLAG) $(USERFLAGS) -DEPFLAGS= -slash $(LOCALINCLUDES) - -OCAMLC_P4O=$(OCAMLC) -pp $(CAMLP4O) $(BYTEFLAGS) -OCAMLOPT_P4O=$(OCAMLOPT) -pp $(CAMLP4O) $(OPTFLAGS) -CAMLP4EXTENSIONS=-I . pa_extend.cmo pa_extend_m.cmo q_MLast.cmo pa_macro.cmo -CAMLP4OPTIONS=$(CAMLP4COMPAT) -D$(CAMLVERSION) -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 -VM= # is "-no-vm" to not use the vm" -UNBOXEDVALUES= # is "-unboxed-values" to use unboxed values -COQOPTS=$(GLOB) $(COQ_XML) $(VM) $(UNBOXEDVALUES) -TIME= # is "'time -p'" to get compilation time of .v - -BOOTCOQTOP= $(TIME) $(BESTCOQTOP) -boot $(COQOPTS) - -########################################################################### -# Objects 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/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 - -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/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 - -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/unification.cmo pretyping/evarconv.cmo \ - pretyping/classops.cmo pretyping/coercion.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/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 - -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 \ - 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/command.cmo toplevel/record.cmo \ - parsing/ppvernac.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 - -SPECTAC= tactics/tauto.ml4 tactics/eqdecide.ml4 -USERTAC = $(SPECTAC) -ML4FILES += $(USERTAC) tactics/extraargs.ml4 tactics/extratactics.ml4 \ - tactics/eauto.ml4 toplevel/whelp.ml4 tactics/hipattern.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/dp/g_dp.ml4 \ - contrib/setoid_ring/newring.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/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 - -NEWRINGCMO=\ - contrib/setoid_ring/newring.cmo - -DPCMO=contrib/dp/dp_why.cmo contrib/dp/dp.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 - -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 \ - contrib/funind/indfun_common.cmo contrib/funind/rawtermops.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/indfun_main.cmo - -RECDEFCMO=\ - contrib/recdef/recdef.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 \ - 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.cmo \ - contrib/subtac/g_subtac.cmo - - -RTAUTOCMO=contrib/rtauto/proof_search.cmo contrib/rtauto/refl_tauto.cmo \ - contrib/rtauto/g_rtauto.cmo - -ML4FILES += contrib/jprover/jprover.ml4 contrib/cc/g_congruence.ml4 \ - contrib/funind/tacinv.ml4 contrib/first-order/g_ground.ml4 \ - contrib/subtac/g_subtac.ml4 contrib/subtac/g_eterm.ml4 \ - contrib/rtauto/g_rtauto.ml4 contrib/recdef/recdef.ml4 \ - contrib/funind/indfun_main.ml4 - - -CONTRIB=$(OMEGACMO) $(ROMEGACMO) $(RINGCMO) $(NEWRINGCMO) $(DPCMO) $(FIELDCMO) \ - $(FOURIERCMO) $(EXTRACTIONCMO) $(JPROVERCMO) $(XMLCMO) \ - $(CCCMO) $(FOCMO) $(SUBTACCMO) $(RTAUTOCMO) \ - $(RECDEFCMO) $(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) $(USERTACMO) $(CONTRIB) - -########################################################################### -# Compilation option for .c files -########################################################################### - -CINCLUDES= -I $(CAMLHLIB) - -# libcoqrun.a - -$(LIBCOQRUN): kernel/byterun/coq_jumptbl.h $(BYTERUN) - $(AR) rc $(LIBCOQRUN) $(BYTERUN) - $(RANLIB) $(LIBCOQRUN) - -#coq_jumptbl.h is required only if you have GCC 2.0 or later -kernel/byterun/coq_jumptbl.h : kernel/byterun/coq_instruct.h - sed -n -e '/^ /s/ \([A-Z]\)/ \&\&coq_lbl_\1/gp' \ - -e '/^}/q' kernel/byterun/coq_instruct.h > \ - kernel/byterun/coq_jumptbl.h - - -kernel/copcodes.ml: kernel/byterun/coq_instruct.h - sed -n -e '/^enum/p' -e 's/,//g' -e '/^ /p' \ - kernel/byterun/coq_instruct.h | \ - awk -f kernel/make-opcodes > kernel/copcodes.ml - -BEFOREDEPEND+= kernel/byterun/coq_jumptbl.h kernel/copcodes.ml - -clean :: - rm -f kernel/byterun/coq_jumptbl.h kernel/copcodes.ml - -########################################################################### -# Main targets (coqmktop, coqtop.opt, coqtop.byte) -########################################################################### - -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) - -COQBINARIES= $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(BESTCOQTOP) $(COQTOP) - -coqbinaries:: ${COQBINARIES} - -coq: coqlib tools coqbinaries - -coqlib:: theories contrib - -coqlight: theories-light tools coqbinaries - -states:: states/initial.coq - -$(COQTOPOPT): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN) $(USERTACCMX) - $(SHOW)'COQMKTOP -o $@' - $(HIDE)$(COQMKTOP) -opt $(OPTFLAGS) -o $@ - $(STRIP) $@ - -$(COQTOPBYTE): $(COQMKTOP) $(LINKCMO) $(LIBCOQRUN) $(USERTACCMO) - $(SHOW)'COQMKTOP -o $@' - $(HIDE)$(COQMKTOP) -top $(BYTEFLAGS) -o $@ - -$(COQTOP): - cd bin; ln -sf coqtop.$(BEST)$(EXE) coqtop$(EXE) - -# coqmktop - -COQMKTOPCMO=$(CONFIG) scripts/tolink.cmo scripts/coqmktop.cmo -COQMKTOPCMX=config/coq_config.cmx scripts/tolink.cmx scripts/coqmktop.cmx - -$(COQMKTOPBYTE): $(COQMKTOPCMO) - $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma unix.cma \ - $(COQMKTOPCMO) $(OSDEPLIBS) - -$(COQMKTOPOPT): $(COQMKTOPCMX) - $(SHOW)'OCAMLOPT -o $@' - $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -o $@ str.cmxa unix.cmxa \ - $(COQMKTOPCMX) $(OSDEPLIBS) - -$(COQMKTOP): $(BESTCOQMKTOP) - cd bin; ln -sf coqmktop.$(BEST)$(EXE) coqmktop$(EXE) - - -scripts/tolink.ml: Makefile - $(SHOW)"ECHO... >" $@ - $(HIDE)echo "let copts = \"-cclib -lcoqrun\"" > $@ - $(HIDE)echo "let core_libs = \""$(LINKCMO)"\"" >> $@ - $(HIDE)echo "let core_objs = \""$(OBJSCMO)"\"" >> $@ - $(HIDE)echo "let ide = \""$(COQIDECMO)"\"" >> $@ - -BEFOREDEPEND+= scripts/tolink.ml - -# coqc - -COQCCMO=$(CONFIG) toplevel/usage.cmo scripts/coqc.cmo -COQCCMX=config/coq_config.cmx toplevel/usage.cmx scripts/coqc.cmx - -$(COQCBYTE): $(COQCCMO) $(COQTOPBYTE) $(BESTCOQTOP) - $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ unix.cma $(COQCCMO) $(OSDEPLIBS) - -$(COQCOPT): $(COQCCMX) $(COQTOPOPT) $(BESTCOQTOP) - $(SHOW)'OCAMLOPT -o $@' - $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -o $@ unix.cmxa $(COQCCMX) $(OSDEPLIBS) - -$(COQC): $(BESTCOQC) - cd bin; ln -sf coqc.$(BEST)$(EXE) coqc$(EXE) - - -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) -byterun: $(BYTERUN) -library: $(LIBRARY) -proofs: $(PROOFS) -tactics: $(TACTICS) -interp: $(INTERP) -parsing: $(PARSING) -pretyping: $(PRETYPING) -highparsing: $(HIGHPARSING) -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) - -########################################################################### -# 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/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) -COQIDEFLAGS=-thread $(COQIDEINCLUDES) -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) $(LINKCMX) $(LIBCOQRUN) $(USERTACCMX) ide/ide.cmxa - $(SHOW)'COQMKTOP -o $@' - $(HIDE)$(COQMKTOP) -ide -opt $(OPTFLAGS) -o $@ - $(STRIP) $@ - -$(COQIDEBYTE): $(COQMKTOP) $(LINKCMO) $(LIBCOQRUN) $(USERTACCMO) ide/ide.cma - $(SHOW)'COQMKTOP -o $@' - $(HIDE)$(COQMKTOP) -g -ide -top $(BYTEFLAGS) -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) +UNSAVED_FILES:=$(shell find . -name '.\#*v' -o -name '.\#*.ml' -o -name '.\#*.mli' -o -name '.\#*.ml4') +ifdef UNSAVED_FILES +$(error You have unsaved changes in your editor (emacs?) [$(UNSAVED_FILES)]; cancel them or save before proceeding. \ +Or your editor crashed. Then, you may want to consider whether you want to restore the autosaves) +#If you try to simply remove this explicit test, the compilation may +#fail later. In particular, if a .#*.v file exists, coqdep fails to +#run. +endif -install-ide-info: - $(MKDIR) $(FULLIDELIB) - cp ide/FAQ $(FULLIDELIB) +ifdef GOTO_STAGE +config/Makefile Makefile.common Makefile.build Makefile: ; -########################################################################### -# Pcoq: special binaries for debugging (coq-interface, parser) -########################################################################### +%: always + $(call stage-template,$(GOTO_STAGE)) +else -# target to build Pcoq -pcoq: pcoq-binaries pcoq-files +.PHONY: stage1 stage2 stage3 world revision -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 +# This is to remove the built-in rule "%: %.o" +# Otherwise, "make foo" recurses into stage1, trying to build foo.o . +%: %.o -INTERFACECMX=$(INTERFACE:.cmo=.cmx) +%.o: always + $(call stage-template,1) -ML4FILES += contrib/interface/debug_tac.ml4 contrib/interface/centaur.ml4 +#STAGE1_TARGETS includes all object files necessary for $(STAGE1) +stage1 $(STAGE1_TARGETS): always + $(call stage-template,1) -PARSERREQUIRES=$(LINKCMO) $(LIBCOQRUN) # Solution de facilité... -PARSERREQUIRESCMX=$(LINKCMX) +CAML_OBJECT_PATTERNS:=%.cmo %.cmx %.cmi %.cma %.cmxa %.dep.ps %.dot +ifdef CM_STAGE1 +$(CAML_OBJECT_PATTERNS): always + $(call stage-template,1) -ifeq ($(BEST),opt) - COQINTERFACE=bin/coq-interface$(EXE) bin/coq-interface.opt$(EXE) bin/parser$(EXE) bin/parser.opt$(EXE) +%.ml4-preprocessed: stage1 + $(call stage-template,2) else - COQINTERFACE=bin/coq-interface$(EXE) bin/parser$(EXE) +$(CAML_OBJECT_PATTERNS) %.ml4-preprocessed: stage1 + $(call stage-template,2) endif -pcoq-binaries:: $(COQINTERFACE) - -bin/coq-interface$(EXE): $(COQMKTOP) $(LINKCMO) $(LIBCOQRUN) $(USERTACCMO) $(INTERFACE) - $(SHOW)'COQMKTOP -o $@' - $(HIDE)$(COQMKTOP) -top $(BYTEFLAGS) -o $@ $(INTERFACE) - -bin/coq-interface.opt$(EXE): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN) $(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):$(LIBCOQRUN) $(PARSERCMO) - $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) -custom -linkall $(BYTEFLAGS) -o $@ \ - dynlink.cma $(LIBCOQRUN) $(CMA) $(PARSERCMO) - -bin/parser.opt$(EXE): $(LIBCOQRUN) $(PARSERCMX) - $(SHOW)'OCAMLOPT -o $@' - $(HIDE)$(OCAMLOPT) -linkall $(OPTFLAGS) -o $@ \ - $(LIBCOQRUN) $(CMXA) $(PARSERCMX) - -INTERFACEVO= - -INTERFACERC= contrib/interface/vernacrc - -pcoq-files:: $(INTERFACEVO) $(INTERFACERC) - -clean:: - rm -f bin/parser$(EXE) bin/parser.opt$(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 +stage2 $(STAGE2_TARGETS): stage1 + $(call stage-template,2) -install-pcoq-manpages: - $(MKDIR) $(FULLMANDIR)/man1 - cp $(PCOQMANPAGES) $(FULLMANDIR)/man1 +%.vo %.glob states/% install-%: stage2 + $(call stage-template,3) -########################################################################### -# tests -########################################################################### +stage3 $(STAGE3_TARGETS): stage2 + $(call stage-template,3) -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 +endif #GOTO_STAGE ########################################################################### -# 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/Tactics.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_Prop.vo theories/Logic/Classical_Pred_Type.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/ClassicalChoice.vo theories/Logic/ClassicalDescription.vo \ - theories/Logic/RelationalChoice.vo theories/Logic/Diaconescu.vo \ - theories/Logic/EqdepFacts.vo theories/Logic/ProofIrrelevanceFacts.vo \ - theories/Logic/ClassicalEpsilon.vo theories/Logic/ClassicalUniqueChoice.vo \ - theories/Logic/DecidableType.vo theories/Logic/DecidableTypeEx.vo \ - theories/Logic/ConstructiveEpsilon.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/Arith_base.vo - -SORTINGVO=\ - theories/Sorting/Heap.vo theories/Sorting/Permutation.vo \ - theories/Sorting/Sorting.vo theories/Sorting/PermutSetoid.vo \ - theories/Sorting/PermutEq.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 \ - theories/NArith/Nnat.vo theories/NArith/Ndigits.vo \ - theories/NArith/Ndec.vo theories/NArith/Ndist.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/Zmax.vo \ - theories/ZArith/Zminmax.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 theories/ZArith/Int.vo \ - theories/ZArith/Zpow_def.vo - -QARITHVO=\ - theories/QArith/QArith_base.vo theories/QArith/Qreduction.vo \ - theories/QArith/Qring.vo theories/QArith/Qreals.vo \ - theories/QArith/QArith.vo theories/QArith/Qcanon.vo - -LISTSVO=\ - theories/Lists/MonoList.vo \ - theories/Lists/ListSet.vo theories/Lists/Streams.vo \ - theories/Lists/TheoryList.vo theories/Lists/List.vo \ - theories/Lists/SetoidList.vo theories/Lists/ListTactics.vo - -STRINGSVO=\ - theories/Strings/Ascii.vo theories/Strings/String.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 - -FSETSBASEVO=\ - theories/FSets/OrderedType.vo \ - theories/FSets/OrderedTypeEx.vo theories/FSets/OrderedTypeAlt.vo \ - theories/FSets/FSetInterface.vo theories/FSets/FSetList.vo \ - theories/FSets/FSetBridge.vo theories/FSets/FSetFacts.vo \ - theories/FSets/FSetProperties.vo theories/FSets/FSetEqProperties.vo \ - theories/FSets/FSets.vo theories/FSets/FSetWeakProperties.vo \ - theories/FSets/FSetWeakInterface.vo theories/FSets/FSetWeakList.vo \ - theories/FSets/FSetWeakFacts.vo theories/FSets/FSetWeak.vo \ - theories/FSets/FMapInterface.vo theories/FSets/FMapList.vo \ - theories/FSets/FMaps.vo theories/FSets/FMapFacts.vo \ - theories/FSets/FMapWeakFacts.vo \ - theories/FSets/FMapWeakInterface.vo theories/FSets/FMapWeakList.vo \ - theories/FSets/FMapWeak.vo theories/FSets/FMapPositive.vo \ - theories/FSets/FMapIntMap.vo theories/FSets/FSetToFiniteSet.vo - -FSETS_basic= - -FSETS_all=\ - theories/FSets/FMapAVL.vo theories/FSets/FSetAVL.vo \ - -FSETSVO=$(FSETSBASEVO) $(FSETS_$(FSETS)) - -ALLFSETS=$(FSETSBASEVO) $(FSETS_all) - -INTMAPVO=\ - theories/IntMap/Adalloc.vo theories/IntMap/Mapcanon.vo \ - theories/IntMap/Mapfold.vo \ - theories/IntMap/Mapcard.vo theories/IntMap/Mapc.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/Rpow_def.vo \ - theories/Reals/Raxioms.vo theories/Reals/RIneq.vo \ - theories/Reals/DiscrR.vo theories/Reals/Rbase.vo \ - theories/Reals/LegacyRfield.vo - -REALS_basic= - -REALS_all=\ - theories/Reals/R_Ifp.vo theories/Reals/Rpow_def.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) - -SETOIDSVO=theories/Setoids/Setoid.vo - -THEORIESVO =\ - $(INITVO) $(LOGICVO) $(ARITHVO) $(BOOLVO) $(NARITHVO) $(ZARITHVO) \ - $(SETOIDSVO) $(LISTSVO) $(STRINGSVO) $(SETSVO) $(FSETSVO) $(INTMAPVO) \ - $(RELATIONSVO) $(WELLFOUNDEDVO) $(REALSVO) $(SORTINGVO) $(QARITHVO) - -THEORIESLIGHTVO = $(INITVO) $(LOGICVO) $(ARITHVO) - -theories: $(THEORIESVO) -theories-light: $(THEORIESLIGHTVO) - -logic: $(LOGICVO) -arith: $(ARITHVO) -bool: $(BOOLVO) -narith: $(NARITHVO) -zarith: $(ZARITHVO) -qarith: $(QARITHVO) -lists: $(LISTSVO) -strings: $(STRINGSVO) -sets: $(SETSVO) -fsets: $(FSETSVO) -allfsets: $(ALLFSETS) -intmap: $(INTMAPVO) -relations: $(RELATIONSVO) -wellfounded: $(WELLFOUNDEDVO) -# reals -reals: $(REALSVO) -allreals: $(ALLREALS) -setoids: $(SETOIDSVO) -sorting: $(SORTINGVO) - -noreal: logic arith bool zarith qarith lists sets fsets 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/LegacyArithRing.vo contrib/ring/Ring_normalize.vo \ - contrib/ring/LegacyRing_theory.vo contrib/ring/LegacyRing.vo \ - contrib/ring/LegacyNArithRing.vo \ - contrib/ring/LegacyZArithRing.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/LegacyField_Compl.vo contrib/field/LegacyField_Theory.vo \ - contrib/field/LegacyField_Tactic.vo contrib/field/LegacyField.vo - -NEWRINGVO=\ - contrib/setoid_ring/BinList.vo contrib/setoid_ring/Ring_theory.vo \ - contrib/setoid_ring/Ring_polynom.vo contrib/setoid_ring/Ring_tac.vo \ - contrib/setoid_ring/Ring_base.vo contrib/setoid_ring/InitialRing.vo \ - contrib/setoid_ring/Ring_equiv.vo contrib/setoid_ring/Ring.vo \ - contrib/setoid_ring/ArithRing.vo contrib/setoid_ring/NArithRing.vo \ - contrib/setoid_ring/ZArithRing.vo \ - contrib/setoid_ring/Field_theory.vo contrib/setoid_ring/Field_tac.vo \ - contrib/setoid_ring/Field.vo contrib/setoid_ring/RealField.vo - -XMLVO= - -FOURIERVO=\ - contrib/fourier/Fourier_util.vo contrib/fourier/Fourier.vo - -FUNINDVO= - -RECDEFVO=contrib/recdef/Recdef.vo - -JPROVERVO= - -CCVO= - -SUBTACVO=contrib/subtac/SubtacTactics.vo contrib/subtac/Heq.vo \ - contrib/subtac/Utils.vo contrib/subtac/FixSub.vo contrib/subtac/Subtac.vo \ - contrib/subtac/FunctionalExtensionality.vo - -RTAUTOVO = \ - contrib/rtauto/Bintree.vo contrib/rtauto/Rtauto.vo - -CONTRIBVO = $(OMEGAVO) $(ROMEGAVO) $(RINGVO) $(FIELDVO) $(XMLVO) \ - $(FOURIERVO) $(JPROVERVO) $(CCVO) $(FUNINDVO) $(SUBTACVO) \ - $(RTAUTOVO) $(RECDEFVO) $(NEWRINGVO) - -$(CONTRIBVO): states/initial.coq - -contrib: $(CONTRIBVO) $(CONTRIBCMO) -omega: $(OMEGAVO) $(OMEGACMO) $(ROMEGAVO) $(ROMEGACMO) -ring: $(RINGVO) $(RINGCMO) -setoid_ring: $(NEWRINGVO) $(NEWRINGCMO) -dp: $(DPCMO) -xml: $(XMLVO) $(XMLCMO) -extraction: $(EXTRACTIONCMO) -field: $(FIELDVO) $(FIELDCMO) -fourier: $(FOURIERVO) $(FOURIERCMO) -jprover: $(JPROVERVO) $(JPROVERCMO) -funind: $(FUNINDCMO) $(FUNINDVO) -cc: $(CCVO) $(CCCMO) -subtac: $(SUBTACVO) $(SUBTACCMO) -rtauto: $(RTAUTOVO) $(RTAUTOCMO) - -ALLVO = $(INITVO) $(THEORIESVO) $(CONTRIBVO) - -########################################################################### -# rules to make theories, contrib and states +# Cleaning ########################################################################### -SYNTAXPP=syntax/PPConstr.v syntax/PPCases.v - -states/initial.coq: states/MakeInitial.v $(INITVO) - $(BOOTCOQTOP) -batch -notop -silent -nois -load-vernac-source states/MakeInitial.v -outputstate states/initial.coq +.PHONY: clean objclean cruftclean indepclean archclean ml4clean clean-ide ml4depclean depclean distclean cleanconfig cleantheories docclean devdocclean -theories/Init/%.vo: $(BESTCOQTOP) theories/Init/%.v - $(BOOTCOQTOP) -nois -compile theories/Init/$* +clean: objclean cruftclean depclean docclean devdocclean -theories/%.vo: theories/%.v states/initial.coq - $(BOOTCOQTOP) -compile theories/$* +objclean: archclean indepclean -contrib/%.vo: contrib/%.v - $(BOOTCOQTOP) -compile contrib/$* - -cleantheories: - rm -f states/*.coq - rm -f theories/*/*.vo - -clean :: cleantheories - -clean :: - rm -f contrib/*/*.cm[io] contrib/*.cma contrib/*/*.vo - -archclean:: - rm -f contrib/*/*.cmx contrib/*.cmxa contrib/*.a contrib/*/*.[so] - -# globalizations (for coqdoc) +cruftclean: ml4clean + find . -name '*~' -or -name '*.annot' | xargs rm -f + rm -f gmon.out core -glob.dump:: +indepclean: + rm -f $(GENFILES) + rm -f $(COQTOPBYTE) $(COQCBYTE) bin/coq-interface$(EXE) bin/parser$(EXE) + find . -name '*~' -or -name '*.cm[ioa]' | xargs rm -f + find contrib -name '*.vo' -or -name '*.glob' | xargs rm -f + rm -f */*.pp[iox] contrib/*/*.pp[iox] + rm -rf $(SOURCEDOCDIR) + rm -f toplevel/mltop.byteml toplevel/mltop.optml 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) - -DEBUGPRINTERS=dev/top_printers.cmo dev/vm_printers.cmo dev/printers.cma - -printers: $(DEBUGPRINTERS) - -tools:: $(TOOLS) $(DEBUGPRINTERS) - -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 - -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/cdglobals.cmo 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 + rm -f revision + +docclean: + rm -f doc/*/*.dvi doc/*/*.aux doc/*/*.log doc/*/*.bbl doc/*/*.blg doc/*/*.toc \ + doc/*/*.idx doc/*/*~ doc/*/*.ilg doc/*/*.ind doc/*/*.dvi.gz doc/*/*.ps.gz doc/*/*.pdf.gz\ + doc/*/*.???idx doc/*/*.???ind doc/*/*.v.tex doc/*/*.atoc doc/*/*.lof\ + doc/*/*.hatoc doc/*/*.haux doc/*/*.hcomind doc/*/*.herrind doc/*/*.hidx doc/*/*.hind \ + doc/*/*.htacind doc/*/*.htoc doc/*/*.v.html + rm -f doc/stdlib/index-list.html doc/stdlib/index-body.html \ + doc/stdlib/Library.coqdoc.tex doc/stdlib/library.files \ + doc/stdlib/library.files.ls + rm -f doc/*/*.ps doc/*/*.pdf + rm -rf doc/refman/html doc/stdlib/html doc/faq/html doc/tutorial/tutorial.v.html + rm -f doc/stdlib/html/*.html + rm -f doc/refman/euclid.ml{,i} doc/refman/heapsort.ml{,i} + rm -f doc/common/version.tex + rm -f doc/refman/*.eps doc/refman/Reference-Manual.html + rm -f doc/coq.tex -archclean:: +archclean: clean-ide cleantheories + rm -f $(COQTOPOPT) $(BESTCOQTOP) $(COQC) $(COQMKTOP) + rm -f $(COQTOP) $(COQCOPT) $(COQMKTOPOPT) + rm -f bin/parser.opt$(EXE) bin/coq-interface.opt$(EXE) + find . -name '*.cmx' -or -name '*.cmxa' -or -name '*.[soa]' | xargs rm -f 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 $@ $(CMA) $(MINICOQCMO) $(OSDEPLIBS) - -archclean:: rm -f $(MINICOQ) -########################################################################### -# Installation -########################################################################### - -COQINSTALLPREFIX= -OLDROOT= - - # 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=$(BINDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) -FULLCOQLIB=$(COQLIB:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) -FULLMANDIR=$(MANDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) -FULLEMACSLIB=$(EMACSLIB:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) -FULLCOQDOCDIR=$(COQDOCDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) - -install-coq: install-binaries install-library 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) - # recopie des fichiers de style pour coqide - $(MKDIR) $(FULLCOQLIB)/tools/coqdoc - touch $(FULLCOQLIB)/tools/coqdoc/coqdoc.sty $(FULLCOQLIB)/tools/coqdoc/coqdoc.css # to have the mode according to umask (bug #1715) - cp tools/coqdoc/coqdoc.css tools/coqdoc/coqdoc.sty $(FULLCOQLIB)/tools/coqdoc - cp $(TOOLS) $(FULLBINDIR) - -LIBFILES=$(THEORIESVO) $(CONTRIBVO) -LIBFILESLIGHT=$(THEORIESLIGHTVO) - - -GRAMMARCMA=parsing/grammar.cma -OBJECTCMA=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 - -OBJECTCMXA=$(OBJECTCMA:.cma=.cmxa) - -install-library: - $(MKDIR) $(FULLCOQLIB) - for f in $(LIBFILES); do \ - $(MKDIR) $(FULLCOQLIB)/`dirname $$f`; \ - cp $$f $(FULLCOQLIB)/`dirname $$f`; \ - done - $(MKDIR) $(FULLCOQLIB)/states - cp states/*.coq $(FULLCOQLIB)/states - $(MKDIR) $(FULLCOQLIB)/user-contrib - cp $(OBJECTCMA) $(OBJECTCMXA) $(GRAMMARCMA) $(FULLCOQLIB) - -install-library-light: - $(MKDIR) $(FULLCOQLIB) - for f in $(LIBFILESLIGHT); do \ - $(MKDIR) $(FULLCOQLIB)/`dirname $$f`; \ - cp $$f $(FULLCOQLIB)/`dirname $$f`; \ - done - $(MKDIR) $(FULLCOQLIB)/states - cp states/*.coq $(FULLCOQLIB)/states - -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: glob.dump - (cd doc; $(MAKE) all) - -clean:: - (cd doc; $(MAKE) clean) - -clean:: - rm -f doc/coq.tex - -########################################################################### -# Documentation of the source code (using ocamldoc) -########################################################################### +clean-ide: + rm -f $(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 -SOURCEDOCDIR=dev/source-doc +ml4clean: + rm -f $(ML4FILESML) $(ML4FILESML:.ml=.ml4-preprocessed) -.PHONY: source-doc +ml4depclean: + find . -name '*.ml4.d' | xargs rm -f -source-doc: - if !(test -d $(SOURCEDOCDIR)); then mkdir $(SOURCEDOCDIR); fi - $(OCAMLDOC) -html -rectypes $(LOCALINCLUDES) -d $(SOURCEDOCDIR) `find . -name "*.ml"` +depclean: + find . -name '*.d' | xargs rm -f -clean:: - rm -rf $(SOURCEDOCDIR) +cleanconfig: + rm -f config/Makefile config/coq_config.ml dev/ocamldebug-v7 ide/undo.mli +distclean: clean cleanconfig +cleantheories: + rm -f states/*.coq + find theories -name '*.vo' -or -name '*.glob' | xargs rm -f +devdocclean: + find . -name '*.dep.ps' -o -name '*.dot' -exec rm -f {} \; ########################################################################### # Emacs tags ########################################################################### -# NB: the -maxdepth 3 is for excluding files from contrib/extraction/test - tags: - find . -maxdepth 3 -regex ".*\.ml[i4]?" | sort -r | xargs \ + echo $(MLIFILES) $(MLFILES) $(ML4FILES) | sort -r | xargs \ etags --language=none\ "--regex=/let[ \t]+\([^ \t]+\)/\1/" \ "--regex=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \ @@ -1372,11 +223,14 @@ tags: "--regex=/exception[ \t]+\([^ \t]+\)/\1/" \ "--regex=/val[ \t]+\([^ \t]+\)/\1/" \ "--regex=/module[ \t]+\([^ \t]+\)/\1/" + echo $(ML4FILES) | sort -r | xargs \ + etags --append --language=none\ + "--regex=/[ \t]*\([^: \t]+\)[ \t]*:/\1/" + otags: - find . -maxdepth 3 -name "*.ml" -o -name "*.mli" \ - | sort -r | xargs otags - find . -maxdepth 3 -name "*.ml4" | sort -r | xargs \ + echo $(MLIFILES) $(MLFILES) | sort -r | xargs otags + echo $(ML4FILES) | sort -r | xargs \ etags --append --language=none\ "--regex=/let[ \t]+\([^ \t]+\)/\1/" \ "--regex=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \ @@ -1387,413 +241,12 @@ otags: "--regex=/module[ \t]+\([^ \t]+\)/\1/" -########################################################################### -### Special rules -########################################################################### - -# grammar modules with camlp4 - -ML4FILES += parsing/lexer.ml4 parsing/pcoq.ml4 parsing/q_util.ml4 \ - parsing/q_coqast.ml4 parsing/g_prim.ml4 - -GRAMMARNEEDEDCMO=\ - lib/pp_control.cmo lib/pp.cmo lib/compat.cmo lib/util.cmo lib/bigint.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/mod_subst.cmo kernel/sign.cmo \ - kernel/cbytecodes.cmo kernel/copcodes.cmo kernel/cemitcodes.cmo \ - kernel/declarations.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) - -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/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 \ - pretyping/termops.cmo pretyping/evd.cmo \ - pretyping/rawterm.cmo pretyping/termops.cmo pretyping/evd.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/unification.cmo pretyping/evarconv.cmo \ - pretyping/tacred.cmo pretyping/classops.cmo pretyping/detyping.cmo \ - pretyping/indrec.cmo pretyping/coercion.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/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 - -dev/printers.cma: $(PRINTERSCMO) - $(SHOW)'Testing $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) gramlib.cma $(PRINTERSCMO) -o test-printer - @rm -f test-printer - $(SHOW)'OCAMLC -a $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) $(PRINTERSCMO) -linkall -a -o $@ - -parsing/grammar.cma: $(GRAMMARCMO) - $(SHOW)'Testing $@' - @touch test.ml4 - $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENSIONS) $(GRAMMARCMO) -impl" -impl test.ml4 -o test-grammar - @rm -f test-grammar test.* - $(SHOW)'OCAMLC -a $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) $(GRAMMARCMO) -linkall -a -o $@ - -clean:: - rm -f parsing/grammar.cma - -ML4FILES +=parsing/g_minicoq.ml4 \ - parsing/g_vernac.ml4 parsing/g_proofs.ml4 \ - parsing/g_xml.ml4 parsing/g_constr.ml4 \ - parsing/g_tactic.ml4 parsing/g_ltac.ml4 \ - parsing/argextend.ml4 parsing/tacextend.ml4 \ - parsing/vernacextend.ml4 parsing/q_constr.ml4 \ - parsing/g_decl_mode.ml4 - - -BEFOREDEPEND+= $(GRAMMARCMO) - -# BEFOREDEPEND+= parsing/pcoq.ml parsing/extend.ml - -# File using pa_macro and only necessary for parsing ml files - -parsing/q_coqast.cmo: parsing/q_coqast.ml4 - $(SHOW)'OCAMLC4 $<' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENSIONS) $(CAMLP4OPTIONS) -impl" -c -impl $< - -# 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) $(CAMLP4EXTENSIONS) pr_o.cmo -DByte -impl $< > $@ || rm -f $@ - -toplevel/mltop.optml: toplevel/mltop.ml4 - $(SHOW)'CAMLP4O $<' - $(HIDE)$(CAMLP4O) $(CAMLP4EXTENSIONS) 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 $< - -parsing/pptactic.cmo: parsing/pptactic.ml - $(SHOW)'OCAMLC -rectypes $<' - $(HIDE)$(OCAMLC) -rectypes $(BYTEFLAGS) -c $< - -parsing/pptactic.cmx: parsing/pptactic.ml - $(SHOW)'OCAMLOPT -rectypes $<' - $(HIDE)$(OCAMLOPT) -rectypes $(OPTFLAGS) -c $< - -ML4FILES += lib/pp.ml4 lib/compat.ml4 - -lib/compat.cmo: lib/compat.ml4 - $(SHOW)'OCAMLC4 $<' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENSIONS) $(CAMLP4OPTIONS) -impl" -c -impl $< - -lib/compat.cmx: lib/compat.ml4 - $(SHOW)'OCAMLOPT $<' - $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENSIONS) $(CAMLP4OPTIONS) -impl" -c -impl $< - -# files compiled with camlp4 because of streams syntax - -ML4FILES += 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) $(CAMLP4EXTENSIONS) pr_o.cmo `$(CAMLP4DEPS) $<` -impl" -c -impl $< - -parsing/lexer.cmo: parsing/lexer.ml4 - $(SHOW)'OCAMLC4 $<' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENSIONS) pr_o.cmo `$(CAMLP4DEPS) $<` -impl" -c -impl $< - -# pretty printing of the revision number when compiling a checked out -# source tree -.PHONY: revision - -revision: -ifeq ($(CHECKEDOUT),1) - - /bin/rm -f revision - sed -ne '/url/s/^.*\/\([^\/"]\{1,\}\)"$$/\1/p' .svn/entries > revision - sed -ne '/revision/s/^.*"\([0-9]\{1,\}\)".*$$/r\1/p' .svn/entries >> revision -endif - -archclean:: - /bin/rm -f revision - - -########################################################################### -# Default rules -########################################################################### - -.SUFFIXES: .ml .mli .cmo .cmi .cmx .mll .mly .ml4 .v .vo .el .elc .h .c .o - -.c.o: - $(CC) -o $@ $(CFLAGS) $(CINCLUDES) -c $< - -.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) $(CAMLP4EXTENSIONS) `$(CAMLP4DEPS) $<` $(CAMLP4OPTIONS) -impl" -c -impl $< - -.ml4.cmo: - $(SHOW)'OCAMLC4 $<' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENSIONS) `$(CAMLP4DEPS) $<` $(CAMLP4OPTIONS) -impl" -c -impl $< - -.el.elc: +%.elc: %.el +ifdef COQ_CONFIGURED 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 kernel/byterun/*.o - rm -f kernel/byterun/libcoqrun.a - 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 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] config/*.annot - rm -f lib/*.cm[ioa] lib/*.annot - rm -f kernel/*.cm[ioa] kernel/*.annot - rm -f library/*.cm[ioa] library/*.annot - rm -f proofs/*.cm[ioa] proofs/*.annot - rm -f tactics/*.cm[ioa] tactics/*.annot - rm -f interp/*.cm[ioa] interp/*.annot - rm -f parsing/*.cm[ioa] parsing/*.ppo parsing/*.annot - rm -f pretyping/*.cm[ioa] pretyping/*.annot - rm -f toplevel/*.cm[ioa] toplevel/*.annot - rm -f ide/*.cm[ioa] ide/*.annot - rm -f ide/utils/*.cm[ioa] ide/utils/*.annot - rm -f tools/*.cm[ioa] tools/*.annot - rm -f tools/*/*.cm[ioa] tools/*/*.annot - rm -f scripts/*.cm[ioa] scripts/*.annot - rm -f dev/*.cm[ioa] dev/*.annot - rm -f */*.pp[iox] contrib/*/*.pp[iox] - -cleanconfig:: - rm -f config/Makefile config/coq_config.ml dev/ocamldebug-v7 - -########################################################################### -# Dependencies -########################################################################### - -.PHONY: alldepend dependcoq scratchdepend - -alldepend: depend dependcoq - -dependcoq: $(BEFOREDEPEND) $(COQDEP) - $(COQDEP) -slash -coqlib . -R theories Coq -R contrib Coq $(COQINCLUDES) \ - $(ALLFSETS:.vo=.v) $(ALLREALS:.vo=.v) $(ALLVO:.vo=.v) > .depend.coq - -# 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 - $(OCAMLDEP) $(DEPFLAGS) */*.mli */*/*.mli */*.ml */*/*.ml > .depend - -$(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 - -.PHONY: dependp4 -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 -.PHONY: ml4filesml -ml4filesml:: .depend.camlp4 parsing/grammar.cma - $(MAKE) -f Makefile.dep $(ML4FILESML) - - -.PHONY: depend -depend: dependp4 ml4filesml $(BEFOREDEPEND) -# 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 \ - bn=`dirname $$f`/`basename $$f .ml4`; \ - deps=`$(CAMLP4DEPS) $$f`; \ - if [ -n "$${deps}" ]; then \ - /bin/mv -f .depend .depend.tmp; \ - sed -e "\|^$${bn}.cmo|s|^$${bn}.cmo: \(.*\)$$|$${bn}.cmo: $${deps} \1|" \ - -e "\|^$${bn}.cmx|s|^$${bn}.cmx: \(.*\)$$|$${bn}.cmx: $${deps} \1|" \ - .depend.tmp > .depend; \ - /bin/rm -f .depend.tmp; \ - fi; \ - done -# 5. We express dependencies of .o files - $(CC) -MM -isystem $(CAMLHLIB) kernel/byterun/*.c >> .depend -# 6. Finally, we erase the generated .ml files - rm -f $(ML4FILESML) -# and the .cmo and .cmi files needed by grammar.cma - rm -f rm parsing/*.cm[io] lib/pp.cm[io] lib/compat.cm[io] -# 7. 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) $(DEBUGPRINTERS) - --include .depend --include .depend.coq - -clean:: - find . -name "\.#*" -exec rm -f {} \; - -########################################################################### + rm -f $*.compile +else + @echo "Please run ./configure first" >&2; exit 1 +endif |