From 3ef7797ef6fc605dfafb32523261fe1b023aeecb Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 28 Apr 2006 14:59:16 +0000 Subject: Imported Upstream version 8.0pl3+8.1alpha --- Makefile | 752 ++++++++++++++++++++++++++++++++++++--------------------------- 1 file changed, 428 insertions(+), 324 deletions(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index fcd6c782..4523b02a 100644 --- a/Makefile +++ b/Makefile @@ -1,12 +1,12 @@ -######################################################################## -# v # The Coq Proof Assistant / The Coq Development Team # -# \ + 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 + +bytecompfile : kernel/byterun/coq_jumptbl.h kernel/copcodes.ml + +beforedepend:: bytecompfile + +clean :: + rm -f kernel/byterun/coq_jumptbl.h kernel/copcodes.ml ########################################################################### # Main targets (coqmktop, coqtop.opt, coqtop.byte) @@ -310,26 +390,20 @@ COQBINARIES= $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(BESTCOQTOP) $(COQTOP) coqbinaries:: ${COQBINARIES} -coq: coqlib tools coqbinaries coqlib7 -coq8: coqlib tools coqbinaries -coq7: coqlib7 tools coqbinaries - -coqlib:: newtheories newcontrib +coq: coqlib tools coqbinaries -coqlib7: theories7 contrib7 +coqlib:: theories contrib coqlight: theories-light tools coqbinaries -states7:: states7/initial.coq - states:: states/initial.coq -$(COQTOPOPT): $(COQMKTOP) $(CMX) $(USERTACCMX) +$(COQTOPOPT): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN) $(USERTACCMX) $(SHOW)'COQMKTOP -o $@' $(HIDE)$(COQMKTOP) -opt $(OPTFLAGS) -o $@ $(STRIP) $@ -$(COQTOPBYTE): $(COQMKTOP) $(CMO) $(USERTACCMO) +$(COQTOPBYTE): $(COQMKTOP) $(LINKCMO) $(LIBCOQRUN) $(USERTACCMO) $(SHOW)'COQMKTOP -o $@' $(HIDE)$(COQMKTOP) -top $(BYTEFLAGS) -o $@ @@ -345,21 +419,12 @@ $(COQMKTOP): $(COQMKTOPCMO) $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ -custom str.cma unix.cma \ $(COQMKTOPCMO) $(OSDEPLIBS) + scripts/tolink.ml: Makefile $(SHOW)"ECHO... >" $@ - $(HIDE)echo "let lib = \""$(LIBREP)"\"" > $@ - $(HIDE)echo "let kernel = \""$(KERNEL)"\"" >> $@ - $(HIDE)echo "let library = \""$(LIBRARY)"\"" >> $@ - $(HIDE)echo "let pretyping = \""$(PRETYPING)"\"" >> $@ - $(HIDE)echo "let proofs = \""$(PROOFS)"\"" >> $@ - $(HIDE)echo "let tactics = \""$(TACTICS)"\"" >> $@ - $(HIDE)echo "let interp = \""$(INTERP)"\"" >> $@ - $(HIDE)echo "let parsing = \""$(PARSING)"\"" >> $@ - $(HIDE)echo "let toplevel = \""$(TOPLEVEL)"\"" >> $@ - $(HIDE)echo "let highparsing = \""$(HIGHPARSING)"\"" >> $@ - $(HIDE)echo "let highparsingnew = \""$(HIGHPARSINGNEW)"\"" >> $@ - $(HIDE)echo "let hightactics = \""$(HIGHTACTICS)" "$(USERTACCMO)"\"" >> $@ - $(HIDE)echo "let contrib = \""$(CONTRIB)"\"" >> $@ + $(HIDE)echo "let copts = \"-cclib -lcoqrun\"" > $@ + $(HIDE)echo "let core_libs = \""$(LINKCMO)"\"" >> $@ + $(HIDE)echo "let core_objs = \""$(OBJSCMO)"\"" >> $@ $(HIDE)echo "let ide = \""$(COQIDECMO)"\"" >> $@ beforedepend:: scripts/tolink.ml @@ -375,10 +440,15 @@ $(COQC): $(COQCCMO) $(COQTOPBYTE) $(BESTCOQTOP) 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) @@ -386,7 +456,6 @@ interp: $(INTERP) parsing: $(PARSING) pretyping: $(PRETYPING) highparsing: $(HIGHPARSING) -highparsingnew: $(HIGHPARSINGNEW) toplevel: $(TOPLEVEL) hightactics: $(HIGHTACTICS) @@ -489,14 +558,6 @@ contrib/contrib.cmxa: $(CONTRIB:.cmo=.cmx) $(SHOW)'OCAMLOPT -a -o $@' $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(CONTRIB:.cmo=.cmx) -parsing/highparsingnew.cma: $(HIGHPARSINGNEW) - $(SHOW)'OCAMLC -a -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $(HIGHPARSINGNEW) - -parsing/highparsingnew.cmxa: $(HIGHPARSINGNEW:.cmo=.cmx) - $(SHOW)'OCAMLOPT -a -o $@' - $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(HIGHPARSINGNEW:.cmo=.cmx) - ########################################################################### # CoqIde special targets ########################################################################### @@ -508,7 +569,7 @@ COQIDEBYTE=bin/coqide.byte$(EXE) COQIDEOPT=bin/coqide.opt$(EXE) COQIDE=bin/coqide$(EXE) -COQIDECMO=ide/utils/okey.cmo ide/utils/uoptions.cmo \ +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 \ @@ -530,7 +591,7 @@ COQIDEVO=ide/utf8.vo $(COQIDEVO): states/initial.coq $(BOOTCOQTOP) -compile $* -IDEFILES=$(COQIDEVO) ide/utf8.v ide/coq.ico ide/coq2.ico ide/.coqide-gtk2rc +IDEFILES=$(COQIDEVO) ide/utf8.v ide/coq.png ide/.coqide-gtk2rc coqide-binaries: coqide-$(HASCOQIDE) coqide-no: @@ -544,47 +605,42 @@ clean-ide: rm -f ide/config_lexer.ml ide/config_parser.mli ide/config_parser.ml rm -f ide/utf8_convert.ml -$(COQIDEOPT): $(COQMKTOP) $(CMX) $(USERTACCMX) ide/ide.cmxa +$(COQIDEOPT): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN) $(USERTACCMX) ide/ide.cmxa $(SHOW)'COQMKTOP -o $@' $(HIDE)$(COQMKTOP) -ide -opt $(OPTFLAGS) -o $@ $(STRIP) $@ -$(COQIDEBYTE): $(COQMKTOP) $(CMO) $(USERTACCMO) ide/ide.cma +$(COQIDEBYTE): $(COQMKTOP) $(LINKCMO) $(LIBCOQRUN) $(USERTACCMO) ide/ide.cma $(SHOW)'COQMKTOP -o $@' - $(HIDE)$(COQMKTOP) -ide -top $(BYTEFLAGS) -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) $(COQIDEFLAGS) $(BYTEFLAGS) -c $< + $(HIDE)$(OCAMLC) -g $(COQIDEFLAGS) $(BYTEFLAGS) -c $< ide/%.cmi: ide/%.mli $(SHOW)'OCAMLC $<' - $(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -c $< + $(HIDE)$(OCAMLC) -g $(COQIDEFLAGS) $(BYTEFLAGS) -c $< ide/%.cmx: ide/%.ml $(SHOW)'OCAMLOPT $<' $(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -c $< -ide/utils/%.cmo: ide/utils/%.ml +ide/utils/%.cmo: ide/%.ml $(SHOW)'OCAMLC $<' - $(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -c $< + $(HIDE)$(OCAMLC) -g $(COQIDEFLAGS) $(BYTEFLAGS) -c $< -ide/utils/%.cmi: ide/utils/%.mli +ide/utils/%.cmi: ide/%.mli $(SHOW)'OCAMLC $<' - $(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -c $< + $(HIDE)$(OCAMLC) -g $(COQIDEFLAGS) $(BYTEFLAGS) -c $< -ide/utils/%.cmx: ide/utils/%.ml +ide/utils/%.cmx: ide/%.ml $(SHOW)'OCAMLOPT $<' $(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -c $< -# Special target to select between whether lablgtk >= 2.6.0 or not -ide/undo.cmi: ide/undo.mli - $(SHOW)'OCAMLC $<' - $(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) $(CAMLP4COMPAT) -intf" -c -intf $< - 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 @@ -642,12 +698,13 @@ INTERFACE=\ contrib/interface/name_to_ast.cmo contrib/interface/debug_tac.cmo \ contrib/interface/showproof_ct.cmo contrib/interface/showproof.cmo \ contrib/interface/blast.cmo contrib/interface/centaur.cmo + INTERFACECMX=$(INTERFACE:.cmo=.cmx) ML4FILES += contrib/interface/debug_tac.ml4 contrib/interface/centaur.ml4 -PARSERREQUIRES=$(CMO) # Solution de facilité... -PARSERREQUIRESCMX=$(CMX) +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) @@ -657,11 +714,11 @@ endif pcoq-binaries:: $(COQINTERFACE) -bin/coq-interface$(EXE): $(COQMKTOP) $(CMO) $(USERTACCMO) $(INTERFACE) +bin/coq-interface$(EXE): $(COQMKTOP) $(LINKCMO) $(LIBCOQRUN) $(USERTACCMO) $(INTERFACE) $(SHOW)'COQMKTOP -o $@' $(HIDE)$(COQMKTOP) -top $(BYTEFLAGS) -o $@ $(INTERFACE) -bin/coq-interface.opt$(EXE): $(COQMKTOP) $(CMX) $(USERTACCMX) $(INTERFACECMX) +bin/coq-interface.opt$(EXE): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN) $(USERTACCMX) $(INTERFACECMX) $(SHOW)'COQMKTOP -o $@' $(HIDE)$(COQMKTOP) -opt $(OPTFLAGS) -o $@ $(INTERFACECMX) @@ -672,13 +729,13 @@ PARSERCMX= $(PARSERREQUIRESCMX) $(PARSERCODE:.cmo=.cmx) bin/parser$(EXE): $(PARSERCMO) $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) -linkall -custom -cclib -lunix $(OPTFLAGS) -o $@ \ + $(HIDE)$(OCAMLC) -linkall -custom -cclib -lunix $(BYTEFLAGS) -o $@ \ dynlink.cma $(CMA) $(PARSERCMO) bin/parser.opt$(EXE): $(PARSERCMX) $(SHOW)'OCAMLOPT -o $@' $(HIDE)$(OCAMLOPT) -linkall -cclib -lunix $(OPTFLAGS) -o $@ \ - $(CMXA) $(PARSERCMX) + $(LIBCOQRUN) $(CMXA) $(PARSERCMX) INTERFACEVO= @@ -686,14 +743,8 @@ INTERFACERC= contrib/interface/vernacrc pcoq-files:: $(INTERFACEVO) $(INTERFACERC) -# Centaur grammar rules now in centaur.ml4 -contrib7/interface/Centaur.vo: contrib7/interface/Centaur.v $(INTERFACE) - $(BESTCOQTOP) $(TRANSLATE) -boot -byte $(COQOPTS) -compile $* - -# Move the grammar rules to dad.ml ? -contrib7/interface/AddDad.vo: contrib7/interface/AddDad.v $(INTERFACE) states7/initial.coq - $(BESTCOQTOP) $(TRANSLATE) -boot -byte $(COQOPTS) -compile $* - +clean:: + rm -f bin/parser$(EXE) bin/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 @@ -730,7 +781,7 @@ INITVO=\ theories/Init/Datatypes.vo theories/Init/Peano.vo \ theories/Init/Logic.vo theories/Init/Specif.vo \ theories/Init/Logic_Type.vo theories/Init/Wf.vo \ - theories/Init/Prelude.vo + theories/Init/Tactics.vo theories/Init/Prelude.vo init: $(INITVO) @@ -743,7 +794,8 @@ LOGICVO=\ theories/Logic/Berardi.vo theories/Logic/Eqdep_dec.vo \ theories/Logic/Decidable.vo theories/Logic/JMeq.vo \ theories/Logic/ClassicalDescription.vo theories/Logic/ClassicalChoice.vo \ - theories/Logic/RelationalChoice.vo theories/Logic/Diaconescu.vo + theories/Logic/RelationalChoice.vo theories/Logic/Diaconescu.vo \ + theories/Logic/EqdepFacts.vo theories/Logic/ProofIrrelevanceFacts.vo ARITHVO=\ theories/Arith/Arith.vo theories/Arith/Gt.vo \ @@ -778,7 +830,8 @@ ZARITHVO=\ theories/ZArith/auxiliary.vo theories/ZArith/Zmisc.vo \ theories/ZArith/Zcompare.vo theories/ZArith/Znat.vo \ theories/ZArith/Zorder.vo theories/ZArith/Zabs.vo \ - theories/ZArith/Zmin.vo theories/ZArith/Zeven.vo \ + theories/ZArith/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 \ @@ -789,7 +842,11 @@ ZARITHVO=\ LISTSVO=\ theories/Lists/MonoList.vo \ theories/Lists/ListSet.vo theories/Lists/Streams.vo \ - theories/Lists/TheoryList.vo theories/Lists/List.vo + theories/Lists/TheoryList.vo theories/Lists/List.vo \ + theories/Lists/SetoidList.vo + +STRINGSVO=\ + theories/Strings/Ascii.vo theories/Strings/String.vo SETSVO=\ theories/Sets/Classical_sets.vo theories/Sets/Permut.vo \ @@ -804,6 +861,19 @@ SETSVO=\ theories/Sets/Multiset.vo theories/Sets/Relations_3_facts.vo \ theories/Sets/Partial_Order.vo theories/Sets/Uniset.vo +FSETSVO=\ + theories/FSets/DecidableType.vo theories/FSets/OrderedType.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/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/FMapWeakInterface.vo theories/FSets/FMapWeakList.vo \ + theories/FSets/FMapWeak.vo + INTMAPVO=\ theories/IntMap/Adalloc.vo theories/IntMap/Mapcanon.vo \ theories/IntMap/Addec.vo theories/IntMap/Mapcard.vo \ @@ -870,28 +940,28 @@ REALS_all=\ REALSVO=$(REALSBASEVO) $(REALS_$(REALS)) ALLREALS=$(REALSBASEVO) $(REALS_all) -ALLOLDREALS=$(REALSBASEVO:theories%.vo:theories7%.vo) $(REALS_all:theories%.vo:theories7%.vo) SETOIDSVO=theories/Setoids/Setoid.vo THEORIESVO =\ $(INITVO) $(LOGICVO) $(ARITHVO) $(BOOLVO) $(NARITHVO) $(ZARITHVO) \ - $(LISTSVO) $(SETSVO) $(INTMAPVO) $(RELATIONSVO) $(WELLFOUNDEDVO) \ - $(REALSVO) $(SETOIDSVO) $(SORTINGVO) + $(LISTSVO) $(STRINGSVO) $(SETSVO) $(FSETSVO) $(INTMAPVO) $(RELATIONSVO) \ + $(WELLFOUNDEDVO) $(REALSVO) $(SETOIDSVO) $(SORTINGVO) -NEWTHEORIESLIGHTVO = $(INITVO) $(LOGICVO) $(ARITHVO) -OLDTHEORIESLIGHTVO = $(NEWTHEORIESLIGHTVO:theories%.vo:theories7%.vo) +THEORIESLIGHTVO = $(INITVO) $(LOGICVO) $(ARITHVO) theories: $(THEORIESVO) -theories-light: $(NEWTHEORIESLIGHTVO) +theories-light: $(THEORIESLIGHTVO) logic: $(LOGICVO) arith: $(ARITHVO) bool: $(BOOLVO) narith: $(NARITHVO) zarith: $(ZARITHVO) -lists: $(LISTVO) $(LISTSVO) +lists: $(LISTSVO) +strings: $(STRINGSVO) sets: $(SETSVO) +fsets: $(FSETSVO) intmap: $(INTMAPVO) relations: $(RELATIONSVO) wellfounded: $(WELLFOUNDEDVO) @@ -901,7 +971,7 @@ allreals: $(ALLREALS) setoids: $(SETOIDSVO) sorting: $(SORTINGVO) -noreal: logic arith bool zarith lists sets intmap relations wellfounded \ +noreal: logic arith bool zarith lists sets fsets intmap relations wellfounded \ setoids sorting ########################################################################### @@ -922,6 +992,11 @@ RINGVO=\ contrib/ring/Quote.vo contrib/ring/Setoid_ring_normalize.vo \ contrib/ring/Setoid_ring.vo contrib/ring/Setoid_ring_theory.vo +NEWRINGVO=\ + contrib/setoid_ring/BinList.vo contrib/setoid_ring/Ring_th.vo \ + contrib/setoid_ring/Pol.vo contrib/setoid_ring/Ring_tac.vo \ + contrib/setoid_ring/ZRing_th.vo + FIELDVO=\ contrib/field/Field_Compl.vo contrib/field/Field_Theory.vo \ contrib/field/Field_Tactic.vo contrib/field/Field.vo @@ -933,19 +1008,28 @@ FOURIERVO=\ FUNINDVO= +RECDEFVO=contrib/recdef/Recdef.vo + JPROVERVO= -CCVO=\ - contrib/cc/CCSolve.vo +CCVO= + +SUBTACVO=contrib/subtac/FixSub.vo contrib/subtac/Utils.vo + +RTAUTOVO = \ + contrib/rtauto/Bintree.vo contrib/rtauto/Rtauto.vo CONTRIBVO = $(OMEGAVO) $(ROMEGAVO) $(RINGVO) $(FIELDVO) $(XMLVO) \ - $(FOURIERVO) $(JPROVERVO) $(CCVO) $(FUNINDVO) + $(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) @@ -953,40 +1037,10 @@ fourier: $(FOURIERVO) $(FOURIERCMO) jprover: $(JPROVERVO) $(JPROVERCMO) funind: $(FUNINDCMO) $(FUNINDVO) cc: $(CCVO) $(CCCMO) +subtac: $(SUBTACVO) $(SUBTACCMO) +rtauto: $(RTAUTOVO) $(RTAUTOCMO) -NEWINITVO=$(INITVO) -NEWTHEORIESVO=$(THEORIESVO) -NEWCONTRIBVO=$(CONTRIBVO) - -OBSOLETETHEORIESVO=\ - theories7/Lists/PolyList.vo theories7/Lists/PolyListSyntax.vo \ - theories7/ZArith/Zsyntax.vo \ - theories7/ZArith/zarith_aux.vo theories7/ZArith/fast_integer.vo \ - theories7/Reals/Rsyntax.vo - -OLDINITVO=$(INITVO:theories%.vo=theories7%.vo) -OLDTHEORIESVO=$(THEORIESVO:theories%.vo=theories7%.vo) $(OBSOLETETHEORIESVO) -OLDCONTRIBVO=$(CONTRIBVO:contrib%.vo=contrib7%.vo) - -$(OLDCONTRIBVO): states7/initial.coq - -NEWINITV=$(INITVO:%.vo=%.v) -NEWTHEORIESV=$(THEORIESVO:%.vo=%.v) -NEWCONTRIBV=$(CONTRIBVO:%.vo=%.v) - -# Made *.vo and new*.v targets explicit, otherwise "make" -# either removes them after use or don't do them (e.g. List.vo) -newinit:: $(NEWINITV) $(NEWINITVO) -newtheories:: $(NEWTHEORIESV) $(NEWTHEORIESVO) -newcontrib:: $(NEWCONTRIBV) $(NEWCONTRIBVO) $(CONTRIBCMO) - -theories7:: $(OLDTHEORIESVO) -contrib7:: $(OLDCONTRIBVO) - -translation:: $(NEWTHEORIESV) $(NEWCONTRIBV) - -ALLNEWVO = $(INITVO) $(THEORIESVO) $(CONTRIBVO) -ALLOLDVO = $(OLDINITVO) $(OLDTHEORIESVO) $(OLDCONTRIBVO) +ALLVO = $(INITVO) $(THEORIESVO) $(CONTRIBVO) ########################################################################### # rules to make theories, contrib and states @@ -994,23 +1048,8 @@ ALLOLDVO = $(OLDINITVO) $(OLDTHEORIESVO) $(OLDCONTRIBVO) SYNTAXPP=syntax/PPConstr.v syntax/PPCases.v -states7/barestate.coq: $(SYNTAXPP) $(BESTCOQTOP) - $(BESTCOQTOP) -v7 -boot -batch -silent -nois -I syntax -load-vernac-source syntax/MakeBare.v -outputstate $@ - -states7/initial.coq: states7/barestate.coq states7/MakeInitial.v $(OLDINITVO) $(BESTCOQTOP) - $(BOOTCOQTOP) -v7 -batch -silent -is states7/barestate.coq -load-vernac-source states7/MakeInitial.v -outputstate states7/initial.coq - -states/initial.coq: states/MakeInitial.v $(NEWINITVO) - $(BOOTCOQTOP) -batch -silent -nois -load-vernac-source states/MakeInitial.v -outputstate states/initial.coq - -theories7/Init/%.vo: $(BESTCOQTOP) theories7/Init/%.v - $(BOOTCOQTOP) $(TRANSLATE) -nois -compile theories7/Init/$* - -theories7/%.vo: theories7/%.v states7/initial.coq - $(BOOTCOQTOP) $(TRANSLATE) -compile theories7/$* - -contrib7/%.vo: contrib7/%.v states7/initial.coq - $(BOOTCOQTOP) $(TRANSLATE) -compile contrib7/$* +states/initial.coq: states/MakeInitial.v $(INITVO) + $(BOOTCOQTOP) -batch -notop -silent -nois -load-vernac-source states/MakeInitial.v -outputstate states/initial.coq theories/Init/%.vo: $(BESTCOQTOP) theories/Init/%.v $(BOOTCOQTOP) -nois -compile theories/Init/$* @@ -1024,13 +1063,14 @@ contrib/%.vo: contrib/%.v contrib/extraction/%.vo: contrib/extraction/%.v states/barestate.coq $(COQC) $(BOOTCOQTOP) -is states/barestate.coq -compile $* -contrib7/extraction/%.vo: contrib7/extraction/%.v states/barestate.coq $(COQC) - $(BOOTCOQTOP) $(TRANSLATE) -is states7/barestate.coq -compile $* +cleantheories: + rm -f states/*.coq + rm -f theories/*/*.vo + +clean :: cleantheories -clean:: - rm -f states/*.coq states7/*.coq - rm -f theories/*/*.vo theories7/*/*.vo - rm -f contrib/*/*.cm[io] contrib/*.cma contrib/*/*.vo contrib7/*/*.vo +clean :: + rm -f contrib/*/*.cm[io] contrib/*.cma contrib/*/*.vo archclean:: rm -f contrib/*/*.cmx contrib/*.cmxa contrib/*.a contrib/*/*.[so] @@ -1056,7 +1096,11 @@ COQDOC=bin/coqdoc$(EXE) TOOLS=$(COQDEP) $(COQMAKEFILE) $(GALLINA) $(COQTEX) \ $(COQWC) $(COQDOC) -tools:: $(TOOLS) dev/top_printers.cmo +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 @@ -1090,9 +1134,9 @@ $(COQWC): tools/coqwc.cmo beforedepend:: tools/coqdoc/pretty.ml tools/coqdoc/index.ml -COQDOCCMO=$(CONFIG) tools/coqdoc/alpha.cmo tools/coqdoc/index.cmo \ - tools/coqdoc/output.cmo tools/coqdoc/pretty.cmo \ - tools/coqdoc/main.cmo +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 $@' @@ -1103,6 +1147,9 @@ clean:: rm -f tools/coqwc.ml rm -f tools/coqdoc/pretty.ml tools/coqdoc/index.ml +archclean:: + rm -f $(TOOLS) + ########################################################################### # minicoq ########################################################################### @@ -1117,23 +1164,24 @@ $(MINICOQ): $(MINICOQCMO) $(SHOW)'OCAMLC -o $@' $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ -custom $(CMA) $(MINICOQCMO) $(OSDEPLIBS) +archclean:: + rm -f $(MINICOQ) + ########################################################################### # Installation ########################################################################### -#COQINSTALLPREFIX= -# Can be changed for a local installation (to make packages). -# You must NOT put a "/" at the end (Cygnus for win32 does not like "//"). +COQINSTALLPREFIX= + # Can be changed for a local installation (to make packages). + # You must NOT put a "/" at the end (Cygnus for win32 does not like "//"). -FULLBINDIR=$(BINDIR:'$(OLDROOT)%='$(COQINSTALLPREFIX)%) -FULLCOQLIB=$(COQLIB:'$(OLDROOT)%='$(COQINSTALLPREFIX)%) -FULLMANDIR=$(MANDIR:'$(OLDROOT)%='$(COQINSTALLPREFIX)%) -FULLEMACSLIB=$(EMACSLIB:'$(OLDROOT)%='$(COQINSTALLPREFIX)%) -FULLCOQDOCDIR=$(COQDOCDIR:'$(OLDROOT)%='$(COQINSTALLPREFIX)%) +FULLBINDIR=$(COQINSTALLPREFIX)$(BINDIR) +FULLCOQLIB=$(COQINSTALLPREFIX)$(COQLIB) +FULLMANDIR=$(COQINSTALLPREFIX)$(MANDIR) +FULLEMACSLIB=$(COQINSTALLPREFIX)$(EMACSLIB) +FULLCOQDOCDIR=$(COQINSTALLPREFIX)$(COQDOCDIR) install-coq: install-binaries install-library install-coq-info -install-coq8: install-binaries install-library8 install-coq-info -install-coq7: install-binaries install-library7 install-coq-info install-coqlight: install-binaries install-library-light install-binaries:: install-$(BEST) install-tools @@ -1152,42 +1200,27 @@ install-tools:: $(MKDIR) $(FULLBINDIR) cp $(TOOLS) $(FULLBINDIR) -LIBFILES=$(OLDTHEORIESVO) $(OLDCONTRIBVO) -LIBFILESLIGHT=$(OLDTHEORIESLIGHTVO) +LIBFILES=$(THEORIESVO) $(CONTRIBVO) +LIBFILESLIGHT=$(THEORIESLIGHTVO) -NEWLIBFILES=$(NEWTHEORIESVO) $(NEWCONTRIBVO) -NEWLIBFILESLIGHT=$(NEWTHEORIESLIGHTVO) - -install-library: install-library7 install-library8 - -install-library8: +install-library: $(MKDIR) $(FULLCOQLIB) - for f in $(NEWLIBFILES); do \ + for f in $(LIBFILES); do \ $(MKDIR) $(FULLCOQLIB)/`dirname $$f`; \ cp $$f $(FULLCOQLIB)/`dirname $$f`; \ done $(MKDIR) $(FULLCOQLIB)/states cp states/*.coq $(FULLCOQLIB)/states - -install-library7: - $(MKDIR) $(FULLCOQLIB) - for f in $(LIBFILES); do \ - $(MKDIR) $(FULLCOQLIB)/`dirname $$f`; \ - cp $$f $(FULLCOQLIB)/`dirname $$f`; \ - done - $(MKDIR) $(FULLCOQLIB)/states7 - cp states7/*.coq $(FULLCOQLIB)/states7 + $(MKDIR) $(FULLCOQLIB)/user-contrib install-library-light: $(MKDIR) $(FULLCOQLIB) - for f in $(LIBFILESLIGHT) $(NEWLIBFILESLIGHT); do \ + for f in $(LIBFILESLIGHT); do \ $(MKDIR) $(FULLCOQLIB)/`dirname $$f`; \ cp $$f $(FULLCOQLIB)/`dirname $$f`; \ done $(MKDIR) $(FULLCOQLIB)/states cp states/*.coq $(FULLCOQLIB)/states - $(MKDIR) $(FULLCOQLIB)/states7 - cp states7/*.coq $(FULLCOQLIB)/states7 install-allreals:: for f in $(ALLREALS); do \ @@ -1215,7 +1248,7 @@ install-emacs: install-latex: $(MKDIR) $(FULLCOQDOCDIR) - cp tools/coqdoc/coqdoc.sty $(FULLCOQDOCDIR) + cp tools/coqdoc/coqdoc.sty $(FULLCOQDOCDIR) # -$(UPDATETEX) ########################################################################### @@ -1223,19 +1256,25 @@ install-latex: # Literate programming (with ocamlweb) ########################################################################### -.PHONY: doc +.PHONY: doc devdoc -doc: doc/coq.tex - $(MAKE) -C doc coq.ps minicoq.dvi +doc: glob.dump + (cd doc; make all) -doc/coq.tex: +clean:: + (cd doc; make clean) + +devdoc: dev/doc/coq.tex + $(MAKE) -C dev/doc coq.ps minicoq.dvi + +dev/doc/coq.tex: ocamlweb -p "\usepackage{epsfig}" \ - doc/macros.tex doc/intro.tex \ + dev/doc/macros.tex dev/doc/intro.tex \ lib/{doc.tex,*.mli} kernel/{doc.tex,*.mli} library/{doc.tex,*.mli} \ pretyping/{doc.tex,*.mli} interp/{doc.tex,*.mli} \ - parsing/{doc.tex,*.mli} proofs/{doc.tex,tacexpr.ml,*.mli} \ - tactics/{doc.tex,*.mli} toplevel/{doc.tex,vernacexpr.ml,*.mli} \ - -o doc/coq.tex + parsing/{doc.tex,*.mli} proofs/{doc.tex,*.mli} \ + tactics/{doc.tex,*.mli} toplevel/{doc.tex,*.mli} \ + -o dev/doc/coq.tex clean:: rm -f doc/coq.tex @@ -1277,60 +1316,116 @@ otags: # grammar modules with camlp4 -ML4FILES += parsing/lexer.ml4 parsing/q_util.ml4 parsing/q_coqast.ml4 \ - parsing/g_prim.ml4 parsing/pcoq.ml4 +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/bignat.cmo \ - lib/dyn.cmo lib/options.cmo \ - lib/hashcons.cmo lib/predicate.cmo lib/rtree.cmo \ - kernel/names.cmo kernel/univ.cmo kernel/esubst.cmo kernel/term.cmo \ - kernel/sign.cmo kernel/declarations.cmo kernel/environ.cmo\ + 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 \ - pretyping/rawterm.cmo pretyping/pattern.cmo pretyping/evd.cmo \ - interp/topconstr.cmo interp/genarg.cmo \ - interp/ppextend.cmo parsing/coqast.cmo parsing/ast.cmo \ - proofs/tacexpr.cmo parsing/ast.cmo \ - parsing/lexer.cmo parsing/q_util.cmo parsing/extend.cmo \ - toplevel/vernacexpr.cmo parsing/pcoq.cmo parsing/q_coqast.cmo \ - parsing/egrammar.cmo + 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 \ - parsing/g_primnew.cmo parsing/g_tacticnew.cmo \ - parsing/g_ltacnew.cmo parsing/g_constrnew.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/cooking.cmo \ + kernel/modops.cmo kernel/type_errors.cmo kernel/inductive.cmo \ + kernel/subtyping.cmo kernel/typeops.cmo kernel/indtypes.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 \ + parsing/ppconstr.cmo parsing/extend.cmo \ + parsing/printer.cmo parsing/pptactic.cmo parsing/tactic_printer.cmo \ + parsing/pcoq.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) $(CAMLP4EXTENDFLAGS) $(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_basevernac.ml4 parsing/g_minicoq.ml4 \ +ML4FILES +=parsing/g_minicoq.ml4 \ parsing/g_vernac.ml4 parsing/g_proofs.ml4 \ - parsing/g_cases.ml4 \ - parsing/g_constr.ml4 parsing/g_module.ml4 \ + parsing/g_xml.ml4 parsing/g_constr.ml4 \ parsing/g_tactic.ml4 parsing/g_ltac.ml4 \ parsing/argextend.ml4 parsing/tacextend.ml4 \ - parsing/vernacextend.ml4 \ - parsing/g_primnew.ml4 \ - parsing/g_vernacnew.ml4 parsing/g_proofsnew.ml4 \ - parsing/g_constrnew.ml4 \ - parsing/g_tacticnew.ml4 parsing/g_ltacnew.ml4 \ + parsing/vernacextend.ml4 parsing/q_constr.ml4 # beforedepend:: $(GRAMMARCMO) # beforedepend:: parsing/pcoq.ml parsing/extend.ml +# File using pa_ifdef and only necessary for parsing ml files + +parsing/q_coqast.cmo: parsing/q_coqast.ml4 + $(SHOW)'OCAMLC4 $<' + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_ifdef.cmo $(CAMLP4COMPAT) -impl" -c -impl $< + # toplevel/mltop.ml4 (ifdef Byte) toplevel/mltop.cmo: toplevel/mltop.byteml @@ -1343,11 +1438,11 @@ toplevel/mltop.cmx: toplevel/mltop.optml toplevel/mltop.byteml: toplevel/mltop.ml4 $(SHOW)'CAMLP4O $<' - $(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pr_o.cmo -DByte -impl $< > $@ || rm -f $@ + $(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_ifdef.cmo pr_o.cmo -DByte -impl $< > $@ || rm -f $@ toplevel/mltop.optml: toplevel/mltop.ml4 $(SHOW)'CAMLP4O $<' - $(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pr_o.cmo -impl $< > $@ || rm -f $@ + $(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_ifdef.cmo pr_o.cmo -impl $< > $@ || rm -f $@ ML4FILES += toplevel/mltop.ml4 @@ -1380,21 +1475,27 @@ proofs/tacexpr.cmx: proofs/tacexpr.ml $(SHOW)'OCAMLOPT -rectypes $<' $(HIDE)$(OCAMLOPT) -rectypes $(OPTFLAGS) -c $< -# files compiled with camlp4 because of macros +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) $(CAMLP4EXTENDFLAGS) -impl" -c -impl $< + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_ifdef.cmo -impl" -c -impl $< lib/compat.cmx: lib/compat.ml4 $(SHOW)'OCAMLOPT $<' - $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) -impl" -c -impl $< + $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_ifdef.cmo -impl" -c -impl $< # files compiled with camlp4 because of streams syntax -ML4FILES += lib/pp.ml4 \ - lib/compat.ml4 \ - contrib/xml/xml.ml4 \ +ML4FILES += contrib/xml/xml.ml4 \ contrib/xml/acic2Xml.ml4 \ contrib/xml/proofTree2Xml.ml4 \ contrib/interface/line_parser.ml4 \ @@ -1404,13 +1505,13 @@ ML4FILES += lib/pp.ml4 \ # Add pr_o.cmo to circumvent a useless-warning bug when preprocessed with # ast-based camlp4 -#parsing/lexer.cmx: parsing/lexer.ml4 -# $(SHOW)'OCAMLOPT4 $<' -# $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4DEPS) $<` pr_o.cmo -impl" -c -impl $< +parsing/lexer.cmx: parsing/lexer.ml4 + $(SHOW)'OCAMLOPT4 $<' + $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4DEPS) $<` pr_o.cmo -impl" -c -impl $< -#parsing/lexer.cmo: parsing/lexer.ml4 -# $(SHOW)'OCAMLC4 $<' -# $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4DEPS) $<` pr_o.cmo -impl" -c -impl $< +parsing/lexer.cmo: parsing/lexer.ml4 + $(SHOW)'OCAMLC4 $<' + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4DEPS) $<` pr_o.cmo -impl" -c -impl $< @@ -1418,7 +1519,10 @@ ML4FILES += lib/pp.ml4 \ # Default rules ########################################################################### -.SUFFIXES: .ml .mli .cmo .cmi .cmx .mll .mly .ml4 .v .vo .el .elc +.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 $<' @@ -1466,10 +1570,11 @@ ML4FILES += lib/pp.ml4 \ ########################################################################### archclean:: - -rm -f bin/* rm -f config/*.cmx* config/*.[soa] rm -f lib/*.cmx* lib/*.[soa] - rm -f kernel/*.cmx* kernel/*.[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] @@ -1479,7 +1584,6 @@ archclean:: rm -f toplevel/*.cmx* toplevel/*.[soa] rm -f ide/*.cmx* ide/*.[soa] rm -f ide/utils/*.cmx* ide/utils/*.[soa] - rm -f translate/*.cmx* translate/*.[soa] rm -f tools/*.cmx* tools/*.[soa] rm -f tools/*/*.cmx* tools/*/*.[soa] rm -f scripts/*.cmx* scripts/*.[soa] @@ -1500,7 +1604,6 @@ clean:: archclean rm -f toplevel/*.cm[ioa] rm -f ide/*.cm[ioa] rm -f ide/utils/*.cm[ioa] - rm -f translate/*.cm[ioa] rm -f tools/*.cm[ioa] rm -f tools/*/*.cm[ioa] rm -f scripts/*.cm[ioa] @@ -1518,9 +1621,7 @@ alldepend: depend dependcoq dependcoq:: beforedepend $(COQDEP) -coqlib . -R theories Coq -R contrib Coq $(COQINCLUDES) \ - $(ALLREALS:.vo=.v) $(ALLNEWVO:.vo=.v) > .depend.coq - $(COQDEP) -coqlib . -R theories7 Coq -R contrib7 Coq $(COQINCLUDES) \ - $(ALLOLDREALS:.vo=.v) $(ALLOLDVO:.vo=.v) > .depend.coq7 + $(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: @@ -1528,6 +1629,7 @@ dependcoq:: beforedepend # .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 @@ -1562,9 +1664,13 @@ depend: beforedepend dependp4 ml4filesml printf "%s" `dirname $$f`/`basename $$f .ml4`".cmx: " >> .depend; \ echo `$(CAMLP4DEPS) $$f` >> .depend; \ done -# 5. Finally, we erase the generated .ml files +# 5. We express dependencies of .o files + gcc -MM $(CINCLUDES) kernel/byterun/*.c >> .depend + gcc -MM $(CINCLUDES) kernel/byterun/*.c | sed -e 's/\.o/.d.o/' >> \ + .depend +# 6. Finally, we erase the generated .ml files rm -f $(ML4FILESML) -# 6. Since .depend contains correct dependencies .depend.devel can be deleted +# 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 @@ -1578,14 +1684,12 @@ clean:: devel: touch .depend.devel $(MAKE) -f dev/Makefile.devel setup-devel - $(MAKE) dev/top_printers.cmo + $(MAKE) $(DEBUGPRINTERS) -include .depend -include .depend.coq -include .depend.coq7 +-include .depend +-include .depend.coq clean:: - rm -fr *.v8 syntax/*.v8 ide/*.v8 theories7/*/*.v8 contrib7/*/*.v8 find . -name "\.#*" -exec rm -f {} \; find . -name "*~" -exec rm -f {} \; -- cgit v1.2.3