diff options
Diffstat (limited to 'Makefile.dev')
| -rw-r--r-- | Makefile.dev | 30 |
1 files changed, 14 insertions, 16 deletions
diff --git a/Makefile.dev b/Makefile.dev index 1f81edc2c9..ea6b8b9194 100644 --- a/Makefile.dev +++ b/Makefile.dev @@ -15,21 +15,18 @@ .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) - -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) +printers: $(CORECMA) $(DEBUGPRINTERS) dev/camlp4.dbg + +ifeq ($(CAMLP4),camlp5) +dev/camlp4.dbg: + echo "load_printer gramlib.cma" > $@ +else +dev/camlp4.dbg: + echo "load_printer camlp4lib.cma" > $@ +endif ############ # revision @@ -124,10 +121,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: engine highparsing stm toplevel ###################### ### 3) theories files @@ -186,6 +182,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,9 +194,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 +.PHONY: fourier funind cc rtauto btauto ltac ################################# ### Misc other development rules |