[build] Refactoring to config lib and ocamldebug tweaks.

We make `config` into a properly library. This is more uniform and
useful for some clients. This also matches what was done in Dune.

Next step would be to push dependencies on `Coq_config` upwards, only
the actual toplevel binaries should depend on it.

We also remove the stale `camlp5.dbg` and refactor the dbg files a
bit, isolating the bits that are specific to the plugin / lib building
method used by makefile.

18 files changed, 143 insertions, 142 deletions

diff --git a/.gitignore b/.gitignore
index 538124b8e5..709e87cc9c 100644
--- a/.gitignore
+++ b/.gitignore
@@ -55,7 +55,6 @@ config/coq_config.ml
 config/coq_config.py
 config/Info-*.plist
 dev/ocamldebug-coq
-dev/camlp5.dbg
 plugins/micromega/csdpcert
 plugins/micromega/.micromega.ml.generated
 kernel/byterun/dllcoqrun.so
diff --git a/META.coq.in b/META.coq.in
index 1ccde1338f..16928587cb 100644
--- a/META.coq.in
+++ b/META.coq.in
@@ -25,6 +25,8 @@ package "config" (
 
   directory   = "config"
 
+  archive(byte)    = "config.cma"
+  archive(native)  = "config.cmxa"
 )
 
 package "clib" (
diff --git a/Makefile b/Makefile
index b74e4e5d4f..9ac32625ab 100644
--- a/Makefile
+++ b/Makefile
@@ -261,7 +261,7 @@ cacheclean:
 	find theories plugins test-suite -name '.*.aux' -exec rm -f {} +
 
 cleanconfig:
-	rm -f config/Makefile config/coq_config.ml dev/ocamldebug-coq dev/camlp5.dbg config/Info-*.plist
+	rm -f config/Makefile config/coq_config.ml dev/ocamldebug-coq config/Info-*.plist
 
 distclean: clean cleanconfig cacheclean timingclean
 
diff --git a/Makefile.build b/Makefile.build
index 77fcfc0abf..08863014ea 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -441,7 +441,7 @@ $(COQTOPBYTE): $(LINKCMO) $(LIBCOQRUN) $(COQTOP_BYTE)
 			 $(LINKCMO) $(BYTEFLAGS) $(COQTOP_BYTE) -o $@
 
 # For coqc
-COQCCMO:=clib/clib.cma lib/lib.cma toplevel/usage.cmo tools/coqc.cmo
+COQCCMO:=config/config.cma clib/clib.cma lib/lib.cma toplevel/usage.cmo tools/coqc.cmo
 
 $(COQC): $(call bestobj, $(COQCCMO))
 	$(SHOW)'OCAMLBEST -o $@'
@@ -502,7 +502,7 @@ $(OCAMLLIBDEPBYTE): tools/ocamllibdep.cmo
 
 # The full coqdep (unused by this build, but distributed by make install)
 
-COQDEPCMO:=clib/clib.cma lib/lib.cma tools/coqdep_lexer.cmo	\
+COQDEPCMO:=config/config.cma clib/clib.cma lib/lib.cma tools/coqdep_lexer.cmo	\
   tools/coqdep_common.cmo tools/coqdep.cmo
 
 $(COQDEP): $(call bestobj, $(COQDEPCMO))
@@ -513,7 +513,7 @@ $(COQDEPBYTE): $(COQDEPCMO)
 	$(SHOW)'OCAMLC -o $@'
 	$(HIDE)$(call ocamlbyte, $(SYSMOD))
 
-COQMAKEFILECMO:=clib/clib.cma lib/lib.cma tools/coq_makefile.cmo
+COQMAKEFILECMO:=config/config.cma clib/clib.cma lib/lib.cma tools/coq_makefile.cmo
 
 $(COQMAKEFILE): $(call bestobj,$(COQMAKEFILECMO))
 	$(SHOW)'OCAMLBEST -o $@'
@@ -539,7 +539,7 @@ $(COQWCBYTE): tools/coqwc.cmo
 	$(SHOW)'OCAMLC -o $@'
 	$(HIDE)$(call ocamlbyte, -package str)
 
-COQDOCCMO:=clib/clib.cma lib/lib.cma $(addprefix tools/coqdoc/, \
+COQDOCCMO:=config/config.cma clib/clib.cma lib/lib.cma $(addprefix tools/coqdoc/, \
   cdglobals.cmo alpha.cmo index.cmo tokens.cmo output.cmo cpretty.cmo main.cmo )
 
 $(COQDOC): $(call bestobj, $(COQDOCCMO))
@@ -550,7 +550,7 @@ $(COQDOCBYTE): $(COQDOCCMO)
 	$(SHOW)'OCAMLC -o $@'
 	$(HIDE)$(call ocamlbyte, -package str,unix)
 
-COQWORKMGRCMO:=clib/clib.cma lib/lib.cma stm/spawned.cmo stm/coqworkmgrApi.cmo tools/coqworkmgr.cmo
+COQWORKMGRCMO:=config/config.cma clib/clib.cma lib/lib.cma stm/spawned.cmo stm/coqworkmgrApi.cmo tools/coqworkmgr.cmo
 
 $(COQWORKMGR): $(call bestobj, $(COQWORKMGRCMO))
 	$(SHOW)'OCAMLBEST -o $@'
@@ -563,7 +563,7 @@ $(COQWORKMGRBYTE): $(COQWORKMGRCMO)
 # fake_ide : for debugging or test-suite purpose, a fake ide simulating
 # a connection to coqidetop
 
-FAKEIDECMO:=clib/clib.cma lib/lib.cma ide/protocol/ideprotocol.cma ide/document.cmo ide/fake_ide.cmo
+FAKEIDECMO:=config/config.cma clib/clib.cma lib/lib.cma ide/protocol/ideprotocol.cma ide/document.cmo ide/fake_ide.cmo
 
 $(FAKEIDE): $(call bestobj, $(FAKEIDECMO)) | $(IDETOP)
 	$(SHOW)'OCAMLBEST -o $@'
diff --git a/Makefile.checker b/Makefile.checker
index 6c19a1a42b..e6b1541efa 100644
--- a/Makefile.checker
+++ b/Makefile.checker
@@ -49,7 +49,7 @@ checker/names.ml: kernel/names.ml
 	sed -i.bak '1i(* AUTOGENERATED FILE: DO NOT EDIT *)\n\n\n\n\n\n\n\n' $@ && rm $@.bak
 
 ifeq ($(BEST),opt)
-$(CHICKEN): checker/check.cmxa checker/main.mli checker/main.ml
+$(CHICKEN): config/config.cmxa checker/check.cmxa checker/main.mli checker/main.ml
 	$(SHOW)'OCAMLOPT -o $@'
 	$(HIDE)$(OCAMLOPT) -linkpkg $(SYSMOD) $(CHKLIBS) $(OPTFLAGS) $(LINKMETADATA) -o $@ $^
 	$(STRIP_HIDE) $@
@@ -59,7 +59,7 @@ $(CHICKEN): $(CHICKENBYTE)
 	cp $< $@
 endif
 
-$(CHICKENBYTE): checker/check.cma checker/main.mli checker/main.ml
+$(CHICKENBYTE): config/config.cma checker/check.cma checker/main.mli checker/main.ml
 	$(SHOW)'OCAMLC -o $@'
 	$(HIDE)$(OCAMLC) -linkpkg $(SYSMOD) $(CHKLIBS) $(BYTEFLAGS) $(CUSTOM) -o $@ $^
 
diff --git a/Makefile.common b/Makefile.common
index f90919a4bc..f2a11ee4b4 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -117,7 +117,7 @@ BYTERUN:=$(addprefix kernel/byterun/, \
 # respecting this order is useful for developers that want to load or link
 # the libraries directly
 
-CORECMA:=clib/clib.cma lib/lib.cma kernel/kernel.cma library/library.cma \
+CORECMA:=config/config.cma clib/clib.cma lib/lib.cma kernel/kernel.cma library/library.cma \
         engine/engine.cma pretyping/pretyping.cma interp/interp.cma proofs/proofs.cma \
         parsing/parsing.cma printing/printing.cma tactics/tactics.cma vernac/vernac.cma \
         stm/stm.cma toplevel/toplevel.cma
diff --git a/Makefile.dev b/Makefile.dev
index 6a2a1b2101..54710b6690 100644
--- a/Makefile.dev
+++ b/Makefile.dev
@@ -20,10 +20,7 @@
 DEBUGPRINTERS:=dev/top_printers.cmo dev/vm_printers.cmo dev/checker_printers.cmo
 
 devel: printers
-printers: $(CORECMA) $(DEBUGPRINTERS) dev/camlp5.dbg
-
-dev/camlp5.dbg:
-	echo "load_printer gramlib.cma" > $@
+printers: $(CORECMA) $(DEBUGPRINTERS)
 
 ############
 # revision
diff --git a/Makefile.ide b/Makefile.ide
index cb55960203..6c069a1e50 100644
--- a/Makefile.ide
+++ b/Makefile.ide
@@ -43,7 +43,7 @@ IDESRCDIRS:= $(CORESRCDIRS) ide ide/protocol
 
 COQIDEFLAGS=$(addprefix -I , $(IDESRCDIRS)) $(COQIDEINCLUDES)
 
-IDEDEPS:=clib/clib.cma lib/lib.cma ide/protocol/ideprotocol.cma
+IDEDEPS:=config/config.cma clib/clib.cma lib/lib.cma ide/protocol/ideprotocol.cma
 IDECMA:=ide/ide.cma
 IDETOPEXE=bin/coqidetop$(EXE)
 IDETOP=bin/coqidetop.opt$(EXE)
diff --git a/checker/check.mllib b/checker/check.mllib
index 139fa765b4..173ad1e325 100644
--- a/checker/check.mllib
+++ b/checker/check.mllib
@@ -1,5 +1,3 @@
-Coq_config
-
 Analyze
 Hook
 Terminal
diff --git a/config/config.mllib b/config/config.mllib
new file mode 100644
index 0000000000..ce3ddfca69
--- /dev/null
+++ b/config/config.mllib
@@ -0,0 +1 @@
+Coq_config
diff --git a/dev/base_db b/dev/base_db
index e18ac534ac..155e9591e0 100644
--- a/dev/base_db
+++ b/dev/base_db
@@ -1,4 +1,5 @@
 source core.dbg
+load_printer ltac_plugin.cmo
 load_printer top_printers.cmo
 install_printer Top_printers.ppid
 install_printer Top_printers.ppsp
diff --git a/dev/checker.dbg b/dev/checker.dbg
index b2323b6175..b5b7f0e6d3 100644
--- a/dev/checker.dbg
+++ b/dev/checker.dbg
@@ -2,5 +2,6 @@ load_printer threads.cma
 load_printer str.cma
 load_printer clib.cma
 load_printer dynlink.cma
+load_printer config.cma
 load_printer lib.cma
 load_printer check.cma
diff --git a/dev/checker_db b/dev/checker_db
index 327e636c57..fcb6f679ed 100644
--- a/dev/checker_db
+++ b/dev/checker_db
@@ -2,38 +2,4 @@ source checker.dbg
 
 load_printer checker_printers.cmo
 
-install_printer Checker_printers.pP
-
-install_printer Checker_printers.ppfuture
-
-install_printer Checker_printers.ppid
-install_printer Checker_printers.pplab
-install_printer Checker_printers.ppmbid
-install_printer Checker_printers.ppdir
-install_printer Checker_printers.ppmp
-install_printer Checker_printers.ppcon
-install_printer Checker_printers.ppproj
-install_printer Checker_printers.ppkn
-install_printer Checker_printers.ppmind
-install_printer Checker_printers.ppind
-
-install_printer Checker_printers.ppbigint
-
-install_printer Checker_printers.ppintset
-install_printer Checker_printers.ppidset
-
-install_printer Checker_printers.ppidmapgen
-
-install_printer Checker_printers.ppididmap
-
-install_printer Checker_printers.ppuni
-install_printer Checker_printers.ppuni_level
-install_printer Checker_printers.ppuniverse_set
-install_printer Checker_printers.ppuniverse_instance
-install_printer Checker_printers.ppauniverse_context
-install_printer Checker_printers.ppuniverse_context
-install_printer Checker_printers.ppconstraints
-install_printer Checker_printers.ppuniverse_context_future
-install_printer Checker_printers.ppuniverses
-
-install_printer Checker_printers.pploc
+source checker_printers.dbg
diff --git a/dev/checker_printers.dbg b/dev/checker_printers.dbg
new file mode 100644
index 0000000000..9ebbd74834
--- /dev/null
+++ b/dev/checker_printers.dbg
@@ -0,0 +1,35 @@
+install_printer Checker_printers.pP
+
+install_printer Checker_printers.ppfuture
+
+install_printer Checker_printers.ppid
+install_printer Checker_printers.pplab
+install_printer Checker_printers.ppmbid
+install_printer Checker_printers.ppdir
+install_printer Checker_printers.ppmp
+install_printer Checker_printers.ppcon
+install_printer Checker_printers.ppproj
+install_printer Checker_printers.ppkn
+install_printer Checker_printers.ppmind
+install_printer Checker_printers.ppind
+
+install_printer Checker_printers.ppbigint
+
+install_printer Checker_printers.ppintset
+install_printer Checker_printers.ppidset
+
+install_printer Checker_printers.ppidmapgen
+
+install_printer Checker_printers.ppididmap
+
+install_printer Checker_printers.ppuni
+install_printer Checker_printers.ppuni_level
+install_printer Checker_printers.ppuniverse_set
+install_printer Checker_printers.ppuniverse_instance
+install_printer Checker_printers.ppauniverse_context
+install_printer Checker_printers.ppuniverse_context
+install_printer Checker_printers.ppconstraints
+install_printer Checker_printers.ppuniverse_context_future
+install_printer Checker_printers.ppuniverses
+
+install_printer Checker_printers.pploc
diff --git a/dev/core.dbg b/dev/core.dbg
index 972ba701e4..f676b643e4 100644
--- a/dev/core.dbg
+++ b/dev/core.dbg
@@ -1,6 +1,7 @@
-source camlp5.dbg
 load_printer threads.cma
 load_printer str.cma
+load_printer gramlib.cma
+load_printer config.cma
 load_printer clib.cma
 load_printer dynlink.cma
 load_printer lib.cma
@@ -16,4 +17,3 @@ load_printer tactics.cma
 load_printer vernac.cma
 load_printer stm.cma
 load_printer toplevel.cma
-load_printer ltac_plugin.cmo
diff --git a/dev/db b/dev/db
index 2f8c13485a..8733c684af 100644
--- a/dev/db
+++ b/dev/db
@@ -1,88 +1,6 @@
 source core.dbg
+
+load_printer ltac_plugin.cmo
 load_printer top_printers.cmo
 
-install_printer Top_printers.pP
-install_printer Top_printers.ppfuture
-install_printer Top_printers.ppid
-install_printer Top_printers.pplab
-install_printer Top_printers.ppmbid
-install_printer Top_printers.ppdir
-install_printer Top_printers.ppmp
-install_printer Top_printers.ppcon
-install_printer Top_printers.ppproj
-install_printer Top_printers.ppkn
-install_printer Top_printers.ppmind
-install_printer Top_printers.ppind
-install_printer Top_printers.ppsp
-install_printer Top_printers.ppqualid
-install_printer Top_printers.ppclindex
-install_printer Top_printers.ppscheme
-install_printer Top_printers.ppwf_paths
-install_printer Top_printers.ppevar
-install_printer Top_printers.ppconstr
-install_printer Top_printers.ppsconstr
-install_printer Top_printers.ppeconstr
-install_printer Top_printers.ppconstr_expr
-install_printer Top_printers.ppglob_constr
-install_printer Top_printers.pppattern
-install_printer Top_printers.ppfconstr
-install_printer Top_printers.ppbigint
-install_printer Top_printers.ppintset
-install_printer Top_printers.ppidset
-install_printer Top_printers.ppidmapgen
-install_printer Top_printers.ppididmap
-install_printer Top_printers.ppconstrunderbindersidmap
-install_printer Top_printers.ppevarsubst
-install_printer Top_printers.ppunbound_ltac_var_map
-install_printer Top_printers.ppclosure
-install_printer Top_printers.ppclosedglobconstr
-install_printer Top_printers.ppclosedglobconstridmap
-install_printer Top_printers.ppglobal
-install_printer Top_printers.ppconst
-install_printer Top_printers.ppvar
-install_printer Top_printers.ppj
-install_printer Top_printers.ppsubst
-install_printer Top_printers.ppdelta
-install_printer Top_printers.pp_idpred
-install_printer Top_printers.pp_cpred
-install_printer Top_printers.pp_transparent_state
-install_printer Top_printers.pp_stack_t
-install_printer Top_printers.pp_cst_stack_t
-install_printer Top_printers.pp_state_t
-install_printer Top_printers.ppmetas
-install_printer Top_printers.ppevm
-install_printer Top_printers.ppexistentialset
-install_printer Top_printers.ppexistentialfilter
-install_printer Top_printers.ppclenv
-install_printer Top_printers.ppgoalgoal
-install_printer Top_printers.ppgoal
-install_printer Top_printers.pphintdb
-install_printer Top_printers.ppproofview
-install_printer Top_printers.ppopenconstr
-install_printer Top_printers.pproof
-install_printer Top_printers.ppuni
-install_printer Top_printers.ppuni_level
-install_printer Top_printers.ppuniverse_set
-install_printer Top_printers.ppuniverse_instance
-install_printer Top_printers.ppuniverse_context
-install_printer Top_printers.ppuniverse_context_set
-install_printer Top_printers.ppuniverse_subst
-install_printer Top_printers.ppuniverse_opt_subst
-install_printer Top_printers.ppuniverse_level_subst
-install_printer Top_printers.ppevar_universe_context
-install_printer Top_printers.ppconstraints
-install_printer Top_printers.ppuniverseconstraints
-install_printer Top_printers.ppuniverse_context_future
-install_printer Top_printers.ppcumulativity_info
-install_printer Top_printers.ppabstract_cumulativity_info
-install_printer Top_printers.ppuniverses
-install_printer Top_printers.ppnamedcontextval
-install_printer Top_printers.ppenv
-install_printer Top_printers.pptac
-install_printer Top_printers.ppobj
-install_printer Top_printers.pploc
-install_printer Top_printers.pp_argument_type
-install_printer Top_printers.pp_generic_argument
-install_printer Top_printers.ppgenarginfo
-install_printer Top_printers.ppgenargargt
-install_printer Top_printers.ppist
+source top_printers.dbg
diff --git a/dev/top_printers.dbg b/dev/top_printers.dbg
new file mode 100644
index 0000000000..eab88c7290
--- /dev/null
+++ b/dev/top_printers.dbg
@@ -0,0 +1,85 @@
+install_printer Top_printers.pP
+install_printer Top_printers.ppfuture
+install_printer Top_printers.ppid
+install_printer Top_printers.pplab
+install_printer Top_printers.ppmbid
+install_printer Top_printers.ppdir
+install_printer Top_printers.ppmp
+install_printer Top_printers.ppcon
+install_printer Top_printers.ppproj
+install_printer Top_printers.ppkn
+install_printer Top_printers.ppmind
+install_printer Top_printers.ppind
+install_printer Top_printers.ppsp
+install_printer Top_printers.ppqualid
+install_printer Top_printers.ppclindex
+install_printer Top_printers.ppscheme
+install_printer Top_printers.ppwf_paths
+install_printer Top_printers.ppevar
+install_printer Top_printers.ppconstr
+install_printer Top_printers.ppsconstr
+install_printer Top_printers.ppeconstr
+install_printer Top_printers.ppconstr_expr
+install_printer Top_printers.ppglob_constr
+install_printer Top_printers.pppattern
+install_printer Top_printers.ppfconstr
+install_printer Top_printers.ppbigint
+install_printer Top_printers.ppintset
+install_printer Top_printers.ppidset
+install_printer Top_printers.ppidmapgen
+install_printer Top_printers.ppididmap
+install_printer Top_printers.ppconstrunderbindersidmap
+install_printer Top_printers.ppevarsubst
+install_printer Top_printers.ppunbound_ltac_var_map
+install_printer Top_printers.ppclosure
+install_printer Top_printers.ppclosedglobconstr
+install_printer Top_printers.ppclosedglobconstridmap
+install_printer Top_printers.ppglobal
+install_printer Top_printers.ppconst
+install_printer Top_printers.ppvar
+install_printer Top_printers.ppj
+install_printer Top_printers.ppsubst
+install_printer Top_printers.ppdelta
+install_printer Top_printers.pp_idpred
+install_printer Top_printers.pp_cpred
+install_printer Top_printers.pp_transparent_state
+install_printer Top_printers.pp_stack_t
+install_printer Top_printers.pp_cst_stack_t
+install_printer Top_printers.pp_state_t
+install_printer Top_printers.ppmetas
+install_printer Top_printers.ppevm
+install_printer Top_printers.ppexistentialset
+install_printer Top_printers.ppexistentialfilter
+install_printer Top_printers.ppclenv
+install_printer Top_printers.ppgoalgoal
+install_printer Top_printers.ppgoal
+install_printer Top_printers.pphintdb
+install_printer Top_printers.ppproofview
+install_printer Top_printers.ppopenconstr
+install_printer Top_printers.pproof
+install_printer Top_printers.ppuni
+install_printer Top_printers.ppuni_level
+install_printer Top_printers.ppuniverse_set
+install_printer Top_printers.ppuniverse_instance
+install_printer Top_printers.ppuniverse_context
+install_printer Top_printers.ppuniverse_context_set
+install_printer Top_printers.ppuniverse_subst
+install_printer Top_printers.ppuniverse_opt_subst
+install_printer Top_printers.ppuniverse_level_subst
+install_printer Top_printers.ppevar_universe_context
+install_printer Top_printers.ppconstraints
+install_printer Top_printers.ppuniverseconstraints
+install_printer Top_printers.ppuniverse_context_future
+install_printer Top_printers.ppcumulativity_info
+install_printer Top_printers.ppabstract_cumulativity_info
+install_printer Top_printers.ppuniverses
+install_printer Top_printers.ppnamedcontextval
+install_printer Top_printers.ppenv
+install_printer Top_printers.pptac
+install_printer Top_printers.ppobj
+install_printer Top_printers.pploc
+install_printer Top_printers.pp_argument_type
+install_printer Top_printers.pp_generic_argument
+install_printer Top_printers.ppgenarginfo
+install_printer Top_printers.ppgenargargt
+install_printer Top_printers.ppist
diff --git a/lib/lib.mllib b/lib/lib.mllib
index 41b3622a99..206b2504db 100644
--- a/lib/lib.mllib
+++ b/lib/lib.mllib
@@ -1,5 +1,3 @@
-Coq_config
-
 Hook
 Flags
 Control