diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2022-01-05 15:22:22 +0100 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2022-01-05 15:22:22 +0100 |
| commit | 1c264a258be01623b8936657a32f2251ca2059c1 (patch) | |
| tree | a6c707ef97373ca91b0f476fd3b9ab1ee47fb073 /Makefile.extr | |
| parent | 89562c917e61c56a167ba13b86021b286cb7e257 (diff) | |
| download | compcert-kvx-1c264a258be01623b8936657a32f2251ca2059c1.tar.gz compcert-kvx-1c264a258be01623b8936657a32f2251ca2059c1.zip | |
ccomp profiling
Diffstat (limited to 'Makefile.extr')
| -rw-r--r-- | Makefile.extr | 43 |
1 files changed, 41 insertions, 2 deletions
diff --git a/Makefile.extr b/Makefile.extr index 6106aff2..0d2ec61f 100644 --- a/Makefile.extr +++ b/Makefile.extr @@ -77,6 +77,9 @@ endif OCAMLC=ocamlc$(DOTOPT) $(COMPFLAGS) OCAMLOPT=ocamlopt$(DOTOPT) $(COMPFLAGS) OCAMLDEP=ocamldep$(DOTOPT) -slash $(INCLUDES) +OCAMLFIND=ocamlfind +LMFLAGS_LINK=-package landmarks -linkpkg +LMFLAGS_COMP=-package landmarks -package landmarks-ppx -ppxopt landmarks-ppx,--auto OCAMLLEX=ocamllex -q MODORDER=tools/modorder .depend.extr @@ -99,9 +102,15 @@ ifeq ($(wildcard .depend.extr),.depend.extr) CCOMP_OBJS:=$(shell $(MODORDER) driver/Driver.cmx) ifeq ($(OCAML_NATIVE_COMP),true) +ifeq ($(OCAML_LM_PROF), true) +ccomp: $(CCOMP_OBJS) + @echo "Linking $@ with landmarks profiling" + @$(OCAMLFIND) opt $(COMPFLAGS) -o $@ $(LMFLAGS_LINK) $(LIBS) $(LINK_OPT) $+ +else ccomp: $(CCOMP_OBJS) @echo "Linking $@" @$(OCAMLOPT) -o $@ $(LIBS) $(LINK_OPT) $+ +endif else ccomp: ccomp.byte @echo "Copying to $@" @@ -112,16 +121,28 @@ endif ccomp.force: $(OCAMLOPT) -o $@ $(LIBS) $(LINK_OPT) $(CCOMP_OBJS) +ifeq ($(OCAML_LM_PROF), true) +ccomp.byte: $(CCOMP_OBJS:.cmx=.cmo) + @echo "Linking $@ with landmarks profiling" + @$(OCAMLFIND) ocamlc $(COMPFLAGS) -o $@ $(LMFLAGS_LINK) $(LIBS_BYTE) $+ +else ccomp.byte: $(CCOMP_OBJS:.cmx=.cmo) @echo "Linking $@" @$(OCAMLC) -o $@ $(LIBS_BYTE) $+ +endif CLIGHTGEN_OBJS:=$(shell $(MODORDER) export/ExportDriver.cmx) ifeq ($(OCAML_NATIVE_COMP),true) +ifeq ($(OCAML_LM_PROF), true) +clightgen: $(CLIGHTGEN_OBJS) + @echo "Linking $@ with landmarks profiling" + @$(OCAMLFIND) opt $(COMPFLAGS) -o $@ $(LMFLAGS_LINK) $(LIBS) $(LINK_OPT) $+ +else clightgen: $(CLIGHTGEN_OBJS) @echo "Linking $@" @$(OCAMLOPT) -o $@ $(LIBS) $(LINK_OPT) $+ +endif else clightgen: clightgen.byte @echo "Copying to $@" @@ -138,15 +159,33 @@ endif # End of part that assumes .depend.extr already exists +ifeq ($(OCAML_LM_PROF), true) %.cmi: %.mli - @echo "OCAMLC $<" + @echo "OCAMLC $< with landmarks profiling" + @$(OCAMLFIND) ocamlc $(COMPFLAGS) -c $(LMFLAGS_COMP) $< +else +%.cmi: %.mli + @echo "OCAMLC $<" @$(OCAMLC) -c $< +endif +ifeq ($(OCAML_LM_PROF), true) +%.cmo: %.ml + @echo "OCAMLC $< with landmarks profiling" + @$(OCAMLFIND) ocamlc $(COMPFLAGS) -c $(LMFLAGS_COMP) $< +else %.cmo: %.ml - @echo "OCAMLC $<" + @echo "OCAMLC $<" @$(OCAMLC) -c $< +endif +ifeq ($(OCAML_LM_PROF), true) +%.cmx: %.ml + @echo "OCAMLOPT $< with landmarks profiling" + @$(OCAMLFIND) opt $(COMPFLAGS) -c $(LMFLAGS_COMP) $< +else %.cmx: %.ml @echo "OCAMLOPT $<" @$(OCAMLOPT) -c $< +endif %.ml: %.mll $(OCAMLLEX) $< |