No more dev/printers.cma

 This file was only used during ocamldebug sessions (in the dev/db
 script). It was containing a large subset of the core cma files,
 up to the printing functions. There were a few notable exceptions,
 for instance no kernel/vm.cmo to avoid loading dllcoqrun.so in ocamldebug.
 But printers.cma was troublesome to maintain : almost each time an ML file
 was added/removed/renamed in the core of Coq, dev/printers.mllib
 had to be edited, in addition to the directory-specific .mllib
 (kernel/kernel.mllib and co). So I propose here to kill this file,
 and put instead in dev/db several "load_printer" of the core cma files.

 For that to work, we need to compile kernel/kernel.cma with the right
 -dllib and -dllpath options, but that shouldn't hurt (on the contrary).
 We also source now the camlpX cma in dev/db, via a new generated file
 dev/camlp4.dbg containing a load_printer of either gramlib.cma or
 camp4lib.cma.

 If one doesn't want to perform the whole "source db" at the start
 of an ocamldebug session, then the former "load_printer printers.cma"
 could be replaced by:

  source core.dbg
  load_printer top_printers.cmo

 See for instance the minimal dev/base_db.

11 files changed, 48 insertions, 243 deletions

diff --git a/.gitignore b/.gitignore
index dd09fc53e..d91a674e1 100644
--- a/.gitignore
+++ b/.gitignore
@@ -49,6 +49,7 @@ config/Makefile
 config/coq_config.ml
 config/Info-*.plist
 dev/ocamldebug-coq
+dev/camlp4.dbg
 plugins/micromega/csdpcert
 kernel/byterun/dllcoqrun.so
 coqdoc.sty
diff --git a/Makefile b/Makefile
index 6649542c8..1b0a63d62 100644
--- a/Makefile
+++ b/Makefile
@@ -227,7 +227,7 @@ cacheclean:
 	find theories plugins test-suite -name '.*.aux' -delete
 
 cleanconfig:
-	rm -f config/Makefile config/coq_config.ml myocamlbuild_config.ml dev/ocamldebug-v7 config/Info-*.plist
+	rm -f config/Makefile config/coq_config.ml myocamlbuild_config.ml dev/ocamldebug-coq dev/camlp4.dbg config/Info-*.plist
 
 distclean: clean cleanconfig cacheclean
 
diff --git a/Makefile.build b/Makefile.build
index d5f9887b9..228b2e736 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -505,6 +505,12 @@ test-suite: world $(ALLSTDLIB).v
 # but the -include mechanism should already ensure that we have
 # up-to-date dependencies.
 
+# Specific rule for kernel.cma, with $(VMBYTEFLAGS).
+# This helps loading dllcoqrun.so during an ocamldebug
+kernel/kernel.cma: kernel/kernel.mllib
+	$(SHOW)'OCAMLC -a -o $@'
+	$(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) $(VMBYTEFLAGS) -a -o $@ $(filter-out %.mllib, $^)
+
 %.cma: %.mllib
 	$(SHOW)'OCAMLC -a -o $@'
 	$(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -a -o $@ $(filter-out %.mllib, $^)
diff --git a/Makefile.dev b/Makefile.dev
index 501a7744a..d9db7055f 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
diff --git a/configure.ml b/configure.ml
index c8096b9e0..63cf138db 100644
--- a/configure.ml
+++ b/configure.ml
@@ -1091,6 +1091,7 @@ let write_makefile f =
   pr "LOCAL=%B\n\n" !Prefs.local;
   pr "# Bytecode link flags : should we use -custom or not ?\n";
   pr "CUSTOM=%s\n" custom_flag;
+  pr "VMBYTEFLAGS=%s\n" (String.concat " " vmbyteflags);
   pr "%s\n\n" !build_loadpath;
   pr "# Paths for true installation\n";
   List.iter (fun (v,msg,_,_) -> pr "# %s: path for %s\n" v msg) install_dirs;
diff --git a/dev/base_db b/dev/base_db
index b540aed6c..e18ac534a 100644
--- a/dev/base_db
+++ b/dev/base_db
@@ -1,6 +1,6 @@
-load_printer "gramlib.cma"
-load_printer "top_printers.cmo"
-install_printer Top_printers.prid
-install_printer Top_printers.prsp
-install_printer Top_printers.print_pure_constr
+source core.dbg
+load_printer top_printers.cmo
+install_printer Top_printers.ppid
+install_printer Top_printers.ppsp
+install_printer Top_printers.ppconstr
 
diff --git a/dev/core.dbg b/dev/core.dbg
new file mode 100644
index 000000000..a43aac89a
--- /dev/null
+++ b/dev/core.dbg
@@ -0,0 +1,16 @@
+source camlp4.dbg
+load_printer threads.cma
+load_printer str.cma
+load_printer clib.cma
+load_printer lib.cma
+load_printer kernel.cma
+load_printer library.cma
+load_printer engine.cma
+load_printer pretyping.cma
+load_printer interp.cma
+load_printer proofs.cma
+load_printer parsing.cma
+load_printer printing.cma
+load_printer tactics.cma
+load_printer stm.cma
+load_printer toplevel.cma
diff --git a/dev/db b/dev/db
index 86e35a3ec..1282352e6 100644
--- a/dev/db
+++ b/dev/db
@@ -1,4 +1,5 @@
-load_printer "printers.cma"
+source core.dbg
+load_printer top_printers.cmo
 
 install_printer Top_printers.ppfuture
 
diff --git a/dev/doc/debugging.txt b/dev/doc/debugging.txt
index f0df2fc37..79cde4884 100644
--- a/dev/doc/debugging.txt
+++ b/dev/doc/debugging.txt
@@ -51,8 +51,8 @@ Debugging from Caml debugger
      failure/error/anomaly has been raised
    - Alternatively, for an error or an anomaly, add breakpoints in the middle  
      of each of error* functions or anomaly* functions in lib/util.ml
-   - If "source db" fails, recompile printers.cma with
-     "make dev/printers.cma" and try again
+   - If "source db" fails, do a "make printers" and try again (it should build
+     top_printers.cmo and the core cma files).
 
 Global gprof-based profiling
 ============================
diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run
index f9310e076..46caca8d6 100644
--- a/dev/ocamldebug-coq.run
+++ b/dev/ocamldebug-coq.run
@@ -12,11 +12,13 @@
 [ -z "$COQTOP" -a -d "$PWD/kernel" ] && COQTOP=$PWD
 [ -z "$COQTOP" -a -d "$PWD/../kernel" ] && COQTOP=`dirname $PWD`
 
+export CAML_LD_LIBRARY_PATH=$COQTOP/kernel/byterun:$CAML_LD_LIBRARY_PATH
+
 exec $OCAMLDEBUG \
-	-I $CAMLP4LIB \
+	-I $CAMLP4LIB -I +threads \
 	-I $COQTOP \
 	-I $COQTOP/config -I $COQTOP/printing -I $COQTOP/grammar \
-	-I $COQTOP/lib -I $COQTOP/intf -I $COQTOP/kernel \
+	-I $COQTOP/lib -I $COQTOP/intf -I $COQTOP/kernel -I $COQTOP/kernel/byterun \
 	-I $COQTOP/library -I $COQTOP/engine \
 	-I $COQTOP/pretyping -I $COQTOP/parsing \
         -I $COQTOP/interp -I $COQTOP/proofs -I $COQTOP/tactics -I $COQTOP/stm \
diff --git a/dev/printers.mllib b/dev/printers.mllib
deleted file mode 100644
index 316549548..000000000
--- a/dev/printers.mllib
+++ /dev/null
@@ -1,219 +0,0 @@
-Coq_config
-
-Terminal
-Hook
-Canary
-Hashset
-Hashcons
-CSet
-CMap
-Int
-Dyn
-HMap
-Option
-Store
-Exninfo
-Backtrace
-IStream
-Pp_control
-Loc
-CList
-CString
-Tok
-Compat
-Flags
-Control
-Loc
-Serialize
-Stateid
-CObj
-CArray
-CStack
-Util
-Pp
-Ppstyle
-Richpp
-Feedback
-Segmenttree
-Unicodetable
-Unicode
-CErrors
-CWarnings
-Bigint
-CUnix
-Minisys
-System
-Envars
-Aux_file
-Profile
-Explore
-Predicate
-Rtree
-Heap
-Genarg
-Stateid
-CEphemeron
-Future
-RemoteCounter
-Monad
-
-Names
-Univ
-UGraph
-Esubst
-Uint31
-Sorts
-Evar
-Constr
-Context
-Vars
-Term
-Mod_subst
-Cbytecodes
-Copcodes
-Cemitcodes
-Nativevalues
-Primitives
-Nativeinstr
-Future
-Opaqueproof
-Declareops
-Retroknowledge
-Conv_oracle
-Pre_env
-Nativelambda
-Nativecode
-Nativelib
-Cbytegen
-Environ
-CClosure
-Reduction
-Nativeconv
-Type_errors
-Modops
-Inductive
-Typeops
-Fast_typeops
-Indtypes
-Cooking
-Term_typing
-Subtyping
-Mod_typing
-Nativelibrary
-Safe_typing
-Unionfind
-
-Summary
-Nameops
-Libnames
-Globnames
-Global
-Nametab
-Libobject
-Lib
-Loadpath
-Goptions
-Decls
-Heads
-Keys
-Locusops
-Miscops
-Universes
-Termops
-Namegen
-UState
-Evd
-Sigma
-Glob_ops
-Redops
-Pretype_errors
-Evarutil
-Reductionops
-Inductiveops
-Arguments_renaming
-Nativenorm
-Retyping
-Cbv
-
-Evardefine
-Evarsolve
-Recordops
-Evarconv
-Typing
-Patternops
-Constr_matching
-Find_subterm
-Tacred
-Classops
-Typeclasses_errors
-Logic_monad
-Proofview_monad
-Proofview
-Ftactic
-Geninterp
-Typeclasses
-Detyping
-Indrec
-Program
-Coercion
-Cases
-Pretyping
-Unification
-Declaremods
-Library
-States
-
-Genprint
-CLexer
-Ppextend
-Pputils
-Ppannotation
-Stdarg
-Constrarg
-Constrexpr_ops
-Genintern
-Notation_ops
-Notation
-Dumpglob
-Syntax_def
-Smartlocate
-Topconstr
-Reserve
-Impargs
-Implicit_quantifiers
-Constrintern
-Modintern
-Constrextern
-Goal
-Miscprint
-Logic
-Refiner
-Clenv
-Evar_refiner
-Refine
-Proof
-Proof_global
-Pfedit
-Decl_mode
-Ppconstr
-Pcoq
-Printer
-Pptactic
-Ppdecl_proof
-Egramml
-Egramcoq
-Tacsubst
-Trie
-Dn
-Btermdn
-Hints
-Himsg
-ExplainErr
-Locality
-Assumptions
-Vernacinterp
-Dischargedhypsmap
-Discharge
-Declare
-Ind_tables
-Top_printers