diff options
| author | Jason Gross | 2020-04-29 18:27:04 -0400 |
|---|---|---|
| committer | Jason Gross | 2020-04-29 18:35:04 -0400 |
| commit | 8bd559370f51d7cc1877380a5ad726da67ceb0fa (patch) | |
| tree | 06153261c61b426088714931099f72ccf740aa93 | |
| parent | 5e611ecb1c38860ee5aaa0ccde1bb982ccc43ae4 (diff) | |
When TIMED=1, emit timing info for OCaml files
| -rw-r--r-- | Makefile.build | 4 | ||||
| -rw-r--r-- | doc/changelog/08-tools/12211-time-ocaml.rst | 5 | ||||
| -rw-r--r-- | tools/CoqMakefile.in | 24 |
3 files changed, 19 insertions, 14 deletions
diff --git a/Makefile.build b/Makefile.build index b7a4dd655a..cf9141853d 100644 --- a/Makefile.build +++ b/Makefile.build @@ -249,8 +249,8 @@ MLINCLUDES=$(LOCALINCLUDES) USERCONTRIBINCLUDES=$(addprefix -I user-contrib/,$(USERCONTRIBDIRS)) -OCAMLC := $(OCAMLFIND) ocamlc $(CAMLFLAGS) -OCAMLOPT := $(OCAMLFIND) opt $(CAMLFLAGS) +OCAMLC := $(TIMER) $(OCAMLFIND) ocamlc $(CAMLFLAGS) +OCAMLOPT := $(TIMER) $(OCAMLFIND) opt $(CAMLFLAGS) BYTEFLAGS=$(CAMLDEBUG) $(USERFLAGS) OPTFLAGS=$(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS) $(FLAMBDA_FLAGS) diff --git a/doc/changelog/08-tools/12211-time-ocaml.rst b/doc/changelog/08-tools/12211-time-ocaml.rst new file mode 100644 index 0000000000..7ff68cc495 --- /dev/null +++ b/doc/changelog/08-tools/12211-time-ocaml.rst @@ -0,0 +1,5 @@ +- **Changed:** + When passing ``TIMED=1`` to ``make`` with either Coq's own makefile + or a ``coq_makefile``\-made makefile, timing information is now + printed for OCaml files as well (`#12211 + <https://github.com/coq/coq/pull/12211>`_, by Jason Gross). diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 57ba036a62..a26eb9dfbe 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -647,7 +647,7 @@ archclean:: $(MLIFILES:.mli=.cmi): %.cmi: %.mli $(SHOW)'CAMLC -c $<' - $(HIDE)$(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $< + $(HIDE)$(TIMER) $(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $< $(MLGFILES:.mlg=.ml): %.ml: %.mlg $(SHOW)'COQPP $<' @@ -656,53 +656,53 @@ $(MLGFILES:.mlg=.ml): %.ml: %.mlg # Stupid hack around a deficient syntax: we cannot concatenate two expansions $(filter %.cmo, $(MLFILES:.ml=.cmo) $(MLGFILES:.mlg=.cmo)): %.cmo: %.ml $(SHOW)'CAMLC -c $<' - $(HIDE)$(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $< + $(HIDE)$(TIMER) $(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $< # Same hack $(filter %.cmx, $(MLFILES:.ml=.cmx) $(MLGFILES:.mlg=.cmx)): %.cmx: %.ml $(SHOW)'CAMLOPT -c $(FOR_PACK) $<' - $(HIDE)$(CAMLOPTC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $(FOR_PACK) $< + $(HIDE)$(TIMER) $(CAMLOPTC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $(FOR_PACK) $< $(MLLIBFILES:.mllib=.cmxs): %.cmxs: %.cmxa $(SHOW)'CAMLOPT -shared -o $@' - $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \ + $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \ -linkall -shared -o $@ $< $(MLLIBFILES:.mllib=.cma): %.cma: | %.mllib $(SHOW)'CAMLC -a -o $@' - $(HIDE)$(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^ + $(HIDE)$(TIMER) $(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^ $(MLLIBFILES:.mllib=.cmxa): %.cmxa: | %.mllib $(SHOW)'CAMLOPT -a -o $@' - $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -a -o $@ $^ + $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -a -o $@ $^ $(MLPACKFILES:.mlpack=.cmxs): %.cmxs: %.cmxa $(SHOW)'CAMLOPT -shared -o $@' - $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \ + $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \ -shared -linkall -o $@ $< $(MLPACKFILES:.mlpack=.cmxa): %.cmxa: %.cmx $(SHOW)'CAMLOPT -a -o $@' - $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -a -o $@ $< + $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -a -o $@ $< $(MLPACKFILES:.mlpack=.cma): %.cma: %.cmo | %.mlpack $(SHOW)'CAMLC -a -o $@' - $(HIDE)$(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^ + $(HIDE)$(TIMER) $(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^ $(MLPACKFILES:.mlpack=.cmo): %.cmo: | %.mlpack $(SHOW)'CAMLC -pack -o $@' - $(HIDE)$(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) -pack -o $@ $^ + $(HIDE)$(TIMER) $(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) -pack -o $@ $^ $(MLPACKFILES:.mlpack=.cmx): %.cmx: | %.mlpack $(SHOW)'CAMLOPT -pack -o $@' - $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -pack -o $@ $^ + $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -pack -o $@ $^ # This rule is for _CoqProject with no .mllib nor .mlpack $(filter-out $(MLLIBFILES:.mllib=.cmxs) $(MLPACKFILES:.mlpack=.cmxs) $(addsuffix .cmxs,$(PACKEDFILES)) $(addsuffix .cmxs,$(LIBEDFILES)),$(MLFILES:.ml=.cmxs) $(MLGFILES:.mlg=.cmxs)): %.cmxs: %.cmx $(SHOW)'[deprecated,use-mllib-or-mlpack] CAMLOPT -shared -o $@' - $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \ + $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \ -shared -o $@ $< ifneq (,$(TIMING)) |