From c054dda76825435019ad1b29f7f4292d937d98f9 Mon Sep 17 00:00:00 2001
From: Matej Košík
Date: Tue, 30 May 2017 10:49:41 +0200
Subject: 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
---
 tools/coq_makefile.ml | 15 +++++++--------
 tools/coqc.ml         |  2 +-
 2 files changed, 8 insertions(+), 9 deletions(-)

(limited to 'tools')

diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 8e2f75fc9c..e4f1359774 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 240531f123..c1f0182d9c 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" :: _ ->
-- 
cgit v1.2.3