From 32be84c5ba384f93b350a551d7bbbeec03768046 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey <pierre.letouzey@inria.fr>
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.
---
 Makefile.dev | 23 ++++++++++-------------
 1 file changed, 10 insertions(+), 13 deletions(-)

(limited to 'Makefile.dev')

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
-- 
cgit v1.2.3