From a19551fd50df93951d78eea4c163d434f844047c Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 3 Jan 2023 17:27:07 +0100 Subject: [PATCH] Makefiles removed in favour of dune-only solution - some Makefiles are still to be removed - some Makefiles in legacy dirs that are no longer compiled will be kept - the Makefile in help is still useful! --- matita/components/content/Makefile | 15 ------ matita/components/content_pres/Makefile | 49 ------------------ matita/components/disambiguation/Makefile | 28 ---------- ...biguate.crit2.ml => disambiguate.crit2_ml} | 0 ...biguate.crit4.ml => disambiguate.crit4_ml} | 0 matita/components/extlib/Makefile | 21 -------- matita/components/getter/Makefile | 21 -------- matita/components/grafite/Makefile | 13 ----- matita/components/grafite_engine/Makefile | 12 ----- matita/components/grafite_parser/Makefile | 29 ----------- matita/components/library/Makefile | 13 ----- matita/components/logger/Makefile | 10 ---- matita/components/ng_cic_content/Makefile | 14 ----- matita/components/ng_disambiguation/Makefile | 15 ------ matita/components/ng_extraction/Makefile | 21 -------- matita/components/ng_kernel/Makefile | 41 --------------- matita/components/ng_library/Makefile | 21 -------- matita/components/ng_paramodulation/Makefile | 18 ------- matita/components/ng_refiner/Makefile | 20 -------- matita/components/ng_tactics/Makefile | 21 -------- matita/components/registry/Makefile | 8 --- matita/components/syntax_extensions/Makefile | 51 ------------------- matita/components/syntax_extensions/dune | 1 - matita/components/thread/Makefile | 31 ----------- matita/components/xml/Makefile | 12 ----- matita/matita/help/C/Makefile | 8 +-- 26 files changed, 4 insertions(+), 489 deletions(-) delete mode 100644 matita/components/content/Makefile delete mode 100644 matita/components/content_pres/Makefile delete mode 100644 matita/components/disambiguation/Makefile rename matita/components/disambiguation/{disambiguate.crit2.ml => disambiguate.crit2_ml} (100%) rename matita/components/disambiguation/{disambiguate.crit4.ml => disambiguate.crit4_ml} (100%) delete mode 100644 matita/components/extlib/Makefile delete mode 100644 matita/components/getter/Makefile delete mode 100644 matita/components/grafite/Makefile delete mode 100644 matita/components/grafite_engine/Makefile delete mode 100644 matita/components/grafite_parser/Makefile delete mode 100644 matita/components/library/Makefile delete mode 100644 matita/components/logger/Makefile delete mode 100644 matita/components/ng_cic_content/Makefile delete mode 100644 matita/components/ng_disambiguation/Makefile delete mode 100644 matita/components/ng_extraction/Makefile delete mode 100644 matita/components/ng_kernel/Makefile delete mode 100644 matita/components/ng_library/Makefile delete mode 100644 matita/components/ng_paramodulation/Makefile delete mode 100644 matita/components/ng_refiner/Makefile delete mode 100644 matita/components/ng_tactics/Makefile delete mode 100644 matita/components/registry/Makefile delete mode 100644 matita/components/syntax_extensions/Makefile delete mode 100644 matita/components/thread/Makefile delete mode 100644 matita/components/xml/Makefile diff --git a/matita/components/content/Makefile b/matita/components/content/Makefile deleted file mode 100644 index 8ea1cd33c..000000000 --- a/matita/components/content/Makefile +++ /dev/null @@ -1,15 +0,0 @@ -PACKAGE = content -PREDICATES = - -INTERFACE_FILES = \ - content.mli \ - notationUtil.mli \ - notationEnv.mli \ - notationPp.mli \ - $(NULL) -IMPLEMENTATION_FILES = \ - notationPt.ml \ - $(INTERFACE_FILES:%.mli=%.ml) - -include ../../Makefile.defs -include ../Makefile.common diff --git a/matita/components/content_pres/Makefile b/matita/components/content_pres/Makefile deleted file mode 100644 index 28d403a70..000000000 --- a/matita/components/content_pres/Makefile +++ /dev/null @@ -1,49 +0,0 @@ -PACKAGE = content_pres -PREDICATES = - -INTERFACE_FILES = \ - renderingAttrs.mli \ - cicNotationLexer.mli \ - cicNotationParser.mli \ - mpresentation.mli \ - box.mli \ - content2presMatcher.mli \ - termContentPres.mli \ - boxPp.mli \ - cicNotationPres.mli \ - content2pres.mli \ - $(NULL) -IMPLEMENTATION_FILES = \ - $(INTERFACE_FILES:%.mli=%.ml) - -all: -clean: - -LOCAL_LINKOPTS = -package helm-content_pres -linkpkg - -cicNotationLexer.cmo: OCAMLC = $(OCAMLC_P4) -cicNotationParser.cmo: OCAMLC = $(OCAMLC_P4) -w -27 -cicNotationLexer.cmx: OCAMLOPT = $(OCAMLOPT_P4) -cicNotationParser.cmx: OCAMLOPT = $(OCAMLOPT_P4) -w -27 -cicNotationLexer.ml.annot: OCAMLC = $(OCAMLC_P4) -cicNotationParser.ml.annot: OCAMLC = $(OCAMLC_P4) - -include ../../Makefile.defs -include ../Makefile.common - -# cross compatibility among ocaml 3.09 and ocaml 3.08, to be removed as -# soon as we have ocaml 3.09 everywhere and "loc" occurrences are replaced by -# "_loc" occurrences -UTF8DIR := $(shell $(OCAMLFIND) query helm-syntax_extensions) -ULEXDIR := $(shell $(OCAMLFIND) query ulex-camlp5) -MY_SYNTAXOPTIONS = -pp "camlp5o -I $(UTF8DIR) -I $(ULEXDIR) pa_extend.cmo pa_ulex.cma pa_unicode_macro.cma -loc loc" -cicNotationLexer.cmo: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) -cicNotationParser.cmo: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) -cicNotationLexer.cmx: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) -cicNotationParser.cmx: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) -cicNotationLexer.ml.annot: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) -cicNotationParser.ml.annot: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) -depend: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) -depend.opt: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) -# - diff --git a/matita/components/disambiguation/Makefile b/matita/components/disambiguation/Makefile deleted file mode 100644 index d01dd73df..000000000 --- a/matita/components/disambiguation/Makefile +++ /dev/null @@ -1,28 +0,0 @@ -PACKAGE = disambiguation -INTERFACE_FILES = \ - disambiguateTypes.mli \ - disambiguate.mli \ - multiPassDisambiguator.mli -IMPLEMENTATION_FILES = \ - $(patsubst %.mli, %.ml, $(INTERFACE_FILES)) - -all: - -clean: -distclean: - -include ../../Makefile.defs -include ../Makefile.common - -OCAMLARCHIVEOPTIONS += -linkall - -disambiguateTypes.cmi: disambiguateTypes.mli - @echo " OCAMLC -rectypes $<" - @$(OCAMLC) -c -rectypes $< -disambiguateTypes.cmo: disambiguateTypes.ml disambiguateTypes.cmi - @echo " OCAMLC -rectypes $<" - @$(OCAMLC) -c -rectypes $< -disambiguateTypes.cmx: disambiguateTypes.ml disambiguateTypes.cmi - @echo " OCAMLOPT -rectypes $<" - @$(OCAMLOPT) -c -rectypes $< - diff --git a/matita/components/disambiguation/disambiguate.crit2.ml b/matita/components/disambiguation/disambiguate.crit2_ml similarity index 100% rename from matita/components/disambiguation/disambiguate.crit2.ml rename to matita/components/disambiguation/disambiguate.crit2_ml diff --git a/matita/components/disambiguation/disambiguate.crit4.ml b/matita/components/disambiguation/disambiguate.crit4_ml similarity index 100% rename from matita/components/disambiguation/disambiguate.crit4.ml rename to matita/components/disambiguation/disambiguate.crit4_ml diff --git a/matita/components/extlib/Makefile b/matita/components/extlib/Makefile deleted file mode 100644 index 8167ec3b4..000000000 --- a/matita/components/extlib/Makefile +++ /dev/null @@ -1,21 +0,0 @@ -PACKAGE = extlib -PREDICATES = - -INTERFACE_FILES = \ - componentsConf.mli \ - hExtlib.mli \ - hMarshal.mli \ - patternMatcher.mli \ - hLog.mli \ - trie.mli \ - discrimination_tree.mli \ - hTopoSort.mli \ - graphvizPp.mli \ - $(NULL) -IMPLEMENTATION_FILES = \ - $(INTERFACE_FILES:%.mli=%.ml) -EXTRA_OBJECTS_TO_INSTALL = -EXTRA_OBJECTS_TO_CLEAN = - -include ../../Makefile.defs -include ../Makefile.common diff --git a/matita/components/getter/Makefile b/matita/components/getter/Makefile deleted file mode 100644 index 0f2132eec..000000000 --- a/matita/components/getter/Makefile +++ /dev/null @@ -1,21 +0,0 @@ - -PACKAGE = getter - -INTERFACE_FILES = \ - http_getter_wget.mli \ - http_getter_logger.mli \ - http_getter_misc.mli \ - http_getter_const.mli \ - http_getter_env.mli \ - http_getter_storage.mli \ - http_getter_common.mli \ - http_getter.mli \ - $(NULL) - -IMPLEMENTATION_FILES = \ - http_getter_types.ml \ - $(INTERFACE_FILES:%.mli=%.ml) - -include ../../Makefile.defs -include ../Makefile.common - diff --git a/matita/components/grafite/Makefile b/matita/components/grafite/Makefile deleted file mode 100644 index 158bc992d..000000000 --- a/matita/components/grafite/Makefile +++ /dev/null @@ -1,13 +0,0 @@ -PACKAGE = grafite -PREDICATES = - -INTERFACE_FILES = \ - grafiteAstPp.mli \ - $(NULL) -IMPLEMENTATION_FILES = \ - grafiteAst.ml \ - $(INTERFACE_FILES:%.mli=%.ml) - - -include ../../Makefile.defs -include ../Makefile.common diff --git a/matita/components/grafite_engine/Makefile b/matita/components/grafite_engine/Makefile deleted file mode 100644 index c8d3866c0..000000000 --- a/matita/components/grafite_engine/Makefile +++ /dev/null @@ -1,12 +0,0 @@ -PACKAGE = grafite_engine -PREDICATES = - -INTERFACE_FILES = \ - grafiteTypes.mli \ - nCicCoercDeclaration.mli \ - grafiteEngine.mli \ - $(NULL) -IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) - -include ../../Makefile.defs -include ../Makefile.common diff --git a/matita/components/grafite_parser/Makefile b/matita/components/grafite_parser/Makefile deleted file mode 100644 index b5b20bb60..000000000 --- a/matita/components/grafite_parser/Makefile +++ /dev/null @@ -1,29 +0,0 @@ -PACKAGE = grafite_parser -PREDICATES = - -INTERFACE_FILES = \ - grafiteParser.mli \ - print_grammar.mli \ - $(NULL) -IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) - -all: -clean: - -# cross compatibility among ocaml 3.09 and ocaml 3.08, to be removed as -# soon as we have ocaml 3.09 everywhere and "loc" occurrences are replaced by -# "_loc" occurrences -UTF8DIR = $(shell $(OCAMLFIND) query helm-syntax_extensions) -ULEXDIR = $(shell $(OCAMLFIND) query ulex-camlp5) -MY_SYNTAXOPTIONS = -pp "camlp5o -I $(UTF8DIR) -I $(ULEXDIR) pa_extend.cmo pa_ulex.cma pa_unicode_macro.cma -loc loc" -grafiteParser.cmo: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) -grafiteParser.cmx: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) -depend: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) -depend.opt: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) -# -# -grafiteParser.cmo: OCAMLC = $(OCAMLC_P4) -w -27 -grafiteParser.cmx: OCAMLOPT = $(OCAMLOPT_P4) -w -27 - -include ../../Makefile.defs -include ../Makefile.common diff --git a/matita/components/library/Makefile b/matita/components/library/Makefile deleted file mode 100644 index 715ee8f01..000000000 --- a/matita/components/library/Makefile +++ /dev/null @@ -1,13 +0,0 @@ -PACKAGE = library -PREDICATES = - -INTERFACE_FILES = \ - librarian.mli \ - libraryMisc.mli \ - libraryClean.mli \ - $(NULL) -IMPLEMENTATION_FILES = \ - $(INTERFACE_FILES:%.mli=%.ml) - -include ../../Makefile.defs -include ../Makefile.common diff --git a/matita/components/logger/Makefile b/matita/components/logger/Makefile deleted file mode 100644 index 39d690084..000000000 --- a/matita/components/logger/Makefile +++ /dev/null @@ -1,10 +0,0 @@ - -PACKAGE = logger -INTERFACE_FILES = \ - helmLogger.mli -IMPLEMENTATION_FILES = \ - $(INTERFACE_FILES:%.mli=%.ml) - -include ../../Makefile.defs -include ../Makefile.common - diff --git a/matita/components/ng_cic_content/Makefile b/matita/components/ng_cic_content/Makefile deleted file mode 100644 index ac40a66f1..000000000 --- a/matita/components/ng_cic_content/Makefile +++ /dev/null @@ -1,14 +0,0 @@ -PACKAGE = ng_cic_content - -INTERFACE_FILES = \ - ncic2astMatcher.mli \ - interpretations.mli - -IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) - - -all: - - -include ../../Makefile.defs -include ../Makefile.common diff --git a/matita/components/ng_disambiguation/Makefile b/matita/components/ng_disambiguation/Makefile deleted file mode 100644 index 082d000bc..000000000 --- a/matita/components/ng_disambiguation/Makefile +++ /dev/null @@ -1,15 +0,0 @@ -PACKAGE = ng_disambiguation -PREDICATES = - -INTERFACE_FILES = \ - nnumber_notation.mli \ - disambiguateChoices.mli \ - nCicDisambiguate.mli \ - grafiteDisambiguate.mli \ - $(NULL) -IMPLEMENTATION_FILES = \ - $(INTERFACE_FILES:%.mli=%.ml) - - -include ../../Makefile.defs -include ../Makefile.common diff --git a/matita/components/ng_extraction/Makefile b/matita/components/ng_extraction/Makefile deleted file mode 100644 index 46f6f14de..000000000 --- a/matita/components/ng_extraction/Makefile +++ /dev/null @@ -1,21 +0,0 @@ -PACKAGE = ng_extraction -PREDICATES = - -INTERFACE_FILES = \ - nCicExtraction.mli \ - coq.mli \ - ocamlExtractionTable.mli \ - mlutil.mli \ - common.mli \ - extraction.mli \ - ocaml.mli \ - ocamlExtraction.mli -# extract_env.mli \ - -IMPLEMENTATION_FILES = \ - miniml.ml $(INTERFACE_FILES:%.mli=%.ml) -EXTRA_OBJECTS_TO_INSTALL = -EXTRA_OBJECTS_TO_CLEAN = - -include ../../Makefile.defs -include ../Makefile.common diff --git a/matita/components/ng_kernel/Makefile b/matita/components/ng_kernel/Makefile deleted file mode 100644 index 31dd1e9c4..000000000 --- a/matita/components/ng_kernel/Makefile +++ /dev/null @@ -1,41 +0,0 @@ -PACKAGE = ng_kernel -PREDICATES = - -INTERFACE_FILES = \ - nUri.mli \ - nReference.mli \ - nCicUtils.mli \ - nCicSubstitution.mli \ - nCicEnvironment.mli \ - nCicReduction.mli \ - nCicTypeChecker.mli \ - nCicUntrusted.mli \ - nCicPp.mli - -IMPLEMENTATION_FILES = \ - nCic.ml $(INTERFACE_FILES:%.mli=%.ml) -EXTRA_OBJECTS_TO_INSTALL = -EXTRA_OBJECTS_TO_CLEAN = - -include ../../Makefile.defs -include ../Makefile.common - -depend.dot: $(IMPLEMENTATION_FILES) $(INTERFACE_FILES) - ocamldoc -o depend.dot -rectypes -I ../extlib/ -I ../cic -I ../cic_proof_checking/ -I ../urimanager/ -I ../logger/ -I ../registry/ -I ../getter/ -I ../hmysql/ -I ../library/ -I ../metadata/ -dot nUri.ml nReference.ml nCic.ml nCicPp.ml nCicEnvironment.ml nCicSubstitution.ml nCicReduction.ml nCicTypeChecker.ml nCicUtils.ml nCicLibrary.ml - cat depend.dot | grep -v "^}$$" > /tmp/depend.dot && mv /tmp/depend.dot . - for i in `cat depend.dot | grep darkturquoise | cut -d '"' -f 2`; do j=`echo $$i | sed s/^N/n/g`; size=`cat $$j.ml | wc -l`; funs=`cat $$j.mli | grep "^val " | wc -l`; size=`expr $$size - 13`; echo "\"$$i\" [ label=\"$$i\\n$$size lines,\\n$$funs functions\"];"; done >> depend.dot - echo "}" >> depend.dot - cat depend.dot | grep -v "darkturquoise" > /tmp/depend.dot && mv /tmp/depend.dot . - cat depend.dot - tred < depend.dot > /tmp/depend.dot && mv /tmp/depend.dot . - cat depend.dot | grep -v "^}$$" > /tmp/depend.dot && mv /tmp/depend.dot . - echo " NCicEnvironment -> NCicTypeChecker;" >> depend.dot - cat depend.dot | grep -v "NCicEnvironment -> NCic;" > /tmp/depend.dot && mv /tmp/depend.dot . - echo "NCicLibrary [ style=dashed ];" >> depend.dot - echo "NCicPp [ style=dashed ];" >> depend.dot - echo "}" >> depend.dot - cat depend.dot | grep -v "rotate" > /tmp/depend.dot && mv /tmp/depend.dot . - -depend.png depend.eps: depend.dot - dot -Tpng > depend.png < depend.dot - dot -Tps > depend.eps < depend.dot diff --git a/matita/components/ng_library/Makefile b/matita/components/ng_library/Makefile deleted file mode 100644 index 20157a09e..000000000 --- a/matita/components/ng_library/Makefile +++ /dev/null @@ -1,21 +0,0 @@ -PACKAGE = ng_library -PREDICATES = - -INTERFACE_FILES = \ - nCicLibrary.mli - -IMPLEMENTATION_FILES = \ - $(INTERFACE_FILES:%.mli=%.ml) -EXTRA_OBJECTS_TO_INSTALL = -EXTRA_OBJECTS_TO_CLEAN = - -all: -%: %.ml $(PACKAGE).cma - $(OCAMLC) -package helm-$(PACKAGE) -linkpkg -o $@ $< -all.opt opt: -%.opt: %.ml $(PACKAGE).cmxa - $(OCAMLOPT) -package helm-$(PACKAGE) -linkpkg -o $@ $< - -include ../../Makefile.defs -include ../Makefile.common - diff --git a/matita/components/ng_paramodulation/Makefile b/matita/components/ng_paramodulation/Makefile deleted file mode 100644 index ca2e5d1af..000000000 --- a/matita/components/ng_paramodulation/Makefile +++ /dev/null @@ -1,18 +0,0 @@ -PACKAGE = ng_paramodulation - -INTERFACE_FILES = \ - terms.mli pp.mli foSubst.mli \ - orderings.mli foUtils.mli foUnif.mli index.mli superposition.mli \ - stats.mli paramod.mli nCicBlob.mli nCicProof.mli \ - nCicParamod.mli - -IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) - -all: hash.o -opt: hash.o - -hash.o: - gcc -I `ocamlc -where`/caml/ -c hash.c - -include ../../Makefile.defs -include ../Makefile.common diff --git a/matita/components/ng_refiner/Makefile b/matita/components/ng_refiner/Makefile deleted file mode 100644 index 612078e3e..000000000 --- a/matita/components/ng_refiner/Makefile +++ /dev/null @@ -1,20 +0,0 @@ -PACKAGE = ng_refiner -PREDICATES = - -INTERFACE_FILES = \ - nDiscriminationTree.mli \ - nCicMetaSubst.mli \ - nCicUnifHint.mli \ - nCicCoercion.mli \ - nCicRefineUtil.mli \ - nCicUnification.mli \ - nCicRefiner.mli - -IMPLEMENTATION_FILES = \ - $(INTERFACE_FILES:%.mli=%.ml) -EXTRA_OBJECTS_TO_INSTALL = -EXTRA_OBJECTS_TO_CLEAN = - -include ../../Makefile.defs -include ../Makefile.common - diff --git a/matita/components/ng_tactics/Makefile b/matita/components/ng_tactics/Makefile deleted file mode 100644 index b7a98406f..000000000 --- a/matita/components/ng_tactics/Makefile +++ /dev/null @@ -1,21 +0,0 @@ -PACKAGE = ng_tactics - -INTERFACE_FILES = \ - continuationals.mli \ - nCicTacReduction.mli \ - nTacStatus.mli \ - nCicElim.mli \ - nTactics.mli \ - nnAuto.mli \ - declarative.mli \ - nDestructTac.mli \ - nInversion.mli - -IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) - - -all: - - -include ../../Makefile.defs -include ../Makefile.common diff --git a/matita/components/registry/Makefile b/matita/components/registry/Makefile deleted file mode 100644 index bb9715ab4..000000000 --- a/matita/components/registry/Makefile +++ /dev/null @@ -1,8 +0,0 @@ - -PACKAGE = registry -INTERFACE_FILES = helm_registry.mli -IMPLEMENTATION_FILES = helm_registry.ml - -include ../../Makefile.defs -include ../Makefile.common - diff --git a/matita/components/syntax_extensions/Makefile b/matita/components/syntax_extensions/Makefile deleted file mode 100644 index 4f34ae818..000000000 --- a/matita/components/syntax_extensions/Makefile +++ /dev/null @@ -1,51 +0,0 @@ -PACKAGE = syntax_extensions -PREDICATES = -MAKE_TABLE_PACKAGES = helm-xml - -# modules which have both a .ml and a .mli -INTERFACE_FILES = utf8Macro.mli -IMPLEMENTATION_FILES = utf8MacroTable.ml $(INTERFACE_FILES:%.mli=%.ml) -EXTRA_OBJECTS_TO_INSTALL = -EXTRA_OBJECTS_TO_CLEAN = - -all: syntax_extensions.cma pa_unicode_macro.cma profiling_macros.cma - -make_table: make_table.ml - @echo " OCAMLC $<" - $(H)$(OCAMLFIND) ocamlc -rectypes -package $(MAKE_TABLE_PACKAGES) -linkpkg -o $@ $^ - -utf8MacroTable.ml: - ./make_table $@ $@.txt -utf8MacroTable.cmo: utf8MacroTable.ml - @echo " OCAMLC $<" - $(H)@$(OCAMLFIND) ocamlc -rectypes -c $< - -pa_unicode_macro.cmo: pa_unicode_macro.ml utf8Macro.cmo - @echo " OCAMLC $<" - $(H)@$(OCAMLFIND) ocamlc -rectypes -package camlp5 -pp "camlp5o q_MLast.cmo pa_extend.cmo -loc loc" -c $< -pa_unicode_macro.cma: utf8MacroTable.cmo utf8Macro.cmo pa_unicode_macro.cmo - @echo " OCAMLC -a $@" - $(H)@$(OCAMLFIND) ocamlc -a -o $@ $^ - -profiling_macros.cmo: profiling_macros.ml - @echo " OCAMLC $<" - $(H)@$(OCAMLFIND) ocamlc -package camlp5 -package str -pp "camlp5o -loc loc" -c $< -profiling_macros.cma:profiling_macros.cmo - @echo " OCAMLC -a $@" - $(H)@$(OCAMLFIND) ocamlc -a -o $@ $^ - - -.PHONY: test -test: test.ml - $(OCAMLFIND) ocamlc -package helm-utf8_macros -syntax camlp5o $< -o $@ - -clean: -distclean: extra_clean -extra_clean: - rm -f make_table test - -STATS_EXCLUDE = utf8MacroTable.ml - -include ../../Makefile.defs -include ../Makefile.common - diff --git a/matita/components/syntax_extensions/dune b/matita/components/syntax_extensions/dune index c9512a384..c36e49904 100644 --- a/matita/components/syntax_extensions/dune +++ b/matita/components/syntax_extensions/dune @@ -16,7 +16,6 @@ (wrapped false) (preprocess (action (system "camlp5o q_MLast.cmo pa_extend.cmo -loc loc %{input-file}"))) (preprocessor_deps helm_syntax_extensions.cma) - ;(library_flags components/syntax_extensions/helm_syntax_extensions.cma) (modules pa_unicode_macro)) (library diff --git a/matita/components/thread/Makefile b/matita/components/thread/Makefile deleted file mode 100644 index 46f009e07..000000000 --- a/matita/components/thread/Makefile +++ /dev/null @@ -1,31 +0,0 @@ - -PACKAGE = thread -INTERFACE_FILES = threadSafe.mli extThread.mli -IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) - -all: thread_fake.cma -opt: thread_fake.cmxa - -include ../../Makefile.defs -include ../Makefile.common - -fake/threadSafe.cmi: fake/threadSafe.mli - @echo " OCAMLC $<" - @cd fake/ \ - && ocamlfind ocamlc -c threadSafe.mli -thread_fake.cma: fake/threadSafe.cmi - @echo " OCAMLC -a $@" - @cd fake/ \ - && ocamlfind ocamlc -a -o $@ threadSafe.ml \ - && cp $@ ../ -thread_fake.cmxa: fake/threadSafe.cmi - @echo " OCAMLOPT -a $@" - @cd fake/ \ - && ocamlfind opt -a -o $@ threadSafe.ml \ - && cp $@ ../ - -clean: clean_fake -clean_fake: - rm -f fake/*.cm[aiox] fake/*.cmxa fake/*.[ao] - rm -f thread_fake.cma thread_fake.cmxa - diff --git a/matita/components/xml/Makefile b/matita/components/xml/Makefile deleted file mode 100644 index 7948435aa..000000000 --- a/matita/components/xml/Makefile +++ /dev/null @@ -1,12 +0,0 @@ -PACKAGE = xml -PREDICATES = - -INTERFACE_FILES = \ - xml.mli \ - xmlPushParser.mli -IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) -EXTRA_OBJECTS_TO_INSTALL = -EXTRA_OBJECTS_TO_CLEAN = - -include ../../Makefile.defs -include ../Makefile.common diff --git a/matita/matita/help/C/Makefile b/matita/matita/help/C/Makefile index 817d6964a..bdffeb5e3 100644 --- a/matita/matita/help/C/Makefile +++ b/matita/matita/help/C/Makefile @@ -1,5 +1,5 @@ -include ../../../Makefile.defs +#include ../../../Makefile.defs XSLTPROC=xsltproc XHTML_XSL=xsl/matita-xhtml.xsl @@ -28,11 +28,11 @@ pdf-stamp: $(patsubst %.xml,%.pdf,$(MAIN)) touch $@ %.pdf: %.xml - dblatex -rscripts/fix-symbols.sh -tpdf $< + dblatex -r scripts/fix-symbols.sh -t pdf $< %.dvi: %.xml - dblatex -rscripts/fix-symbols.sh -tdvi $< + dblatex -r scripts/fix-symbols.sh -t dvi $< %.ps: %.xml - dblatex -rscripts/fix-symbols.sh -tps $< + dblatex -r scripts/fix-symbols.sh -t ps $< install: install-html install-pdf install-pdf: pdf-stamp -- 2.39.2