diff options
Diffstat (limited to 'Makefile.dev')
| -rw-r--r-- | Makefile.dev | 46 |
1 files changed, 13 insertions, 33 deletions
diff --git a/Makefile.dev b/Makefile.dev index 1f81edc2c9..0105df972a 100644 --- a/Makefile.dev +++ b/Makefile.dev @@ -15,21 +15,13 @@ .PHONY: devel printers -DEBUGPRINTERS:=dev/top_printers.cmo dev/vm_printers.cmo dev/printers.cma +DEBUGPRINTERS:=dev/top_printers.cmo dev/vm_printers.cmo devel: printers -printers: $(DEBUGPRINTERS) +printers: $(CORECMA) $(DEBUGPRINTERS) dev/camlp4.dbg -dev/printers.cma: dev/printers.mllib - $(SHOW)'Testing $@' - $(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) $(SYSCMA) $(P4CMA) $(filter-out %.mllib, $^) -o test-printer - @rm -f test-printer - $(SHOW)'OCAMLC -a $@' - $(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) $(SYSCMA) $(P4CMA) $(filter-out %.mllib, $^) -linkall -a -o $@ - -dev/%.mllib.d: dev/%.mllib | $(OCAMLLIBDEP) $(GENFILES) - $(SHOW)'OCAMLLIBDEP $<' - $(HIDE)$(OCAMLLIBDEP) $(DEPFLAGS) -I dev "$<" $(TOTARGET) +dev/camlp4.dbg: + echo "load_printer gramlib.cma" > $@ ############ # revision @@ -105,7 +97,10 @@ minibyte: $(COQTOPBYTE) pluginsbyte pluginsopt: $(PLUGINSOPT) pluginsbyte: $(PLUGINS) -.PHONY: coqlight states miniopt minibyte pluginsopt pluginsbyte +# This should build all the ocaml code but not (most of) the .v files +coqocaml: tools coqbinaries pluginsopt coqide printers bin/votour + +.PHONY: coqlight states miniopt minibyte pluginsopt pluginsbyte coqocaml ########################## ### 2) core ML components @@ -124,10 +119,9 @@ pretyping: pretyping/pretyping.cma highparsing: parsing/highparsing.cma stm: stm/stm.cma toplevel: toplevel/toplevel.cma -ltac: ltac/ltac.cma -.PHONY: lib kernel byterun library proofs tactics interp parsing pretyping -.PHONY: engine highparsing stm toplevel ltac +.PHONY: lib kernel byterun library proofs tactics interp parsing pretyping API +.PHONY: engine highparsing stm toplevel ###################### ### 3) theories files @@ -186,6 +180,7 @@ RTAUTOVO:=$(filter plugins/rtauto/%, $(PLUGINSVO)) EXTRACTIONVO:=$(filter plugins/extraction/%, $(PLUGINSVO)) CCVO:= DERIVEVO:=$(filter plugins/derive/%, $(PLUGINSVO)) +LTACVO:=$(filter plugins/ltac/%, $(PLUGINSVO)) omega: $(OMEGAVO) $(OMEGACMO) $(ROMEGAVO) $(ROMEGACMO) micromega: $(MICROMEGAVO) $(MICROMEGACMO) $(CSDPCERT) @@ -197,25 +192,10 @@ funind: $(FUNINDCMO) $(FUNINDVO) cc: $(CCVO) $(CCCMO) rtauto: $(RTAUTOVO) $(RTAUTOCMO) btauto: $(BTAUTOVO) $(BTAUTOCMO) +ltac: $(LTACVO) $(LTACCMO) .PHONY: omega micromega setoid_ring nsatz extraction -.PHONY: fourier funind cc rtauto btauto - -################################# -### Misc other development rules -################################# - -# NOTA : otags only accepts camlp4 as preprocessor, so the following rule -# won't build tags of .ml4 when compiling with camlp5 - -otags: - otags $(MLIFILES) $(filter-out configure.ml, $(MLSTATICFILES)) \ - $(if $(filter camlp5,$(CAMLP4)), , \ - -pa op -pa g -pa m -pa rq $(addprefix -pa , $(CAMLP4DEPS)) \ - $(addprefix -impl , $(ML4FILES))) - -.PHONY: otags - +.PHONY: fourier funind cc rtauto btauto ltac # For emacs: # Local Variables: |