From c051f623926cdc3b744c38ba393c0a9c7622d299 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 31 Jan 2006 09:57:33 +0000 Subject: [PATCH] some makefile work --- helm/ocaml/Makefile.common.in | 36 +++++++++++-------- helm/ocaml/Makefile.in | 13 ++++--- helm/ocaml/cic_disambiguation/Makefile | 9 +++-- helm/ocaml/cic_proof_checking/Makefile | 9 +++-- .../cic_proof_checking/utilities/Makefile | 8 +++-- helm/ocaml/content_pres/Makefile | 3 +- helm/ocaml/grafite_parser/Makefile | 9 +++-- helm/ocaml/metadata/Makefile | 18 ++++++---- helm/ocaml/metadata/extractor/Makefile | 14 +++++--- helm/ocaml/metadata/table_creator/Makefile | 12 ++++--- helm/ocaml/tactics/.depend | 21 ++++++----- helm/ocaml/tactics/paramodulation/Makefile | 8 +++-- helm/ocaml/tactics/paramodulation/indexing.ml | 22 +++++++++--- .../tactics/paramodulation/saturation.ml | 32 +++++++++++++++++ helm/ocaml/thread/Makefile | 9 +++-- helm/ocaml/utf8_macros/Makefile | 12 ++++--- 16 files changed, 166 insertions(+), 69 deletions(-) diff --git a/helm/ocaml/Makefile.common.in b/helm/ocaml/Makefile.common.in index da539d460..2dc345235 100644 --- a/helm/ocaml/Makefile.common.in +++ b/helm/ocaml/Makefile.common.in @@ -1,3 +1,5 @@ +H=@ + # This Makefile must be included by another one defining: # $PACKAGE # $PREDICATES @@ -29,11 +31,13 @@ OCAMLOPT_P4 = $(OCAMLFIND) opt $(OCAMLOPTIONS) $(SYNTAXOPTIONS) LIBRARIES = $(shell $(OCAMLFIND) query -recursive -predicates "byte $(PREDICATES)" -format "%d/%a" $(REQUIRES)) LIBRARIES_OPT = $(shell $(OCAMLFIND) query -recursive -predicates "native $(PREDICATES)" -format "%d/%a" $(REQUIRES)) -LIBRARIES_DEPS = $(foreach X,$(LIBRARIES),$(wildcard \ - $(shell dirname $(X))/*.mli \ - $(shell dirname $(X))/*.ml \ - $(shell dirname $(X))/*/*.ml \ - $(shell dirname $(X))/*/*.mli)) +LIBRARIES_DEPS = \ + $(foreach X,$(filter-out /usr/lib/ocaml%,$(LIBRARIES)),\ + $(wildcard \ + $(shell dirname $(X))/*.mli \ + $(shell dirname $(X))/*.ml \ + $(shell dirname $(X))/paramodulation/*.ml \ + $(shell dirname $(X))/paramodultation/*.mli)) ARCHIVE = $(PACKAGE).cma @@ -44,20 +48,22 @@ OBJECTS_TO_INSTALL = $(ARCHIVE) $(ARCHIVE_OPT) $(ARCHIVE_OPT:%.cmxa=%.a) \ DEPEND_FILES = $(INTERFACE_FILES) $(IMPLEMENTATION_FILES) $(ARCHIVE): $(IMPLEMENTATION_FILES:%.ml=%.cmo) $(LIBRARIES) - @if [ $(PACKAGE) != dummy ]; then \ - echo OCAMLC $@;\ + $(H)if [ $(PACKAGE) != dummy ]; then \ + echo " OCAMLC -a $@";\ $(OCAMLC) $(OCAMLARCHIVEOPTIONS) -a -o $@ \ $(IMPLEMENTATION_FILES:%.ml=%.cmo); fi $(ARCHIVE_OPT): $(IMPLEMENTATION_FILES:%.ml=%.cmx) $(LIBRARIES_OPT) - @if [ $(PACKAGE) != dummy ]; then \ - echo OCAMLOPT $@;\ + $(H)if [ $(PACKAGE) != dummy ]; then \ + echo " OCAMLOPT -a $@";\ $(OCAMLOPT) $(OCAMLARCHIVEOPTIONS) -a -o $@ \ $(IMPLEMENTATION_FILES:%.ml=%.cmx); fi prereq: $(PREREQ) all: prereq $(IMPLEMENTATION_FILES:%.ml=%.cmo) $(ARCHIVE) + @echo -n opt: prereq $(IMPLEMENTATION_FILES:%.ml=%.cmx) $(ARCHIVE_OPT) + @echo -n world: all opt test: test.ml $(ARCHIVE) $(OCAMLC) $(ARCHIVE) -linkpkg -o $@ $< @@ -74,14 +80,14 @@ $(PACKAGE).ps: .dep.dot ocamldot < .depend > $@ %.cmi: %.mli - @echo OCAMLC $< - @$(OCAMLC) -c $< + @echo " OCAMLC $<" + $(H)$(OCAMLC) -c $< %.cmo %.cmi: %.ml - @echo OCAMLC $< - @$(OCAMLC) -c $< + @echo " OCAMLC $<" + $(H)$(OCAMLC) -c $< %.cmx: %.ml - @echo OCAMLOPT $< - @$(OCAMLOPT) -c $< + @echo " OCAMLOPT $<" + $(H)$(OCAMLOPT) -c $< %.annot: %.ml $(OCAMLC) -dtypes $(PKGS) -c $< %.ml %.mli: %.mly diff --git a/helm/ocaml/Makefile.in b/helm/ocaml/Makefile.in index 19624a460..2b1783b3c 100644 --- a/helm/ocaml/Makefile.in +++ b/helm/ocaml/Makefile.in @@ -57,14 +57,19 @@ distclean: clean clean_metas .PHONY: all opt world metas depend install uninstall clean clean_metas distclean %.all: - @OCAMLPATH=$(OCAMLPATH):$$OCAMLPATH $(MAKE) -C $* all + @echo building module: $* + @OCAMLPATH=$(OCAMLPATH):$$OCAMLPATH $(MAKE) -C $* all --no-print-directory %.opt: - @OCAMLPATH=$(OCAMLPATH):$$OCAMLPATH $(MAKE) -C $* opt + @echo building module: $* + @OCAMLPATH=$(OCAMLPATH):$$OCAMLPATH $(MAKE) -C $* opt --no-print-directory %.clean: - @OCAMLPATH=$(OCAMLPATH):$$OCAMLPATH $(MAKE) -C $* clean + @echo cleaning module: $* + @OCAMLPATH=$(OCAMLPATH):$$OCAMLPATH $(MAKE) -C $* clean --no-print-directory %.depend: - @OCAMLPATH=$(OCAMLPATH):$$OCAMLPATH $(MAKE) -C $* depend + @echo calculating dependencies for module: $* + @OCAMLPATH=$(OCAMLPATH):$$OCAMLPATH $(MAKE) -C $* depend --no-print-directory %.stats: + @echo generating stats for module: $* @$(MAKE) -C $* .stats $(MODULES:%=%.install): diff --git a/helm/ocaml/cic_disambiguation/Makefile b/helm/ocaml/cic_disambiguation/Makefile index 729590da5..9c231dd87 100644 --- a/helm/ocaml/cic_disambiguation/Makefile +++ b/helm/ocaml/cic_disambiguation/Makefile @@ -19,9 +19,12 @@ include ../Makefile.common OCAMLARCHIVEOPTIONS += -linkall disambiguateTypes.cmi: disambiguateTypes.mli - $(OCAMLC) -c -rectypes $< + @echo " OCAMLC -rectypes $<" + @$(OCAMLC) -c -rectypes $< disambiguateTypes.cmo: disambiguateTypes.ml disambiguateTypes.cmi - $(OCAMLC) -c -rectypes $< + @echo " OCAMLC -rectypes $<" + @$(OCAMLC) -c -rectypes $< disambiguateTypes.cmx: disambiguateTypes.ml disambiguateTypes.cmi - $(OCAMLOPT) -c -rectypes $< + @echo " OCAMLOPT -rectypes $<" + @$(OCAMLOPT) -c -rectypes $< diff --git a/helm/ocaml/cic_proof_checking/Makefile b/helm/ocaml/cic_proof_checking/Makefile index 28462e58e..c81573f51 100644 --- a/helm/ocaml/cic_proof_checking/Makefile +++ b/helm/ocaml/cic_proof_checking/Makefile @@ -32,11 +32,14 @@ all: all_utilities opt: opt_utilities all_utilities: - $(MAKE) -C utilities/ all + @echo " building: utilities" + @$(MAKE) -C utilities/ all --no-print-directory opt_utilities: - $(MAKE) -C utilities/ opt + @echo " building: utilities" + @$(MAKE) -C utilities/ opt --no-print-directory clean: clean_utilities clean_utilities: - $(MAKE) -C utilities/ clean + @echo " cleaning: utilities" + @$(MAKE) -C utilities/ clean --no-print-directory diff --git a/helm/ocaml/cic_proof_checking/utilities/Makefile b/helm/ocaml/cic_proof_checking/utilities/Makefile index 2cd98f894..174546634 100644 --- a/helm/ocaml/cic_proof_checking/utilities/Makefile +++ b/helm/ocaml/cic_proof_checking/utilities/Makefile @@ -5,11 +5,15 @@ LIBS = helm-cic_proof_checking OCAMLC = ocamlfind ocamlc $(LINKOPTS) -package $(LIBS) OCAMLOPT = ocamlfind opt $(LINKOPTS) -package $(LIBS) all: $(UTILITIES) + @echo -n opt: $(UTILITIES_OPT) + @echo -n %: %.ml - $(OCAMLC) -o $@ $< + @echo " OCAMLC $<" + @$(OCAMLC) -o $@ $< %.opt: %.ml - $(OCAMLOPT) -o $@ $< + @echo " OCAMLOPT $<" + @$(OCAMLOPT) -o $@ $< clean: rm -f $(UTILITIES) $(UTILITIES_OPT) *.cm[iox] *.o diff --git a/helm/ocaml/content_pres/Makefile b/helm/ocaml/content_pres/Makefile index 642e3ce0e..459b793f0 100644 --- a/helm/ocaml/content_pres/Makefile +++ b/helm/ocaml/content_pres/Makefile @@ -27,7 +27,8 @@ clean: clean_tests LOCAL_LINKOPTS = -package helm-content_pres -linkpkg test: test_lexer test_lexer: test_lexer.ml $(PACKAGE).cma - $(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $< + @echo " OCAMLC $<" + @$(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $< clean_tests: rm -f test_lexer{,.opt} diff --git a/helm/ocaml/grafite_parser/Makefile b/helm/ocaml/grafite_parser/Makefile index 4b04b597e..25896da87 100644 --- a/helm/ocaml/grafite_parser/Makefile +++ b/helm/ocaml/grafite_parser/Makefile @@ -33,10 +33,13 @@ clean_tests: LOCAL_LINKOPTS = -package helm-$(PACKAGE) -linkpkg test: test_parser print_grammar test_dep test_parser: test_parser.ml $(PACKAGE).cma - $(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $< + @echo " OCAMLC $<" + @$(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $< print_grammar: print_grammar.ml $(PACKAGE).cma - $(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $< + @echo " OCAMLC $<" + @$(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $< test_dep: test_dep.ml $(PACKAGE).cma - $(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $< + @echo " OCAMLC $<" + @$(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $< include ../Makefile.common diff --git a/helm/ocaml/metadata/Makefile b/helm/ocaml/metadata/Makefile index 29ca2d3bc..80dc4133e 100644 --- a/helm/ocaml/metadata/Makefile +++ b/helm/ocaml/metadata/Makefile @@ -18,20 +18,26 @@ all: all_table_creator all_extractor opt: opt_table_creator opt_extractor all_table_creator: - make -C table_creator/ all + @echo " building: table_creator" + @make -C table_creator/ all --no-print-directory opt_table_creator: - make -C table_creator/ opt + @echo " building: table_creator" + @make -C table_creator/ opt --no-print-directory all_extractor: - make -C extractor/ all + @echo " building: extractor" + @make -C extractor/ all --no-print-directory opt_extractor: - make -C extractor/ opt + @echo " building: extractor" + @make -C extractor/ opt --no-print-directory clean: clean_table_creator clean_extractor clean_table_creator: - make -C table_creator/ clean + @echo " cleaning: table_creator" + @make -C table_creator/ clean --no-print-directory clean_extractor: - make -C extractor/ clean + @echo " cleaning: extractor" + @make -C extractor/ clean --no-print-directory diff --git a/helm/ocaml/metadata/extractor/Makefile b/helm/ocaml/metadata/extractor/Makefile index e58064b41..7c2aec0e5 100644 --- a/helm/ocaml/metadata/extractor/Makefile +++ b/helm/ocaml/metadata/extractor/Makefile @@ -1,25 +1,31 @@ OCAMLFIND=ocamlfind all: extractor extractor_manager + @echo -n opt: extractor.opt extractor_manager.opt + @echo -n clean: rm -f *.cm[ixo] *.[ao] extractor extractor.opt *.err *.out extractor_manager extractor_manager.opt extractor: extractor.ml - $(OCAMLFIND) ocamlc \ + @echo " OCAMLC $<" + @$(OCAMLFIND) ocamlc \ -thread -package mysql,helm-metadata -linkpkg -o $@ $< extractor.opt: extractor.ml - $(OCAMLFIND) ocamlopt \ + @echo " OCAMLOPT $<" + @$(OCAMLFIND) ocamlopt \ -thread -package mysql,helm-metadata -linkpkg -o $@ $< extractor_manager: extractor_manager.ml - $(OCAMLFIND) ocamlc \ + @echo " OCAMLC $<" + @$(OCAMLFIND) ocamlc \ -thread -package mysql,helm-metadata -linkpkg -o $@ $< extractor_manager.opt: extractor_manager.ml - $(OCAMLFIND) ocamlopt \ + @echo " OCAMLOPT $<" + @$(OCAMLFIND) ocamlopt \ -thread -package mysql,helm-metadata -linkpkg -o $@ $< export: extractor.opt extractor_manager.opt diff --git a/helm/ocaml/metadata/table_creator/Makefile b/helm/ocaml/metadata/table_creator/Makefile index cb8ab7636..06335681c 100644 --- a/helm/ocaml/metadata/table_creator/Makefile +++ b/helm/ocaml/metadata/table_creator/Makefile @@ -8,21 +8,25 @@ EXTRA_OBJECTS_TO_CLEAN = \ table_creator table_creator.opt table_destructor table_destructor.opt all: table_creator table_destructor + @echo -n opt: table_creator.opt table_destructor.opt + @echo -n table_creator: table_creator.ml ../metadata.cma - $(OCAMLFIND) ocamlc \ + @echo " OCAMLC $<" + @$(OCAMLFIND) ocamlc \ -thread -package mysql,helm-metadata -linkpkg -o $@ $< table_destructor: table_creator - ln -f $< $@ + @ln -f $< $@ table_creator.opt: table_creator.ml ../metadata.cmxa - $(OCAMLFIND) ocamlopt \ + @echo " OCAMLOPT $<" + @$(OCAMLFIND) ocamlopt \ -thread -package mysql,helm-metadata -linkpkg -o $@ $< table_destructor.opt: table_creator.opt - ln -f $< $@ + @ln -f $< $@ clean: rm -f *.cm[iox] *.a *.o diff --git a/helm/ocaml/tactics/.depend b/helm/ocaml/tactics/.depend index dd623b9ae..6ad9ccf25 100644 --- a/helm/ocaml/tactics/.depend +++ b/helm/ocaml/tactics/.depend @@ -6,7 +6,6 @@ proofEngineStructuralRules.cmi: proofEngineTypes.cmi primitiveTactics.cmi: proofEngineTypes.cmi metadataQuery.cmi: proofEngineTypes.cmi paramodulation/inference.cmi: proofEngineTypes.cmi -paramodulation/indexing.cmi: proofEngineTypes.cmi paramodulation/saturation.cmi: proofEngineTypes.cmi variousTactics.cmi: proofEngineTypes.cmi autoTactic.cmi: proofEngineTypes.cmi @@ -51,22 +50,22 @@ metadataQuery.cmo: proofEngineTypes.cmi primitiveTactics.cmi \ hashtbl_equiv.cmi metadataQuery.cmi metadataQuery.cmx: proofEngineTypes.cmx primitiveTactics.cmx \ hashtbl_equiv.cmx metadataQuery.cmi -paramodulation/utils.cmo: paramodulation/utils.cmi -paramodulation/utils.cmx: paramodulation/utils.cmi +paramodulation/utils.cmo: proofEngineReduction.cmi paramodulation/utils.cmi +paramodulation/utils.cmx: proofEngineReduction.cmx paramodulation/utils.cmi paramodulation/inference.cmo: proofEngineReduction.cmi proofEngineHelpers.cmi \ metadataQuery.cmi paramodulation/inference.cmi paramodulation/inference.cmx: proofEngineReduction.cmx proofEngineHelpers.cmx \ metadataQuery.cmx paramodulation/inference.cmi paramodulation/equality_indexing.cmo: paramodulation/equality_indexing.cmi paramodulation/equality_indexing.cmx: paramodulation/equality_indexing.cmi -paramodulation/indexing.cmo: proofEngineTypes.cmi primitiveTactics.cmi \ - paramodulation/indexing.cmi -paramodulation/indexing.cmx: proofEngineTypes.cmx primitiveTactics.cmx \ - paramodulation/indexing.cmi -paramodulation/saturation.cmo: proofEngineTypes.cmi proofEngineReduction.cmi \ - primitiveTactics.cmi paramodulation/saturation.cmi -paramodulation/saturation.cmx: proofEngineTypes.cmx proofEngineReduction.cmx \ - primitiveTactics.cmx paramodulation/saturation.cmi +paramodulation/indexing.cmo: paramodulation/indexing.cmi +paramodulation/indexing.cmx: paramodulation/indexing.cmi +paramodulation/saturation.cmo: reductionTactics.cmi proofEngineTypes.cmi \ + proofEngineReduction.cmi primitiveTactics.cmi \ + paramodulation/saturation.cmi +paramodulation/saturation.cmx: reductionTactics.cmx proofEngineTypes.cmx \ + proofEngineReduction.cmx primitiveTactics.cmx \ + paramodulation/saturation.cmi variousTactics.cmo: tacticals.cmi proofEngineTypes.cmi \ proofEngineReduction.cmi proofEngineHelpers.cmi primitiveTactics.cmi \ variousTactics.cmi diff --git a/helm/ocaml/tactics/paramodulation/Makefile b/helm/ocaml/tactics/paramodulation/Makefile index 880b95953..ba8bd40aa 100644 --- a/helm/ocaml/tactics/paramodulation/Makefile +++ b/helm/ocaml/tactics/paramodulation/Makefile @@ -5,12 +5,16 @@ LOCALLINKOPTS = -package helm-cic_disambiguation,helm-content_pres,helm-grafite, include ../../Makefile.common all $(PACKAGE).cma :saturate + @echo -n opt $(PACKAGE).cmxa:saturate.opt + @echo -n saturate: saturate_main.ml $(LIBRARIES) - $(OCAMLC) $(LOCALLINKOPTS) -thread -linkpkg -o $@ $< + @echo " OCAMLC $<" + @$(OCAMLC) $(LOCALLINKOPTS) -thread -linkpkg -o $@ $< saturate.opt: saturate_main.ml $(LIBRARIES) - $(OCAMLOPT) $(LOCALLINKOPTS) -thread -linkpkg -o $@ $< + @echo " OCAMLOPT $<" + @$(OCAMLOPT) $(LOCALLINKOPTS) -thread -linkpkg -o $@ $< clean: rm -f saturate saturate.opt diff --git a/helm/ocaml/tactics/paramodulation/indexing.ml b/helm/ocaml/tactics/paramodulation/indexing.ml index 207fb9433..8ffde4bdf 100644 --- a/helm/ocaml/tactics/paramodulation/indexing.ml +++ b/helm/ocaml/tactics/paramodulation/indexing.ml @@ -130,7 +130,6 @@ let rec find_matches metasenv context ugraph lift_amount term termty = let module M = CicMetaSubst in let module HL = HelmLibraryObjects in let cmp = !Utils.compare_terms in - ignore(CicTypeChecker.type_of_aux' metasenv context term); let check = match termty with C.Implicit None -> false | _ -> true in function | [] -> None @@ -157,7 +156,8 @@ let rec find_matches metasenv context ugraph lift_amount term termty = match_unif_time_no := !match_unif_time_no +. (t2 -. t1); raise e | CicUtil.Meta_not_found _ as exn -> - prerr_endline "siam qua"; raise exn + prerr_endline "zurg"; + raise exn in Some (C.Rel (1 + lift_amount), subst', metasenv', ugraph', (candidate, eq_URI)) @@ -354,7 +354,7 @@ let rec demodulation_aux ?(typecheck=false) let module S = CicSubstitution in let module M = CicMetaSubst in let module HL = HelmLibraryObjects in - let candidates = get_candidates Matching table term in + let candidates = get_candidates Matching table term in match term with | C.Meta _ -> None | term -> @@ -546,6 +546,19 @@ let rec demodulation_equality newmeta env table sign target = in !maxmeta, res in + let _ = + try + CicTypeChecker.type_of_aux' metasenv' context left ugraph; + CicTypeChecker.type_of_aux' metasenv' context right ugraph; + with + CicUtil.Meta_not_found _ as exn -> + begin + prerr_endline "siamo in demodulation_equality 1"; + prerr_endline (CicPp.ppterm left); + prerr_endline (CicPp.ppterm right); + raise exn + end + in let res = demodulation_aux metasenv' context ugraph table 0 left in let newmeta, newtarget = match res with @@ -949,7 +962,8 @@ let rec demodulation_goal newmeta env table goal = bo, Inference.ProofGoalBlock (Inference.NoProof, goal_proof) in let m = Inference.metas_of_term newterm in - let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) (metas @ menv')in + (* QUA *) + let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) (menv @ menv')in !maxmeta, (newproof, newmetasenv, newterm) in let res = diff --git a/helm/ocaml/tactics/paramodulation/saturation.ml b/helm/ocaml/tactics/paramodulation/saturation.ml index 07fbaa41c..9c4dce460 100644 --- a/helm/ocaml/tactics/paramodulation/saturation.ml +++ b/helm/ocaml/tactics/paramodulation/saturation.ml @@ -483,6 +483,22 @@ let forward_simplify env (sign, current) ?passive (active_list, active_table) = let demodulate table current = let newmeta, newcurrent = + let _ = + let w, proof, (eq_ty, left, right, order), metas, args = current in + let metasenv, context, ugraph = env in + let metasenv' = metasenv @ metas in + try + CicTypeChecker.type_of_aux' metasenv' context left ugraph; + CicTypeChecker.type_of_aux' metasenv' context right ugraph; + with + CicUtil.Meta_not_found _ as exn -> + begin + prerr_endline "siamo in forward_simplify"; + prerr_endline (CicPp.ppterm left); + prerr_endline (CicPp.ppterm right); + raise exn + end + in Indexing.demodulation_equality !maxmeta env table sign current in maxmeta := newmeta; if is_identity env newcurrent then @@ -568,6 +584,22 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active = let demodulate sign table target = let newmeta, newtarget = + let _ = + let w, proof, (eq_ty, left, right, order), metas, args = target in + let metasenv, context, ugraph = env in + let metasenv' = metasenv @ metas in + try + CicTypeChecker.type_of_aux' metasenv' context left ugraph; + CicTypeChecker.type_of_aux' metasenv' context right ugraph; + with + CicUtil.Meta_not_found _ as exn -> + begin + prerr_endline "siamo in forward_simplify_new"; + prerr_endline (CicPp.ppterm left); + prerr_endline (CicPp.ppterm right); + raise exn + end + in Indexing.demodulation_equality !maxmeta env table sign target in maxmeta := newmeta; newtarget diff --git a/helm/ocaml/thread/Makefile b/helm/ocaml/thread/Makefile index 24a96b6e9..db722abaa 100644 --- a/helm/ocaml/thread/Makefile +++ b/helm/ocaml/thread/Makefile @@ -9,14 +9,17 @@ opt: thread_fake.cmxa include ../Makefile.common fake/threadSafe.cmi: fake/threadSafe.mli - cd fake/ \ + @echo " OCAMLC $<" + @cd fake/ \ && ocamlfind ocamlc -c threadSafe.mli thread_fake.cma: fake/threadSafe.cmi - cd fake/ \ + @echo " OCAMLC -a $@" + @cd fake/ \ && ocamlfind ocamlc -a -o $@ threadSafe.ml \ && cp $@ ../ thread_fake.cmxa: fake/threadSafe.cmi - cd fake/ \ + @echo " OCAMLOPT -a $@" + @cd fake/ \ && ocamlfind opt -a -o $@ threadSafe.ml \ && cp $@ ../ diff --git a/helm/ocaml/utf8_macros/Makefile b/helm/ocaml/utf8_macros/Makefile index 018f58cef..952b9f597 100644 --- a/helm/ocaml/utf8_macros/Makefile +++ b/helm/ocaml/utf8_macros/Makefile @@ -11,17 +11,21 @@ EXTRA_OBJECTS_TO_CLEAN = all: utf8_macros.cma pa_unicode_macro.cma make_table: make_table.ml - $(OCAMLFIND) ocamlc -package $(MAKE_TABLE_PACKAGES) -linkpkg -o $@ $^ + @echo " OCAMLC $<" + @$(OCAMLFIND) ocamlc -package $(MAKE_TABLE_PACKAGES) -linkpkg -o $@ $^ utf8MacroTable.ml: ./make_table $@ utf8MacroTable.cmo: utf8MacroTable.ml - $(OCAMLFIND) ocamlc -c $< + @echo " OCAMLC $<" + @$(OCAMLFIND) ocamlc -c $< pa_unicode_macro.cmo: pa_unicode_macro.ml utf8Macro.cmo - $(OCAMLFIND) ocamlc -package camlp4 -pp "camlp4o q_MLast.cmo pa_extend.cmo -loc loc" -c $< + @echo " OCAMLC $<" + @$(OCAMLFIND) ocamlc -package camlp4 -pp "camlp4o q_MLast.cmo pa_extend.cmo -loc loc" -c $< pa_unicode_macro.cma: utf8MacroTable.cmo utf8Macro.cmo pa_unicode_macro.cmo - $(OCAMLFIND) ocamlc -a -o $@ $^ + @echo " OCAMLC -a $@" + @$(OCAMLFIND) ocamlc -a -o $@ $^ .PHONY: test test: test.ml -- 2.39.2