diff options
| author |  Matej Kosik <m4tej.kosik@gmail.com> | 2017-04-07 15:11:43 +0200 |
|---|---|---|
| committer |  Matej Kosik <matej.kosik@inria.fr> | 2017-06-01 10:24:16 +0200 |
| commit | dfbb5c5dc82c30dd3bac46d14e5e7190bbe80a9b (patch) | |
| tree | 748745531cc5ef0134f0fcfee503383b3a9e7b23 /Makefile.build | |
| parent | 466e6a97c97e83679d49f0867d8f571402e1548f (diff) | |
a solution that works also with make 3.81
Diffstat (limited to 'Makefile.build')
| -rw-r--r-- | Makefile.build | 35 |
1 files changed, 25 insertions, 10 deletions
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 |