From 32be84c5ba384f93b350a551d7bbbeec03768046 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Mon, 25 Jul 2016 15:56:24 +0200 Subject: 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. --- .gitignore | 1 + 1 file changed, 1 insertion(+) (limited to '.gitignore') 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 -- cgit v1.2.3