Imported Upstream version 8.8.2upstream/8.8.2

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: