diff options
| -rw-r--r-- | dev/base_include | 5 | ||||
| -rw-r--r-- | test-suite/dune | 8 | ||||
| -rwxr-xr-x | test-suite/misc/printers.sh | 16 | ||||
| -rw-r--r-- | toplevel/coqinit.ml | 2 |
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 |