From 466e6a97c97e83679d49f0867d8f571402e1548f Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Thu, 23 Mar 2017 14:42:24 +0100 Subject: extract "plugins/micromega/micromega.ml{,i}" files from "plugins/micromega/MExtraction.v" --- Makefile.build | 10 ++++++++++ 1 file changed, 10 insertions(+) (limited to 'Makefile.build') diff --git a/Makefile.build b/Makefile.build index 8aedd9cec..32322cb0d 100644 --- a/Makefile.build +++ b/Makefile.build @@ -635,6 +635,16 @@ endif $(SHOW)'COQDEP $<' $(HIDE)$(COQDEPBOOT) -boot $(DEPNATDYN) "$<" $(TOTARGET) +# Below we provide those dependecies that are not discovered {coq,ocaml}dep programs. + +plugins/micromega/micromega.cmi \ +plugins/micromega/micromega.cmo \ +plugins/micromega/micromega.cmx \ +$(patsubst %.ml,%.ml.d,$(wildcard plugins/micromega/*.ml)) \ +$(patsubst %.mli,%.mli.d,$(wildcard plugins/micromega/*.mli)) \ +plugins/micromega/micromega_plugin.mlpack.d \ + : plugins/micromega/MExtraction.vo + ########################################################################### # To speed-up things a bit, let's dissuade make to attempt rebuilding makefiles -- cgit v1.2.3 From dfbb5c5dc82c30dd3bac46d14e5e7190bbe80a9b Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Fri, 7 Apr 2017 15:11:43 +0200 Subject: a solution that works also with make 3.81 --- Makefile.build | 35 +++++++++++++++++++++++++---------- 1 file changed, 25 insertions(+), 10 deletions(-) (limited to 'Makefile.build') diff --git a/Makefile.build b/Makefile.build index 32322cb0d..c8aa6d6c1 100644 --- a/Makefile.build +++ b/Makefile.build @@ -70,6 +70,29 @@ include Makefile.ide ## provides the 'coqide' rule include Makefile.install include Makefile.dev ## provides the 'printers' and 'revision' rules +########################################################################### +# Adding missing pieces of information not discovered by ocamldep +# due to the fact that: +# - plugins/micromega/micromega_plugin.ml +# - plugins/micromega/micromega_plugin.mli +# are generated (and not yet present when we run "ocamldep"). +########################################################################### + +plugins/micromega/micromega_plugin.cmo : plugins/micromega/micromega.cmo +plugins/micromega/micromega_plugin.cmx : plugins/micromega/micromega.cmx + +plugins/micromega/certificate.cmo plugins/micromega/coq_micromega.cmo plugins/micromega/csdpcert.cmo plugins/micromega/mfourier.cmo plugins/micromega/mutils.cmo plugins/micromega/polynomial.cmo : plugins/micromega/micromega.cmo + +plugins/micromega/certificate.cmx plugins/micromega/coq_micromega.cmx plugins/micromega/csdpcert.cmx plugins/micromega/mfourier.cmx plugins/micromega/mutils.cmx plugins/micromega/polynomial.cmx : plugins/micromega/micromega.cmx + +plugins/micromega/micromega.cmx plugins/micromega/micromega.cmo : plugins/micromega/micromega.cmi +plugins/micromega/micromega.cmi : plugins/micromega/micromega.mli + +plugins/micromega/micromega.mli plugins/micromega/micromega.ml : plugins/micromega/MExtraction.vo + @: + +########################################################################### + # This include below will lauch the build of all .d. # The - at front is for disabling warnings about currently missing ones. # For creating the missing .d, make will recursively build things like @@ -80,6 +103,8 @@ DEPENDENCIES := \ -include $(DEPENDENCIES) +plugins/micromega/micromega_FORPACK:= -for-pack Micromega_plugin + # All dependency includes must be declared secondary, otherwise make will # delete them if it decided to build them by dependency instead of because # of include, and they will then be automatically deleted, leading to an @@ -635,16 +660,6 @@ endif $(SHOW)'COQDEP $<' $(HIDE)$(COQDEPBOOT) -boot $(DEPNATDYN) "$<" $(TOTARGET) -# Below we provide those dependecies that are not discovered {coq,ocaml}dep programs. - -plugins/micromega/micromega.cmi \ -plugins/micromega/micromega.cmo \ -plugins/micromega/micromega.cmx \ -$(patsubst %.ml,%.ml.d,$(wildcard plugins/micromega/*.ml)) \ -$(patsubst %.mli,%.mli.d,$(wildcard plugins/micromega/*.mli)) \ -plugins/micromega/micromega_plugin.mlpack.d \ - : plugins/micromega/MExtraction.vo - ########################################################################### # To speed-up things a bit, let's dissuade make to attempt rebuilding makefiles -- cgit v1.2.3