[test-suite] Fix printers test

- fix the printers themselves after discharge was moved to the kernel

- change the test to make it more robust
  In addition to checking that there is no "Error|Unbound" in the
  output, ensure that the "go" function at the end of base_include
  is defined. If there are any errors in base_include it won't be defined.

This makes us find out that the test was silently failing in all CI
jobs except trunk+make. It failed to find the "include" file and so
failed with "could not find file include.", which we didn't detect.
To fix this:

- change automatically included paths in Coqinit.init_ocaml_path to be
  based on coqlib instead of coqroot. This way top_printers.ml and
  base_include can find the compiled ml objects.

- fix for dune: adapt the script to use include_dune when INSIDE_DUNE,
  add dependencies to test-suite/dune.

  The dependencies should be calculated automatically once Dune has
  better support for debug, or we implement proper support for test
  printers.

Co-authored-by: Emilio Jesus Gallego Arias <e+git@x80.org>

4 files changed, 27 insertions, 4 deletions

diff --git a/dev/base_include b/dev/base_include
index f764eaf4f5..b30bbaa3fa 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -142,7 +142,6 @@ open Ind_tables
 open Auto_ind_decl
 open Coqinit
 open Coqtop
-open Discharge
 open Himsg
 open Metasyntax
 open Mltop
@@ -209,3 +208,7 @@ let _ =
  print_string
    ("\n\tOcaml toplevel with Coq printers and utilities (use go();; to exit)\n\n");
  flush_all()
+
+(* Local Variables: *)
+(* mode: tuareg *)
+(* End: *)
diff --git a/test-suite/dune b/test-suite/dune
index 041c181d66..6ab2988331 100644
--- a/test-suite/dune
+++ b/test-suite/dune
@@ -20,6 +20,14 @@
    ../dev/header.ml
    ../dev/tools/update-compat.py
    ../doc/stdlib/index-list.html.template
+   ; For the misc/printers.sh test
+   ../dev/incdir_dune
+   ../dev/base_include
+   ../dev/inc_ltac_dune
+   ../dev/include_printers
+   ../dev/include_dune
+   ../dev/top_printers.ml
+   ../dev/vm_printers.ml
    ; For the changelog test
    ../config/coq_config.py
    (source_tree doc/changelog)
diff --git a/test-suite/misc/printers.sh b/test-suite/misc/printers.sh
index f659fce680..f2bf6b8681 100755
--- a/test-suite/misc/printers.sh
+++ b/test-suite/misc/printers.sh
@@ -3,6 +3,18 @@
 command -v "${BIN}coqtop.byte" || { echo "Missing coqtop.byte"; exit 1; }
 
 f=$(mktemp)
-printf 'Drop. #use"include";; #quit;;\n' | "${BIN}coqtop.byte" -q 2>&1 | tee "$f"
+{
+    if [ -n "$INSIDE_DUNE" ]; then
+        printf 'Drop.\n#directory "../dev";;\n#use "include_dune";;\n#quit;;\n' | coqtop.byte -q
+    else
+        # -I ../dev is not needed when compiled with -local (usual dev
+        # setup), but is needed for CI testing.
+        printf 'Drop. #use "include";; #quit;;\n' | "${BIN}coqtop.byte" -I ../dev -q
+    fi
+} 2>&1 | tee "$f"
 
-if grep -q -E "Error|Unbound" "$f"; then exit 1; fi
+# if there's an issue in base_include 'go' won't be defined
+# if there's an issue in include_printers it will be an undefined printer
+if ! grep -q -F 'val go : unit -> unit = <fun>' "$f" ||
+        grep -q -E "Error|Unbound" "$f";
+then exit 1; fi
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index ce1b3c7896..6ffb2ae815 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -118,7 +118,7 @@ let init_ocaml_path () =
   let open Loadpath in
   let lp s = { recursive = false; path_spec = MlPath s } in
   let add_subdir dl =
-    Loadpath.add_coq_path (lp (List.fold_left (/) Envars.coqroot [dl]))
+    Loadpath.add_coq_path (lp (List.fold_left (/) (Envars.coqlib()) [dl]))
   in
     Loadpath.add_coq_path (lp (Envars.coqlib ()));
     List.iter add_subdir Coq_config.all_src_dirs