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 --- dev/base_include | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'dev') 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: *) -- cgit v1.2.3