From 2ad3eaa5e34c8cc1d2e15fbd2f9e8fbae715b2ce Mon Sep 17 00:00:00 2001 From: letouzey Date: Mon, 16 Mar 2009 13:41:44 +0000 Subject: Makefile: minor improvements * no need anymore for special rules for -rectypes: we use it everywhere * $(REVISIONCMO) is obsolete * avoid triple references to almost all files of kernel/ git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11982 85f007b7-540e-0410-9357-904b9bb8a0f7 --- Makefile.build | 15 --------------- Makefile.common | 40 ++++++++++++++-------------------------- 2 files changed, 14 insertions(+), 41 deletions(-) diff --git a/Makefile.build b/Makefile.build index ea2fad128..5d5ff8533 100644 --- a/Makefile.build +++ b/Makefile.build @@ -768,21 +768,6 @@ toplevel/mltop.optml: toplevel/mltop.ml4 config/Makefile # no camlp4deps here $(NATDYNLINKDEF) -impl $< > $@ \ || ( RV=$$?; rm -f "$@"; exit $${RV} ) -# files compiled with -rectypes - -define rectypes-rules-template -$(1:.ml=.cmo): $(1) | $(1).d - $(SHOW)'OCAMLC -rectypes $$<' - $(HIDE)$(OCAMLC) -rectypes $(BYTEFLAGS) -c $$< - -$(1:.ml=.cmx): $(1) | $(1).d - $(SHOW)'OCAMLOPT -rectypes $$<' - $(HIDE)$(OCAMLOPT) -rectypes $(OPTFLAGS) -c $$< - -endef - -$(foreach f,$(RECTYPESML),$(eval $(call rectypes-rules-template,$(f)))) - # pretty printing of the revision number when compiling a checked out # source tree .PHONY: revision diff --git a/Makefile.common b/Makefile.common index 5a981ae12..ce1fad6b2 100644 --- a/Makefile.common +++ b/Makefile.common @@ -153,16 +153,20 @@ LIBREP:=$(addprefix lib/, \ BYTERUN:=$(addprefix kernel/byterun/, \ coq_fix_code.o coq_memory.o coq_values.o coq_interp.o ) -KERNEL:=$(addprefix kernel/, \ +KERNEL0:=$(addprefix kernel/, \ names.cmo univ.cmo esubst.cmo term.cmo \ mod_subst.cmo sign.cmo cbytecodes.cmo copcodes.cmo \ - cemitcodes.cmo vm.cmo declarations.cmo \ + cemitcodes.cmo declarations.cmo \ retroknowledge.cmo pre_env.cmo cbytegen.cmo environ.cmo \ - csymtable.cmo conv_oracle.cmo closure.cmo reduction.cmo \ + conv_oracle.cmo closure.cmo reduction.cmo \ type_errors.cmo entries.cmo modops.cmo inductive.cmo \ - vconv.cmo typeops.cmo indtypes.cmo cooking.cmo \ + typeops.cmo indtypes.cmo cooking.cmo \ term_typing.cmo subtyping.cmo mod_typing.cmo safe_typing.cmo ) +KERNEL1:=$(addprefix kernel/, vm.cmo csymtable.cmo vconv.cmo ) + +KERNEL:=$(KERNEL0) $(KERNEL1) + LIBRARY:=$(addprefix library/, \ nameops.cmo libnames.cmo libobject.cmo summary.cmo \ nametab.cmo global.cmo lib.cmo declaremods.cmo \ @@ -223,7 +227,7 @@ TOPLEVEL:=\ 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 $(REVISIONCMO) toplevel/usage.cmo \ + toplevel/toplevel.cmo toplevel/usage.cmo \ toplevel/coqinit.cmo toplevel/coqtop.cmo HIGHTACTICS:=$(addprefix tactics/, \ @@ -311,7 +315,7 @@ COQENVCMO:=$(CONFIG) \ COQMKTOPCMO:=$(COQENVCMO) scripts/tolink.cmo scripts/coqmktop.cmo COQMKTOPCMX:=$(COQMKTOPCMO:.cmo=.cmx) -COQCCMO:=$(COQENVCMO) $(REVISIONCMO) toplevel/usage.cmo scripts/coqc.cmo +COQCCMO:=$(COQENVCMO) toplevel/usage.cmo scripts/coqc.cmo COQCCMX:=$(COQCCMO:.cmo=.cmx) ## Pcoq tools : coq-interface, coq-parser @@ -380,13 +384,7 @@ GRAMMARNEEDEDCMO:=\ $(addprefix lib/, \ pp_control.cmo pp.cmo compat.cmo flags.cmo util.cmo \ bigint.cmo dyn.cmo hashcons.cmo predicate.cmo rtree.cmo option.cmo ) \ - $(addprefix kernel/, \ - names.cmo univ.cmo esubst.cmo term.cmo mod_subst.cmo sign.cmo \ - cbytecodes.cmo copcodes.cmo cemitcodes.cmo declarations.cmo \ - retroknowledge.cmo pre_env.cmo cbytegen.cmo conv_oracle.cmo \ - environ.cmo closure.cmo reduction.cmo type_errors.cmo entries.cmo \ - modops.cmo inductive.cmo typeops.cmo indtypes.cmo cooking.cmo \ - term_typing.cmo subtyping.cmo mod_typing.cmo safe_typing.cmo ) \ + $(KERNEL0) \ $(addprefix library/, \ nameops.cmo libnames.cmo summary.cmo nametab.cmo libobject.cmo \ lib.cmo goptions.cmo decl_kinds.cmo global.cmo ) \ @@ -405,7 +403,7 @@ CAMLP4EXTENSIONSCMO:=\ GRAMMARSCMO:=$(addprefix parsing/, \ g_prim.cmo g_tactic.cmo g_ltac.cmo g_constr.cmo ) -GRAMMARCMO:=config/coq_config.cmo $(GRAMMARNEEDEDCMO) $(CAMLP4EXTENSIONSCMO) $(GRAMMARSCMO) +GRAMMARCMO:=$(CONFIG) $(GRAMMARNEEDEDCMO) $(CAMLP4EXTENSIONSCMO) $(GRAMMARSCMO) GRAMMARCMA:=parsing/grammar.cma @@ -420,14 +418,8 @@ STAGE1_CMO:=$(GRAMMARCMO) parsing/q_constr.cmo STAGE1:=parsing/grammar.cma parsing/q_constr.cmo PRINTERSCMO:=\ - config/coq_config.cmo lib/lib.cma \ - $(addprefix kernel/, \ - names.cmo univ.cmo esubst.cmo term.cmo mod_subst.cmo sign.cmo \ - cbytecodes.cmo copcodes.cmo cemitcodes.cmo declarations.cmo \ - retroknowledge.cmo pre_env.cmo cbytegen.cmo conv_oracle.cmo \ - environ.cmo closure.cmo reduction.cmo type_errors.cmo entries.cmo \ - modops.cmo inductive.cmo typeops.cmo indtypes.cmo cooking.cmo \ - term_typing.cmo subtyping.cmo mod_typing.cmo safe_typing.cmo ) \ + $(CONFIG) lib/lib.cma \ + $(KERNEL0) \ $(addprefix library/, \ summary.cmo global.cmo nameops.cmo libnames.cmo nametab.cmo \ libobject.cmo lib.cmo goptions.cmo decls.cmo heads.cmo ) \ @@ -777,10 +769,6 @@ MANPAGES:=man/coq-tex.1 man/coqdep.1 man/gallina.1 \ PCOQMANPAGES:=man/coq-interface.1 man/coq-parser.1 -RECTYPESML:=kernel/term.ml library/nametab.ml proofs/tacexpr.ml \ - parsing/pptactic.ml - - ######################################################### # .mli files by directory (used for dependencies graphs # ######################################################### -- cgit v1.2.3