aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/db
diff options
context:
space:
mode:
authorGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2016-07-25 15:56:24 +0200
committerGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2016-07-26 16:32:49 +0200
commit32be84c5ba384f93b350a551d7bbbeec03768046 (patch)
tree13f29c903bb30d6335af4e7162692ed65eb61d5a /dev/db
parent41ef1ae0ad4043f308a06365f4e5b1369eb5d453 (diff)
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.
Diffstat (limited to 'dev/db')
-rw-r--r--dev/db3
1 files changed, 2 insertions, 1 deletions
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