From: Claudio Sacerdoti Coen Date: Wed, 5 Feb 2003 12:46:20 +0000 (+0000) Subject: Makefile.common.in and .depend backtracked to my last commit (before the X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=8d384f4df7e7411870a36486db9e2282dca1cbd5 Makefile.common.in and .depend backtracked to my last commit (before the ones of Ferruccio) and then modified. Dependencies between a file and a library are now handled correctly. --- diff --git a/helm/gTopLevel/.depend b/helm/gTopLevel/.depend new file mode 100644 index 000000000..fa167f5f1 --- /dev/null +++ b/helm/gTopLevel/.depend @@ -0,0 +1,52 @@ +xml2Gdome.cmo: xml2Gdome.cmi +xml2Gdome.cmx: xml2Gdome.cmi +proofEngine.cmo: proofEngine.cmi +proofEngine.cmx: proofEngine.cmi +doubleTypeInference.cmo: doubleTypeInference.cmi +doubleTypeInference.cmx: doubleTypeInference.cmi +cic2acic.cmo: doubleTypeInference.cmi cic2acic.cmi +cic2acic.cmx: doubleTypeInference.cmx cic2acic.cmi +cic2Xml.cmo: cic2acic.cmi cic2Xml.cmi +cic2Xml.cmx: cic2acic.cmx cic2Xml.cmi +cic2Xml.cmi: cic2acic.cmi +logicalOperations.cmo: proofEngine.cmi logicalOperations.cmi +logicalOperations.cmx: proofEngine.cmx logicalOperations.cmi +sequentPp.cmo: cic2Xml.cmi cic2acic.cmi sequentPp.cmi +sequentPp.cmx: cic2Xml.cmx cic2acic.cmx sequentPp.cmi +mQueryLevels.cmo: mQueryLevels.cmi +mQueryLevels.cmx: mQueryLevels.cmi +mQueryLevels2.cmi: mQueryGenerator.cmi +mQueryLevels2.cmo: mQueryLevels2.cmi +mQueryLevels2.cmx: mQueryLevels2.cmi +mQueryGenerator.cmo: mQueryGenerator.cmi +mQueryGenerator.cmx: mQueryGenerator.cmi +misc.cmo: misc.cmi +misc.cmx: misc.cmi +disambiguate.cmo: mQueryGenerator.cmi misc.cmi disambiguate.cmi +disambiguate.cmx: mQueryGenerator.cmx misc.cmx disambiguate.cmi +termEditor.cmo: disambiguate.cmi termEditor.cmi +termEditor.cmx: disambiguate.cmx termEditor.cmi +termEditor.cmi: disambiguate.cmi +applyStylesheets.cmo: cic2Xml.cmi misc.cmi sequentPp.cmi xml2Gdome.cmi \ + applyStylesheets.cmi +applyStylesheets.cmx: cic2Xml.cmx misc.cmx sequentPp.cmx xml2Gdome.cmx \ + applyStylesheets.cmi +applyStylesheets.cmi: cic2acic.cmi +termViewer.cmo: applyStylesheets.cmi cic2acic.cmi logicalOperations.cmi \ + misc.cmi termViewer.cmi +termViewer.cmx: applyStylesheets.cmx cic2acic.cmx logicalOperations.cmx \ + misc.cmx termViewer.cmi +termViewer.cmi: cic2acic.cmi +invokeTactics.cmo: logicalOperations.cmi proofEngine.cmi termEditor.cmi \ + termViewer.cmi invokeTactics.cmi +invokeTactics.cmx: logicalOperations.cmx proofEngine.cmx termEditor.cmx \ + termViewer.cmx invokeTactics.cmi +invokeTactics.cmi: termEditor.cmi termViewer.cmi +gTopLevel.cmo: applyStylesheets.cmi cic2Xml.cmi cic2acic.cmi \ + invokeTactics.cmi logicalOperations.cmi mQueryGenerator.cmi \ + mQueryLevels.cmi mQueryLevels2.cmi misc.cmi proofEngine.cmi sequentPp.cmi \ + termEditor.cmi termViewer.cmi +gTopLevel.cmx: applyStylesheets.cmx cic2Xml.cmx cic2acic.cmx \ + invokeTactics.cmx logicalOperations.cmx mQueryGenerator.cmx \ + mQueryLevels.cmx mQueryLevels2.cmx misc.cmx proofEngine.cmx sequentPp.cmx \ + termEditor.cmx termViewer.cmx diff --git a/helm/gTopLevel/Makefile b/helm/gTopLevel/Makefile index 5f630f23c..7822b1ace 100644 --- a/helm/gTopLevel/Makefile +++ b/helm/gTopLevel/Makefile @@ -4,7 +4,6 @@ REQUIRES = lablgtkmathview helm-cic_textual_parser helm-cic_proof_checking \ helm-mathql_interpreter PREDICATES = "gnome,init,glade" OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" -pp camlp4o -OCAMLDEPOPTIONS = $(shell ocamlfind query -recursive -predicates "$(PREDICATES)" -i-format $(REQUIRES)) OCAMLFIND = ocamlfind OCAMLC = $(OCAMLFIND) ocamlc $(OCAMLOPTIONS) OCAMLOPT = $(OCAMLFIND) ocamlopt $(OCAMLOPTIONS) @@ -34,7 +33,7 @@ TOPLEVELOBJS = \ gTopLevel.cmo depend: - $(OCAMLDEP) $(OCAMLDEPOPTIONS) $(DEPOBJS) > .depend + $(OCAMLDEP) $(DEPOBJS) > .depend gTopLevel: $(TOPLEVELOBJS) $(LIBRARIES) $(OCAMLC) -linkpkg -o gTopLevel $(TOPLEVELOBJS) @@ -43,13 +42,16 @@ gTopLevel.opt: $(TOPLEVELOBJS:.cmo=.cmx) $(LIBRARIES_OPT) $(OCAMLOPT) -linkpkg -o gTopLevel.opt $(TOPLEVELOBJS:.cmo=.cmx) .SUFFIXES: .ml .mli .cmo .cmi .cmx -.ml.cmo: $(LIBRARIES) +.ml.cmo: $(OCAMLC) -c $< -.mli.cmi: $(LIBRARIES) +.mli.cmi: $(OCAMLC) -c $< -.ml.cmx: $(LIBRARIES_OPT) +.ml.cmx: $(OCAMLOPT) -c $< +$(TOPLEVELOBJS): $(LIBRARIES) +$(TOPLEVELOBJS:.cmo=.cmx)): $(LIBRARIES_OPT) + clean: rm -f *.cm[iox] *.o gTopLevel gTopLevel.opt diff --git a/helm/ocaml/Makefile.common.in b/helm/ocaml/Makefile.common.in index 519b2ea9a..42015d622 100644 --- a/helm/ocaml/Makefile.common.in +++ b/helm/ocaml/Makefile.common.in @@ -19,7 +19,7 @@ OCAMLYACC = ocamlyacc 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)) -OCAMLDEPOPTIONS = $(shell ocamlfind query -recursive -predicates "$(PREDICATES)" -i-format $(REQUIRES)) + ARCHIVE = $(PACKAGE).cma ARCHIVE_OPT = $(PACKAGE).cmxa @@ -38,14 +38,14 @@ all: $(IMPLEMENTATION_FILES:%.ml=%.cmo) $(ARCHIVE) opt: $(IMPLEMENTATION_FILES:%.ml=%.cmx) $(ARCHIVE_OPT) depend: $(DEPEND_FILES) - $(OCAMLDEP) $(OCAMLDEPOPTIONS) $(INTERFACE_FILES) $(IMPLEMENTATION_FILES) > .depend + $(OCAMLDEP) $(INTERFACE_FILES) $(IMPLEMENTATION_FILES) > .depend .SUFFIXES: .ml .mli .cmo .cmi .cmx .mll .mly -.ml.cmo: $(LIBRARIES) +.ml.cmo: $(OCAMLC) -c $< -.mli.cmi: $(LIBRARIES) +.mli.cmi: $(OCAMLC) -c $< -.ml.cmx: $(LIBRARIES_OPT) +.ml.cmx: $(OCAMLOPT) -c $< .mly.ml: $(OCAMLYACC) $< @@ -54,6 +54,9 @@ depend: $(DEPEND_FILES) .mll.ml: $(OCAMLLEX) $< +$(IMPLEMENTATION_FILES:%.ml=%.cmo): $(LIBRARIES) +$(IMPLEMENTATION_FILES:%.ml=%.cmx): $(LIBRARIES_OPT) + clean: rm -f *.cm[ioax] *.cmxa *.o *.a $(EXTRA_OBJECTS_TO_CLEAN) diff --git a/helm/ocaml/cic/.depend b/helm/ocaml/cic/.depend new file mode 100644 index 000000000..591cea8df --- /dev/null +++ b/helm/ocaml/cic/.depend @@ -0,0 +1,12 @@ +deannotate.cmi: cic.cmo +cicParser3.cmi: cic.cmo +cicParser2.cmi: cic.cmo cicParser3.cmi +cicParser.cmi: cic.cmo +deannotate.cmo: cic.cmo deannotate.cmi +deannotate.cmx: cic.cmx deannotate.cmi +cicParser3.cmo: cic.cmo cicParser3.cmi +cicParser3.cmx: cic.cmx cicParser3.cmi +cicParser2.cmo: cic.cmo cicParser3.cmi cicParser2.cmi +cicParser2.cmx: cic.cmx cicParser3.cmx cicParser2.cmi +cicParser.cmo: cicParser2.cmi cicParser3.cmi deannotate.cmi cicParser.cmi +cicParser.cmx: cicParser2.cmx cicParser3.cmx deannotate.cmx cicParser.cmi diff --git a/helm/ocaml/cic_annotations/.depend b/helm/ocaml/cic_annotations/.depend new file mode 100644 index 000000000..2c30fa7d7 --- /dev/null +++ b/helm/ocaml/cic_annotations/.depend @@ -0,0 +1,8 @@ +cicXPath.cmo: cicXPath.cmi +cicXPath.cmx: cicXPath.cmi +cicAnnotation2Xml.cmo: cicXPath.cmi cicAnnotation2Xml.cmi +cicAnnotation2Xml.cmx: cicXPath.cmx cicAnnotation2Xml.cmi +cicAnnotationParser2.cmo: cicAnnotationParser2.cmi +cicAnnotationParser2.cmx: cicAnnotationParser2.cmi +cicAnnotationParser.cmo: cicAnnotationParser2.cmi cicAnnotationParser.cmi +cicAnnotationParser.cmx: cicAnnotationParser2.cmx cicAnnotationParser.cmi diff --git a/helm/ocaml/cic_annotations_cache/.depend b/helm/ocaml/cic_annotations_cache/.depend new file mode 100644 index 000000000..06775e1c6 --- /dev/null +++ b/helm/ocaml/cic_annotations_cache/.depend @@ -0,0 +1,2 @@ +cicCache.cmo: cicCache.cmi +cicCache.cmx: cicCache.cmi diff --git a/helm/ocaml/cic_cache/.depend b/helm/ocaml/cic_cache/.depend new file mode 100644 index 000000000..06775e1c6 --- /dev/null +++ b/helm/ocaml/cic_cache/.depend @@ -0,0 +1,2 @@ +cicCache.cmo: cicCache.cmi +cicCache.cmx: cicCache.cmi diff --git a/helm/ocaml/cic_proof_checking/.depend b/helm/ocaml/cic_proof_checking/.depend new file mode 100644 index 000000000..c1319a692 --- /dev/null +++ b/helm/ocaml/cic_proof_checking/.depend @@ -0,0 +1,22 @@ +logger.cmo: logger.cmi +logger.cmx: logger.cmi +cicEnvironment.cmo: logger.cmi cicEnvironment.cmi +cicEnvironment.cmx: logger.cmx cicEnvironment.cmi +cicPp.cmo: cicEnvironment.cmi cicPp.cmi +cicPp.cmx: cicEnvironment.cmx cicPp.cmi +cicSubstitution.cmo: cicEnvironment.cmi cicSubstitution.cmi +cicSubstitution.cmx: cicEnvironment.cmx cicSubstitution.cmi +cicMiniReduction.cmo: cicSubstitution.cmi cicMiniReduction.cmi +cicMiniReduction.cmx: cicSubstitution.cmx cicMiniReduction.cmi +cicReductionNaif.cmo: cicEnvironment.cmi cicPp.cmi cicSubstitution.cmi \ + cicReductionNaif.cmi +cicReductionNaif.cmx: cicEnvironment.cmx cicPp.cmx cicSubstitution.cmx \ + cicReductionNaif.cmi +cicReduction.cmo: cicEnvironment.cmi cicPp.cmi cicSubstitution.cmi \ + cicReduction.cmi +cicReduction.cmx: cicEnvironment.cmx cicPp.cmx cicSubstitution.cmx \ + cicReduction.cmi +cicTypeChecker.cmo: cicEnvironment.cmi cicPp.cmi cicReduction.cmi \ + cicSubstitution.cmi logger.cmi cicTypeChecker.cmi +cicTypeChecker.cmx: cicEnvironment.cmx cicPp.cmx cicReduction.cmx \ + cicSubstitution.cmx logger.cmx cicTypeChecker.cmi diff --git a/helm/ocaml/cic_textual_parser/.depend b/helm/ocaml/cic_textual_parser/.depend new file mode 100644 index 000000000..d7aabf85c --- /dev/null +++ b/helm/ocaml/cic_textual_parser/.depend @@ -0,0 +1,10 @@ +cicTextualParser.cmi: cicTextualParser0.cmo +cicTextualParserContext.cmi: cicTextualParser.cmi cicTextualParser0.cmo +cicTextualParser.cmo: cicTextualParser0.cmo cicTextualParser.cmi +cicTextualParser.cmx: cicTextualParser0.cmx cicTextualParser.cmi +cicTextualParserContext.cmo: cicTextualParser.cmi cicTextualParser0.cmo \ + cicTextualParserContext.cmi +cicTextualParserContext.cmx: cicTextualParser.cmx cicTextualParser0.cmx \ + cicTextualParserContext.cmi +cicTextualLexer.cmo: cicTextualParser.cmi +cicTextualLexer.cmx: cicTextualParser.cmx diff --git a/helm/ocaml/cic_unification/.depend b/helm/ocaml/cic_unification/.depend new file mode 100644 index 000000000..d22689dce --- /dev/null +++ b/helm/ocaml/cic_unification/.depend @@ -0,0 +1,5 @@ +cicRefine.cmi: cicUnification.cmi +cicUnification.cmo: cicUnification.cmi +cicUnification.cmx: cicUnification.cmi +cicRefine.cmo: cicUnification.cmi cicRefine.cmi +cicRefine.cmx: cicUnification.cmx cicRefine.cmi diff --git a/helm/ocaml/getter/.depend b/helm/ocaml/getter/.depend new file mode 100644 index 000000000..2013e9b3e --- /dev/null +++ b/helm/ocaml/getter/.depend @@ -0,0 +1,6 @@ +configuration.cmo: configuration.cmi +configuration.cmx: configuration.cmi +clientHTTP.cmo: configuration.cmi clientHTTP.cmi +clientHTTP.cmx: configuration.cmx clientHTTP.cmi +getter.cmo: clientHTTP.cmi configuration.cmi getter.cmi +getter.cmx: clientHTTP.cmx configuration.cmx getter.cmi diff --git a/helm/ocaml/pxp/.depend b/helm/ocaml/pxp/.depend new file mode 100644 index 000000000..c2a1a4be6 --- /dev/null +++ b/helm/ocaml/pxp/.depend @@ -0,0 +1,2 @@ +pxpUrlResolver.cmo: pxpUrlResolver.cmi +pxpUrlResolver.cmx: pxpUrlResolver.cmi diff --git a/helm/ocaml/tactics/.depend b/helm/ocaml/tactics/.depend new file mode 100644 index 000000000..e6dc05be5 --- /dev/null +++ b/helm/ocaml/tactics/.depend @@ -0,0 +1,77 @@ +proofEngineHelpers.cmi: proofEngineTypes.cmo +tacticals.cmi: proofEngineTypes.cmo +reductionTactics.cmi: proofEngineTypes.cmo +proofEngineStructuralRules.cmi: proofEngineTypes.cmo +primitiveTactics.cmi: proofEngineTypes.cmo +variousTactics.cmi: proofEngineTypes.cmo +introductionTactics.cmi: proofEngineTypes.cmo +eliminationTactics.cmi: proofEngineTypes.cmo +negationTactics.cmi: proofEngineTypes.cmo +equalityTactics.cmi: proofEngineTypes.cmo +discriminationTactics.cmi: proofEngineTypes.cmo +ring.cmi: proofEngineTypes.cmo +fourierR.cmi: proofEngineTypes.cmo +proofEngineReduction.cmo: proofEngineReduction.cmi +proofEngineReduction.cmx: proofEngineReduction.cmi +proofEngineHelpers.cmo: proofEngineHelpers.cmi +proofEngineHelpers.cmx: proofEngineHelpers.cmi +fourier.cmo: fourier.cmi +fourier.cmx: fourier.cmi +tacticals.cmo: proofEngineTypes.cmo tacticals.cmi +tacticals.cmx: proofEngineTypes.cmx tacticals.cmi +reductionTactics.cmo: proofEngineReduction.cmi reductionTactics.cmi +reductionTactics.cmx: proofEngineReduction.cmx reductionTactics.cmi +proofEngineStructuralRules.cmo: proofEngineTypes.cmo \ + proofEngineStructuralRules.cmi +proofEngineStructuralRules.cmx: proofEngineTypes.cmx \ + proofEngineStructuralRules.cmi +primitiveTactics.cmo: proofEngineHelpers.cmi proofEngineReduction.cmi \ + proofEngineTypes.cmo reductionTactics.cmi tacticals.cmi \ + primitiveTactics.cmi +primitiveTactics.cmx: proofEngineHelpers.cmx proofEngineReduction.cmx \ + proofEngineTypes.cmx reductionTactics.cmx tacticals.cmx \ + primitiveTactics.cmi +variousTactics.cmo: primitiveTactics.cmi proofEngineHelpers.cmi \ + proofEngineReduction.cmi proofEngineTypes.cmo tacticals.cmi \ + variousTactics.cmi +variousTactics.cmx: primitiveTactics.cmx proofEngineHelpers.cmx \ + proofEngineReduction.cmx proofEngineTypes.cmx tacticals.cmx \ + variousTactics.cmi +introductionTactics.cmo: primitiveTactics.cmi proofEngineTypes.cmo \ + introductionTactics.cmi +introductionTactics.cmx: primitiveTactics.cmx proofEngineTypes.cmx \ + introductionTactics.cmi +eliminationTactics.cmo: primitiveTactics.cmi proofEngineStructuralRules.cmi \ + tacticals.cmi eliminationTactics.cmi +eliminationTactics.cmx: primitiveTactics.cmx proofEngineStructuralRules.cmx \ + tacticals.cmx eliminationTactics.cmi +negationTactics.cmo: eliminationTactics.cmi primitiveTactics.cmi \ + proofEngineTypes.cmo tacticals.cmi variousTactics.cmi negationTactics.cmi +negationTactics.cmx: eliminationTactics.cmx primitiveTactics.cmx \ + proofEngineTypes.cmx tacticals.cmx variousTactics.cmx negationTactics.cmi +equalityTactics.cmo: introductionTactics.cmi primitiveTactics.cmi \ + proofEngineHelpers.cmi proofEngineReduction.cmi \ + proofEngineStructuralRules.cmi proofEngineTypes.cmo reductionTactics.cmi \ + tacticals.cmi equalityTactics.cmi +equalityTactics.cmx: introductionTactics.cmx primitiveTactics.cmx \ + proofEngineHelpers.cmx proofEngineReduction.cmx \ + proofEngineStructuralRules.cmx proofEngineTypes.cmx reductionTactics.cmx \ + tacticals.cmx equalityTactics.cmi +discriminationTactics.cmo: eliminationTactics.cmi equalityTactics.cmi \ + introductionTactics.cmi primitiveTactics.cmi proofEngineTypes.cmo \ + tacticals.cmi discriminationTactics.cmi +discriminationTactics.cmx: eliminationTactics.cmx equalityTactics.cmx \ + introductionTactics.cmx primitiveTactics.cmx proofEngineTypes.cmx \ + tacticals.cmx discriminationTactics.cmi +ring.cmo: eliminationTactics.cmi equalityTactics.cmi primitiveTactics.cmi \ + proofEngineStructuralRules.cmi proofEngineTypes.cmo tacticals.cmi \ + ring.cmi +ring.cmx: eliminationTactics.cmx equalityTactics.cmx primitiveTactics.cmx \ + proofEngineStructuralRules.cmx proofEngineTypes.cmx tacticals.cmx \ + ring.cmi +fourierR.cmo: equalityTactics.cmi fourier.cmi primitiveTactics.cmi \ + proofEngineHelpers.cmi proofEngineTypes.cmo reductionTactics.cmi ring.cmi \ + tacticals.cmi fourierR.cmi +fourierR.cmx: equalityTactics.cmx fourier.cmx primitiveTactics.cmx \ + proofEngineHelpers.cmx proofEngineTypes.cmx reductionTactics.cmx ring.cmx \ + tacticals.cmx fourierR.cmi diff --git a/helm/ocaml/urimanager/.depend b/helm/ocaml/urimanager/.depend new file mode 100644 index 000000000..482148423 --- /dev/null +++ b/helm/ocaml/urimanager/.depend @@ -0,0 +1,2 @@ +uriManager.cmo: uriManager.cmi +uriManager.cmx: uriManager.cmi diff --git a/helm/ocaml/xml/.depend b/helm/ocaml/xml/.depend new file mode 100644 index 000000000..bc6941bdf --- /dev/null +++ b/helm/ocaml/xml/.depend @@ -0,0 +1,2 @@ +xml.cmo: xml.cmi +xml.cmx: xml.cmi