diff options
Diffstat (limited to 'Makefile.dev')
-rw-r--r-- | Makefile.dev | 63 |
1 files changed, 22 insertions, 41 deletions
diff --git a/Makefile.dev b/Makefile.dev index 1f81edc2..0461fe07 100644 --- a/Makefile.dev +++ b/Makefile.dev @@ -1,10 +1,12 @@ -####################################################################### -# v # The Coq Proof Assistant / The Coq Development Team # -# <O___,, # INRIA-Rocquencourt & LRI-CNRS-Orsay # -# \VV/ ############################################################# -# // # This file is distributed under the terms of the # -# # GNU Lesser General Public License Version 2.1 # -####################################################################### +########################################################################## +## # The Coq Proof Assistant / The Coq Development Team ## +## v # INRIA, CNRS and contributors - Copyright 1999-2018 ## +## <O___,, # (see CREDITS file for the list of authors) ## +## \VV/ ############################################################### +## // # This file is distributed under the terms of the ## +## # GNU Lesser General Public License Version 2.1 ## +## # (see LICENSE file for the text of the license) ## +########################################################################## # Extra targets for developpers : # debug printers, revision, partial targets ... @@ -15,21 +17,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/camlp5.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/camlp5.dbg: + echo "load_printer gramlib.cma" > $@ ############ # revision @@ -105,7 +99,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 $(PLUGINSCMO:.cmo=$(DYNOBJ)) coqide printers bin/votour + +.PHONY: coqlight states miniopt minibyte pluginsopt pluginsbyte coqocaml ########################## ### 2) core ML components @@ -121,13 +118,11 @@ tactics: tactics/tactics.cma interp: interp/interp.cma parsing: parsing/parsing.cma 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 stm toplevel ###################### ### 3) theories files @@ -186,36 +181,22 @@ 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) setoid_ring: $(RINGVO) $(RINGCMO) nsatz: $(NSATZVO) $(NSATZCMO) -extraction: $(EXTRACTIONCMO) +extraction: $(EXTRACTIONCMO) $(EXTRACTIONVO) fourier: $(FOURIERVO) $(FOURIERCMO) 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: |