From a3549bef1b4d4498f91e6ad35ae65b48a2fb302f Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Wed, 19 Jun 2019 14:44:29 +0200 Subject: [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 --- test-suite/dune | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'test-suite/dune') 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) -- cgit v1.2.3