Merge PR#406: coq makefile2

5 files changed, 300 insertions, 5 deletions

diff --git a/lib/clib.mllib b/lib/clib.mllib
index 9eb479fcc..d5c938fe5 100644
--- a/lib/clib.mllib
+++ b/lib/clib.mllib
@@ -33,3 +33,4 @@ CUnix
 Envars
 Aux_file
 Monad
+CoqProject_file
diff --git a/lib/coqProject_file.ml4 b/lib/coqProject_file.ml4
new file mode 100644
index 000000000..7a1660569
--- /dev/null
+++ b/lib/coqProject_file.ml4
@@ -0,0 +1,215 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+type project = {
+  project_file  : string option;
+  makefile : string option;
+  install_kind  : install option;
+  use_ocamlopt : bool;
+
+  v_files : string list;
+  mli_files : string list;
+  ml4_files : string list;
+  ml_files : string list;
+  mllib_files : string list;
+  mlpack_files : string list;
+
+  ml_includes : path list;
+  r_includes  : (path * logic_path) list;
+  q_includes  : (path * logic_path) list;
+  extra_args : string list;
+  defs : (string * string) list;
+  
+  extra_targets : extra_target list;
+  subdirs : string list;
+}
+and extra_target = {
+  target : string;
+  dependencies : string;
+  phony : bool;
+  command : string;
+}
+and logic_path = string
+and path = { path : string; canonical_path : string }
+and install =
+  | NoInstall
+  | TraditionalInstall
+  | UserInstall
+
+(* TODO generate with PPX *)
+let mk_project project_file makefile install_kind use_ocamlopt = {
+  project_file;
+  makefile;
+  install_kind;
+  use_ocamlopt;
+
+  v_files = [];
+  mli_files = [];
+  ml4_files = [];
+  ml_files = [];
+  mllib_files = [];
+  mlpack_files = [];
+  extra_targets = [];
+  subdirs = [];
+  ml_includes = [];
+  r_includes = [];
+  q_includes = [];
+  extra_args = [];
+  defs = [];
+}
+
+(********************* utils ********************************************)
+
+let rec post_canonize f =
+  if Filename.basename f = Filename.current_dir_name
+  then let dir = Filename.dirname f in
+    if dir = Filename.current_dir_name then f else post_canonize dir
+  else f
+
+(* Avoid Sys.is_directory raise an exception (if the file does not exists) *)
+let is_directory f = Sys.file_exists f && Sys.is_directory f
+
+(********************* parser *******************************************)
+
+exception Parsing_error of string
+
+let rec parse_string = parser
+  | [< '' ' | '\n' | '\t' >] -> ""
+  | [< 'c; s >] -> (String.make 1 c)^(parse_string s)
+  | [< >] -> ""
+and parse_string2 = parser
+  | [< ''"' >] -> ""
+  | [< 'c; s >] -> (String.make 1 c)^(parse_string2 s)
+  | [< >] -> raise (Parsing_error "unterminated string")
+and parse_skip_comment = parser
+  | [< ''\n'; s >] -> s
+  | [< 'c; s >] -> parse_skip_comment s
+  | [< >] -> [< >]
+and parse_args = parser
+  | [< '' ' | '\n' | '\t'; s >] -> parse_args s
+  | [< ''#'; s >] -> parse_args (parse_skip_comment s)
+  | [< ''"'; str = parse_string2; s >] -> ("" ^ str) :: parse_args s
+  | [< 'c; str = parse_string; s >] -> ((String.make 1 c) ^ str) :: (parse_args s)
+  | [< >] -> []
+
+let parse f =
+  let c = open_in f in
+  let res = parse_args (Stream.of_channel c) in
+  close_in c;
+  res
+;;
+
+let process_cmd_line orig_dir proj args =
+  let orig_dir = (* avoids turning foo.v in ./foo.v *)
+    if orig_dir = "." then "" else orig_dir in
+  let error s = Feedback.msg_error (Pp.str (s^".")); exit 1 in
+  let mk_path d =
+    let p = CUnix.correct_path d orig_dir in
+    { path = CUnix.remove_path_dot (post_canonize p);
+      canonical_path = CUnix.canonical_path_name p } in
+  let rec aux proj = function
+  | [] -> proj
+  | "-impredicative-set" :: _ ->
+    error "Use \"-arg -impredicative-set\" instead of \"-impredicative-set\""
+  | "-no-install" :: _ ->
+    error "Use \"-install none\" instead of \"-no-install\""
+  | "-custom" :: _ ->
+    error "Use \"-extra[-phony] target deps command\" instead of \"-custom command deps target\""
+  
+  | ("-no-opt"|"-byte") :: r -> aux { proj with use_ocamlopt =  false } r
+  | ("-full"|"-opt") :: r -> aux { proj with use_ocamlopt =  true } r
+  | "-install" :: d :: r ->
+    if proj.install_kind <> None then
+      Feedback.msg_warning (Pp.str "-install set more than once.");
+    let install = match d with
+      | "user" -> UserInstall
+      | "none" -> NoInstall
+      | "global" -> TraditionalInstall
+      | _ -> error ("invalid option \""^d^"\" passed to -install") in
+    aux { proj with install_kind = Some install } r
+  | "-extra" :: target :: dependencies :: command :: r ->
+    let tgt = { target; dependencies; phony = false; command } in
+    aux { proj with extra_targets = proj.extra_targets @ [tgt] } r
+  | "-extra-phony" :: target :: dependencies :: command :: r ->
+    let tgt = { target; dependencies; phony = true; command } in
+    aux { proj with extra_targets = proj.extra_targets @ [tgt] } r
+
+  | "-Q" :: d :: lp :: r ->
+    aux { proj with q_includes = proj.q_includes @ [mk_path d,lp] } r
+  | "-I" :: d :: r ->
+    aux { proj with ml_includes = proj.ml_includes @ [mk_path d] } r
+  | "-R" :: d :: lp :: r ->
+    aux { proj with r_includes = proj.r_includes @ [mk_path d,lp] } r
+
+  | "-f" :: file :: r ->
+    let file = CUnix.remove_path_dot (CUnix.correct_path file orig_dir) in
+    let () = match proj.project_file with
+      | None -> ()
+      | Some _ -> Feedback.msg_warning (Pp.str
+	"Multiple project files are deprecated.")
+    in
+    let proj = aux { proj with project_file = Some file } (parse file) in
+    aux proj r
+
+  | "-o" :: file :: r ->
+    if String.contains file '/' then
+      error "Output file must be in the current directory";
+    if proj.makefile <> None then
+      error "Option -o given more than once";
+    aux { proj with makefile = Some file } r  
+  | v :: "=" :: def :: r ->
+    aux { proj with defs = proj.defs @ [v,def] } r
+  | "-arg" :: a :: r ->
+    aux { proj with extra_args = proj.extra_args @ [a] } r
+  | f :: r ->
+      let f = CUnix.correct_path f orig_dir in
+      let proj =
+        if is_directory f then { proj with subdirs = proj.subdirs @ [f] }
+        else match CUnix.get_extension f with
+        | ".v" -> { proj with v_files = proj.v_files @ [f] }
+        | ".ml" -> { proj with ml_files = proj.ml_files @ [f] }
+        | ".ml4" -> { proj with ml4_files = proj.ml4_files @ [f] }
+        | ".mli" -> { proj with mli_files = proj.mli_files @ [f] }
+        | ".mllib" -> { proj with mllib_files = proj.mllib_files @ [f] }
+        | ".mlpack" -> { proj with mlpack_files = proj.mlpack_files @ [f] }
+        | _ -> raise (Parsing_error ("Unknown option "^f)) in
+      aux proj r
+ in
+   aux proj args
+
+ (******************************* API ************************************)
+
+let cmdline_args_to_project ~curdir args =
+  process_cmd_line curdir (mk_project None None None true) args
+
+let read_project_file f =
+  process_cmd_line (Filename.dirname f)
+    (mk_project (Some f) None (Some NoInstall) true) (parse f)
+
+let rec find_project_file ~from ~projfile_name =
+  let fname = Filename.concat from projfile_name in
+  if Sys.file_exists fname then Some fname
+  else
+    let newdir = Filename.dirname from in
+    if newdir = "" || newdir = "/" then None
+    else find_project_file ~from:newdir ~projfile_name
+;;
+
+let coqtop_args_from_project
+  { ml_includes; r_includes; q_includes; extra_args }
+=
+  let map = List.map in
+  let args =
+    map (fun { canonical_path = i } -> ["-I"; i]) ml_includes @
+    map (fun ({ canonical_path = i }, l) -> ["-Q"; i; l]) q_includes @
+    map (fun ({ canonical_path = p }, l) -> ["-R"; p; l]) r_includes @
+    [extra_args] in
+  List.flatten args
+;;
+
+(* vim:set ft=ocaml: *)
diff --git a/lib/coqProject_file.mli b/lib/coqProject_file.mli
new file mode 100644
index 000000000..8c8fc068a
--- /dev/null
+++ b/lib/coqProject_file.mli
@@ -0,0 +1,52 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+exception Parsing_error of string
+
+type project = {
+  project_file  : string option;
+  makefile : string option;
+  install_kind  : install option;
+  use_ocamlopt : bool;
+
+  v_files : string list;
+  mli_files : string list;
+  ml4_files : string list;
+  ml_files : string list;
+  mllib_files : string list;
+  mlpack_files : string list;
+
+  ml_includes : path list;
+  r_includes  : (path * logic_path) list;
+  q_includes  : (path * logic_path) list;
+  extra_args : string list;
+  defs : (string * string) list;
+
+  (* deprecated in favor of a Makefile.local using :: rules *)
+  extra_targets : extra_target list;
+  subdirs : string list;
+
+}
+and extra_target = {
+  target : string;
+  dependencies : string;
+  phony : bool;
+  command : string;
+}
+and logic_path = string
+and path = { path : string; canonical_path : string }
+and install =
+  | NoInstall
+  | TraditionalInstall
+  | UserInstall
+
+val cmdline_args_to_project : curdir:string -> string list -> project
+val read_project_file : string -> project
+val coqtop_args_from_project : project -> string list
+val find_project_file : from:string -> projfile_name:string -> string option
+
diff --git a/lib/envars.ml b/lib/envars.ml
index 89ce52831..79516bb1b 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -146,12 +146,8 @@ let coqpath =
 
 let exe s = s ^ Coq_config.exec_extension
 
-let guess_ocamlfind () = which (user_path ()) (exe "ocamlfind")
-
 let ocamlfind () =
-  if !Flags.ocamlfind_spec then !Flags.ocamlfind else
-    if !Flags.boot then Coq_config.ocamlfind else
-      try guess_ocamlfind () / "ocamlfind"  with Not_found -> Coq_config.ocamlfind
+  if !Flags.ocamlfind_spec then !Flags.ocamlfind else Coq_config.ocamlfind
 
 (** {2 Camlp4 paths} *)
 
@@ -207,3 +203,28 @@ let xdg_config_dirs warn =
 
 let xdg_dirs ~warn =
   List.filter Sys.file_exists (xdg_data_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" ] @
+   Coq_config.plugins_dirs
+  
+let print_config ?(prefix_var_name="") f =
+  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 ());
+  fprintf f "%sDOCDIR=%s/\n" prefix_var_name (docdir ());
+  fprintf f "%sOCAMLFIND=%s\n" prefix_var_name (ocamlfind ());
+  fprintf f "%sCAMLP4=%s\n" prefix_var_name Coq_config.camlp4;
+  fprintf f "%sCAMLP4O=%s\n" prefix_var_name Coq_config.camlp4o;
+  fprintf f "%sCAMLP4BIN=%s/\n" prefix_var_name (camlp4bin ());
+  fprintf f "%sCAMLP4LIB=%s\n" prefix_var_name (camlp4lib ());
+  fprintf f "%sCAMLP4OPTIONS=%s\n" prefix_var_name Coq_config.camlp4compat;
+  fprintf f "%sHASNATDYNLINK=%s\n" prefix_var_name
+    (if Coq_config.has_natdynlink then "true" else "false");
+  fprintf f "%sCOQ_SRC_SUBDIRS=%s\n" prefix_var_name (String.concat " " coq_src_subdirs)
+
diff --git a/lib/envars.mli b/lib/envars.mli
index 90a42859b..b164e789d 100644
--- a/lib/envars.mli
+++ b/lib/envars.mli
@@ -69,3 +69,9 @@ val xdg_data_home   : (string -> unit) -> string
 val xdg_config_dirs : (string -> unit) -> string list
 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