Add support for "-bypass-API" argument of "coq_makefile"

Plugin-writers can now use:

  -bypass-API

parameter with "coq_makefile".

The effect of that is that instead of

  -I API

the plugin will be compiled with:

  -I config" -I dev -I lib -I kernel -I library -I engine -I pretyping -I interp -I parsing -I proofs -I tactics -I toplevel -I printing -I intf -I grammar -I ide -I stm -I vernac

16 files changed, 112 insertions, 28 deletions

diff --git a/.gitignore b/.gitignore
index 84fe89d1e..fa83045e7 100644
--- a/.gitignore
+++ b/.gitignore
@@ -72,6 +72,8 @@ test-suite/coq-makefile/*/mlihtml
 test-suite/coq-makefile/*/subdir/done
 test-suite/coq-makefile/latex1/all.pdf
 test-suite/coq-makefile/merlin1/.merlin
+test-suite/coq-makefile/plugin-reach-outside-API-and-fail/_CoqProject
+test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/_CoqProject
 
 # documentation
 
diff --git a/config/coq_config.mli b/config/coq_config.mli
index 2b3bc2c25..3f7b65c39 100644
--- a/config/coq_config.mli
+++ b/config/coq_config.mli
@@ -53,7 +53,10 @@ val compile_date : string (* compile date *)
 val vo_magic_number : int
 val state_magic_number : int
 
+val core_src_dirs : string list
+val api_dirs : string list
 val plugins_dirs : string list
+val all_src_dirs : string list
 
 val exec_extension : string (* "" under Unix, ".exe" under MS-windows *)
 val with_geoproof : bool ref (* to (de)activate functions specific to Geoproof with Coqide *)
diff --git a/configure.ml b/configure.ml
index a5204d5b5..316cea5c9 100644
--- a/configure.ml
+++ b/configure.ml
@@ -1088,7 +1088,19 @@ let write_configml f =
   pr_s "wwwstdlib" (!Prefs.coqwebsite ^ "distrib/" ^ coq_version ^ "/stdlib/");
   pr_s "localwwwrefman"  ("file:/" ^ docdir ^ "/html/refman");
   pr_b "no_native_compiler" (not !Prefs.nativecompiler);
+
+  let core_src_dirs = [ "config"; "dev"; "kernel"; "library";
+                        "engine"; "pretyping"; "interp"; "parsing"; "proofs";
+                        "tactics"; "toplevel"; "printing"; "intf";
+                        "grammar"; "ide"; "stm"; "vernac" ] in
+  let core_src_dirs = List.fold_left (fun acc core_src_subdir -> acc ^ "  \"" ^ core_src_subdir ^ "\";\n")
+                                    ""
+                                    core_src_dirs in
+
+  pr "\nlet core_src_dirs = [\n%s]\n" core_src_dirs;
+  pr "\nlet api_dirs = [\"API\"; \"lib\"]\n";
   pr "\nlet plugins_dirs = [\n";
+
   let plugins = Sys.readdir "plugins" in
   Array.sort compare plugins;
   Array.iter
@@ -1097,6 +1109,9 @@ let write_configml f =
       if Sys.is_directory f' && f.[0] <> '.' then pr "  %S;\n" f')
     plugins;
   pr "]\n";
+
+  pr "\nlet all_src_dirs = core_src_dirs @ api_dirs @ plugins_dirs\n";
+
   close_out o;
   Unix.chmod f 0o444
 
diff --git a/lib/coqProject_file.ml4 b/lib/coqProject_file.ml4
index 7a1660569..97aa90e07 100644
--- a/lib/coqProject_file.ml4
+++ b/lib/coqProject_file.ml4
@@ -11,6 +11,7 @@ type project = {
   makefile : string option;
   install_kind  : install option;
   use_ocamlopt : bool;
+  bypass_API : bool;
 
   v_files : string list;
   mli_files : string list;
@@ -42,11 +43,12 @@ and install =
   | UserInstall
 
 (* TODO generate with PPX *)
-let mk_project project_file makefile install_kind use_ocamlopt = {
+let mk_project project_file makefile install_kind use_ocamlopt bypass_API = {
   project_file;
   makefile;
   install_kind;
   use_ocamlopt;
+  bypass_API;
 
   v_files = [];
   mli_files = [];
@@ -166,6 +168,8 @@ let process_cmd_line orig_dir proj args =
     aux { proj with defs = proj.defs @ [v,def] } r
   | "-arg" :: a :: r ->
     aux { proj with extra_args = proj.extra_args @ [a] } r
+  | "-bypass-API" :: r ->
+    aux { proj with bypass_API = true } r
   | f :: r ->
       let f = CUnix.correct_path f orig_dir in
       let proj =
@@ -185,11 +189,11 @@ let process_cmd_line orig_dir proj args =
  (******************************* API ************************************)
 
 let cmdline_args_to_project ~curdir args =
-  process_cmd_line curdir (mk_project None None None true) args
+  process_cmd_line curdir (mk_project None None None true false) args
 
 let read_project_file f =
   process_cmd_line (Filename.dirname f)
-    (mk_project (Some f) None (Some NoInstall) true) (parse f)
+    (mk_project (Some f) None (Some NoInstall) true false) (parse f)
 
 let rec find_project_file ~from ~projfile_name =
   let fname = Filename.concat from projfile_name in
diff --git a/lib/coqProject_file.mli b/lib/coqProject_file.mli
index 8c8fc068a..19fc9227a 100644
--- a/lib/coqProject_file.mli
+++ b/lib/coqProject_file.mli
@@ -13,6 +13,7 @@ type project = {
   makefile : string option;
   install_kind  : install option;
   use_ocamlopt : bool;
+  bypass_API : bool;
 
   v_files : string list;
   mli_files : string list;
diff --git a/lib/envars.ml b/lib/envars.ml
index 2f76183eb..47baf66a6 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -202,14 +202,7 @@ let xdg_dirs ~warn =
 
 (* Print the configuration information *)
 
-let coq_src_subdirs = [ 
-   "config" ; "dev" ; "lib" ; "kernel" ; "library" ;
-   "engine" ; "pretyping" ; "interp" ; "parsing" ; "proofs" ;
-   "tactics" ; "toplevel" ; "printing" ; "intf" ;
-   "grammar" ; "ide" ; "stm"; "vernac" ; "API" ] @
-   Coq_config.plugins_dirs
-  
-let print_config ?(prefix_var_name="") f =
+let print_config ?(prefix_var_name="") f coq_src_subdirs =
   let open Printf in 
   fprintf f "%sLOCAL=%s\n" prefix_var_name (if Coq_config.local then "1" else "0");
   fprintf f "%sCOQLIB=%s/\n" prefix_var_name (coqlib ());
diff --git a/lib/envars.mli b/lib/envars.mli
index c8bbf17d9..edd13447f 100644
--- a/lib/envars.mli
+++ b/lib/envars.mli
@@ -76,7 +76,4 @@ val xdg_data_dirs   : (string -> unit) -> string list
 val xdg_dirs : warn : (string -> unit) -> string list
 
 (** {6 Prints the configuration information } *)
-val print_config : ?prefix_var_name:string -> out_channel -> unit
-
-(** Directories in which coq sources are found *)
-val coq_src_subdirs : string list
+val print_config : ?prefix_var_name:string -> out_channel -> string list -> unit
diff --git a/test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh b/test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh
new file mode 100755
index 000000000..6301aa03c
--- /dev/null
+++ b/test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh
@@ -0,0 +1,37 @@
+#!/usr/bin/env bash
+
+set -e
+
+git clean -dfx
+
+cat > _CoqProject <<EOT
+-I src/
+
+./src/test_plugin.mllib
+./src/test.ml4
+./src/test.mli
+EOT
+
+mkdir src
+
+cat > src/test_plugin.mllib <<EOT
+Test
+EOT
+
+touch src/test.mli
+
+cat > src/test.ml4 <<EOT
+DECLARE PLUGIN "test"
+
+let _ = Pre_env.empty_env
+EOT
+
+${COQBIN}coq_makefile -f _CoqProject -o Makefile
+
+if make VERBOSE=1; then
+  # make command should have failed (but didn't)
+  exit 1
+else
+  # make command should have failed (and it indeed did)
+  exit 0
+fi
diff --git a/test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/run.sh b/test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/run.sh
new file mode 100755
index 000000000..991fb4a61
--- /dev/null
+++ b/test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/run.sh
@@ -0,0 +1,32 @@
+#!/usr/bin/env bash
+
+set -e
+
+git clean -dfx
+
+cat > _CoqProject <<EOT
+-bypass-API
+-I src/
+
+./src/test_plugin.mllib
+./src/test.ml4
+./src/test.mli
+EOT
+
+mkdir src
+
+cat > src/test_plugin.mllib <<EOT
+Test
+EOT
+
+touch src/test.mli
+
+cat > src/test.ml4 <<EOT
+DECLARE PLUGIN "test"
+
+let _ = Pre_env.empty_env
+EOT
+
+${COQBIN}coq_makefile -f _CoqProject -o Makefile
+
+make VERBOSE=1
diff --git a/test-suite/coq-makefile/template/src/test.ml4 b/test-suite/coq-makefile/template/src/test.ml4
index 72765abe0..e7d0bfe1f 100644
--- a/test-suite/coq-makefile/template/src/test.ml4
+++ b/test-suite/coq-makefile/template/src/test.ml4
@@ -1,3 +1,4 @@
+open API
 open Ltac_plugin
 DECLARE PLUGIN "test_plugin"
 let () = Mltop.add_known_plugin (fun () -> ()) "test_plugin";;
diff --git a/test-suite/coq-makefile/template/src/test_aux.ml b/test-suite/coq-makefile/template/src/test_aux.ml
index a01d0865a..e134abd84 100644
--- a/test-suite/coq-makefile/template/src/test_aux.ml
+++ b/test-suite/coq-makefile/template/src/test_aux.ml
@@ -1 +1 @@
-let tac = Proofview.tclUNIT ()
+let tac = API.Proofview.tclUNIT ()
diff --git a/test-suite/coq-makefile/template/src/test_aux.mli b/test-suite/coq-makefile/template/src/test_aux.mli
index 10020f27d..2e7ad1529 100644
--- a/test-suite/coq-makefile/template/src/test_aux.mli
+++ b/test-suite/coq-makefile/template/src/test_aux.mli
@@ -1 +1 @@
-val tac : unit Proofview.tactic
+val tac : unit API.Proofview.tactic
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 8e2f75fc9..e4f135977 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -27,11 +27,6 @@ let rec print_prefix_list sep = function
   | x :: l -> print sep; print x; print_prefix_list sep l
   | [] -> ()
 
-(* These are the Coq library directories that are used for
- * plugin development
- *)
-let lib_dirs = Envars.coq_src_subdirs
-
 let usage () =
   output_string stderr "Usage summary:\
 \n\
@@ -73,6 +68,7 @@ let usage () =
 \n[-f file]: take the contents of file as arguments\
 \n[-o file]: output should go in file file\
 \n	Output file outside the current directory is forbidden.\
+\n[-bypass-API]: when compiling plugins, bypass Coq API\
 \n[-h]: print this usage summary\
 \n[--help]: equivalent to [-h]\n";
   exit 1
@@ -197,9 +193,12 @@ let generate_conf_includes oc { ml_includes; r_includes; q_includes } =
     (S.concat " " (map (fun ({ path },l) -> dash2 "R" path l) r_includes))
 ;;
 
-let generate_conf_coq_config oc args =
+let generate_conf_coq_config oc args bypass_API =
   section oc "Coq configuration.";
-  Envars.print_config ~prefix_var_name:"COQMF_" oc;
+  let src_dirs = if bypass_API
+                 then Coq_config.all_src_dirs
+                 else Coq_config.api_dirs @ Coq_config.plugins_dirs in
+  Envars.print_config ~prefix_var_name:"COQMF_" oc src_dirs;
   fprintf oc "COQMF_MAKEFILE=%s\n" (quote (List.hd args)); 
 ;;
 
@@ -258,7 +257,7 @@ let generate_conf oc project args  =
   fprintf oc "# %s\n\n" (String.concat " " (List.map quote args));
   generate_conf_files oc project;
   generate_conf_includes oc project;
-  generate_conf_coq_config oc args;
+  generate_conf_coq_config oc args project.bypass_API;
   generate_conf_defs oc project;
   generate_conf_doc oc project;
   generate_conf_extra_target oc project.extra_targets;
diff --git a/tools/coqc.ml b/tools/coqc.ml
index 240531f12..c1f0182d9 100644
--- a/tools/coqc.ml
+++ b/tools/coqc.ml
@@ -83,7 +83,7 @@ let parse_args () =
 
     | ("-config" | "--config") :: _ ->
         Envars.set_coqlib ~fail:(fun x -> x);
-        Envars.print_config stdout;
+        Envars.print_config stdout Coq_config.all_src_dirs;
         exit 0
       
     |"--print-version" :: _ ->
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 8fca30268..16fe40555 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -124,7 +124,7 @@ let init_ocaml_path () =
     Mltop.add_ml_dir (List.fold_left (/) Envars.coqroot [dl])
   in
     Mltop.add_ml_dir (Envars.coqlib ());
-    List.iter add_subdir Envars.coq_src_subdirs
+    List.iter add_subdir Coq_config.all_src_dirs
 
 let get_compat_version = function
   | "8.7" -> Flags.Current
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 26ee413fb..31450ebd5 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -621,7 +621,7 @@ let init_toplevel arglist =
       Spawned.init_channels ();
       Envars.set_coqlib ~fail:(fun msg -> CErrors.user_err Pp.(str msg));
       if !print_where then (print_endline(Envars.coqlib ()); exit(exitcode ()));
-      if !print_config then (Envars.print_config stdout; exit (exitcode ()));
+      if !print_config then (Envars.print_config stdout Coq_config.all_src_dirs; exit (exitcode ()));
       if !print_tags then (print_style_tags (); exit (exitcode ()));
       if !filter_opts then (print_string (String.concat "\n" extras); exit 0);
       init_load_path ();