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

1 files changed, 1 insertions, 1 deletions

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