[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.

.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

META.coq.in

@@ -25,6 +25,8 @@ package "config" (
 
   directory   = "config"
 
+  archive(byte)    = "config.cma"
+  archive(native)  = "config.cmxa"
 )
 
 package "clib" (

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
 

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 $@'

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 [email protected]
 
 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 $@ $^
 

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

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

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)

checker/check.mllib

@@ -1,5 +1,3 @@
-Coq_config
-
 Analyze
 Hook
 Terminal

config/config.mllib

@@ -0,0 +1 @@
+Coq_config

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

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

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

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

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

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