aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.gitignore2
-rw-r--r--config/coq_config.mli3
-rw-r--r--configure.ml15
-rw-r--r--lib/coqProject_file.ml410
-rw-r--r--lib/coqProject_file.mli1
-rw-r--r--lib/envars.ml9
-rw-r--r--lib/envars.mli5
-rwxr-xr-xtest-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh37
-rwxr-xr-xtest-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/run.sh32
-rw-r--r--test-suite/coq-makefile/template/src/test.ml41
-rw-r--r--test-suite/coq-makefile/template/src/test_aux.ml2
-rw-r--r--test-suite/coq-makefile/template/src/test_aux.mli2
-rw-r--r--tools/coq_makefile.ml15
-rw-r--r--tools/coqc.ml2
-rw-r--r--toplevel/coqinit.ml2
-rw-r--r--toplevel/coqtop.ml2
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 ();
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-15 13:14:52 +0000