From 51f6c9fbd1efc2af87ce9f56bc0e2056d7c9152f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Wed, 27 Jun 2018 17:21:33 +0200
Subject: Turn CoqProject_file into a normal OCaml file.

---
 lib/coqProject_file.ml  | 269 ++++++++++++++++++++++++++++++++++++++++++++++++
 lib/coqProject_file.ml4 | 262 ----------------------------------------------
 2 files changed, 269 insertions(+), 262 deletions(-)
 create mode 100644 lib/coqProject_file.ml
 delete mode 100644 lib/coqProject_file.ml4

(limited to 'lib')

diff --git a/lib/coqProject_file.ml b/lib/coqProject_file.ml
new file mode 100644
index 000000000..6c2f8105d
--- /dev/null
+++ b/lib/coqProject_file.ml
@@ -0,0 +1,269 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(* This needs to go trou feedback as it is invoked from IDEs, but
+   ideally we would like to make this independent so it can be
+   bootstrapped. *)
+
+(* Note the problem with the error invokation below calling exit... *)
+(* let error msg = Feedback.msg_error msg *)
+let warning msg = Feedback.msg_warning Pp.(str msg)
+
+type arg_source = CmdLine | ProjectFile
+
+type 'a sourced = { thing : 'a; source : arg_source }
+
+type project = {
+  project_file  : string option;
+  makefile : string option;
+  install_kind  : install option;
+  use_ocamlopt : bool;
+
+  v_files : string sourced list;
+  mli_files : string sourced list;
+  ml4_files : string sourced list;
+  ml_files : string sourced list;
+  mllib_files : string sourced list;
+  mlpack_files : string sourced list;
+
+  ml_includes : path sourced list;
+  r_includes  : (path * logic_path) sourced list;
+  q_includes  : (path * logic_path) sourced list;
+  extra_args : string sourced list;
+  defs : (string * string) sourced list;
+
+  (* deprecated in favor of a Makefile.local using :: rules *)
+  extra_targets : extra_target sourced list;
+  subdirs : string sourced 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
+
+(********************* parser *******************************************)
+
+exception Parsing_error of string
+
+let rec parse_string s = match Stream.next s with
+| ' ' | '\n' | '\t' -> ""
+| c -> (String.make 1 c)^(parse_string s)
+| exception Stream.Failure -> ""
+
+and parse_string2 s = match Stream.next s with
+| '"' -> ""
+| c -> (String.make 1 c)^(parse_string2 s)
+| exception Stream.Failure -> raise (Parsing_error "unterminated string")
+
+and parse_skip_comment s = match Stream.next s with
+| '\n' -> s
+| _ -> parse_skip_comment s
+| exception Stream.Failure -> Stream.of_list []
+
+and parse_args s = match Stream.next s with
+| ' ' | '\n' | '\t' -> parse_args s
+| '#' -> parse_args (parse_skip_comment s)
+| '"' ->
+  let str = parse_string2 s in
+  ("" ^ str) :: parse_args s
+| c ->
+  let str = parse_string s in
+  ((String.make 1 c) ^ str) :: (parse_args s)
+| exception Stream.Failure -> []
+
+let parse f =
+  let c = open_in f in
+  let res = parse_args (Stream.of_channel c) in
+  close_in c;
+  res
+;;
+
+(* Copy from minisys.ml, since we don't see that file here *)
+let exists_dir dir =
+  let rec strip_trailing_slash dir =
+    let len = String.length dir in
+    if len > 0 && (dir.[len-1] = '/' || dir.[len-1] = '\\')
+    then strip_trailing_slash (String.sub dir 0 (len-1)) else dir in
+  try Sys.is_directory (strip_trailing_slash dir) with Sys_error _ -> false
+
+
+let process_cmd_line orig_dir proj args =
+  let parsing_project_file = ref (proj.project_file <> None) in
+  let sourced x = { thing = x; source = if !parsing_project_file then ProjectFile else CmdLine } in
+  let orig_dir = (* avoids turning foo.v in ./foo.v *)
+    if orig_dir = "." then "" else orig_dir in
+  let error s = (Format.eprintf "Error: @[%s@].@\n%!" 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
+      (warning "-install set more than once.@\n%!");
+    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 @ [sourced tgt] } r
+  | "-extra-phony" :: target :: dependencies :: command :: r ->
+    let tgt = { target; dependencies; phony = true; command } in
+    aux { proj with extra_targets = proj.extra_targets @ [sourced tgt] } r
+
+  | "-Q" :: d :: lp :: r ->
+    aux { proj with q_includes = proj.q_includes @ [sourced (mk_path d,lp)] } r
+  | "-I" :: d :: r ->
+    aux { proj with ml_includes = proj.ml_includes @ [sourced (mk_path d)] } r
+  | "-R" :: d :: lp :: r ->
+    aux { proj with r_includes = proj.r_includes @ [sourced (mk_path d,lp)] } r
+
+  | "-f" :: file :: r ->
+    if !parsing_project_file then
+      raise (Parsing_error ("Invalid option -f in project file " ^ Option.get proj.project_file));
+    let file = CUnix.remove_path_dot (CUnix.correct_path file orig_dir) in
+    let () = match proj.project_file with
+      | None -> ()
+      | Some _ -> warning "Multiple project files are deprecated.@\n%!"
+    in
+    parsing_project_file := true;
+    let proj = aux { proj with project_file = Some file } (parse file) in
+    parsing_project_file := false;
+    aux proj r
+
+  | "-o" :: file :: r ->
+    if !parsing_project_file then
+     raise (Parsing_error ("Invalid option -o in project file " ^ Option.get proj.project_file));
+    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 @ [sourced (v,def)] } r
+  | "-arg" :: a :: r ->
+    aux { proj with extra_args = proj.extra_args @ [sourced a] } r
+  | f :: r ->
+      let f = CUnix.correct_path f orig_dir in
+      let proj =
+        if exists_dir f then { proj with subdirs = proj.subdirs @ [sourced f] }
+        else match CUnix.get_extension f with
+          | ".v" ->
+            { proj with v_files = proj.v_files @ [sourced f] }
+        | ".ml" -> { proj with ml_files = proj.ml_files @ [sourced f] }
+        | ".ml4" -> { proj with ml4_files = proj.ml4_files @ [sourced f] }
+        | ".mli" -> { proj with mli_files = proj.mli_files @ [sourced f] }
+        | ".mllib" -> { proj with mllib_files = proj.mllib_files @ [sourced f] }
+        | ".mlpack" -> { proj with mlpack_files = proj.mlpack_files @ [sourced 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 = from then None
+    else find_project_file ~from:newdir ~projfile_name
+;;
+
+let all_files { v_files; ml_files; mli_files; ml4_files;
+                mllib_files; mlpack_files } =
+  v_files @ mli_files @ ml4_files @ ml_files @ mllib_files @ mlpack_files
+
+let map_sourced_list f l = List.map (fun x -> f x.thing) l
+;;
+
+let map_cmdline f l = CList.map_filter (function
+    | {thing=x; source=CmdLine} -> Some (f x)
+    | {source=ProjectFile} -> None) l
+
+let coqtop_args_from_project
+  { ml_includes; r_includes; q_includes; extra_args }
+=
+  let map = map_sourced_list  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 @
+    [map (fun x -> x) extra_args] in
+  List.flatten args
+;;
+
+let filter_cmdline l = CList.map_filter
+    (function {thing; source=CmdLine} -> Some thing | {source=ProjectFile} -> None)
+    l
+;;
+
+let forget_source {thing} = thing
+
+(* vim:set ft=ocaml: *)
diff --git a/lib/coqProject_file.ml4 b/lib/coqProject_file.ml4
deleted file mode 100644
index 61eb1dafd..000000000
--- a/lib/coqProject_file.ml4
+++ /dev/null
@@ -1,262 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-(* This needs to go trou feedback as it is invoked from IDEs, but
-   ideally we would like to make this independent so it can be
-   bootstrapped. *)
-
-(* Note the problem with the error invokation below calling exit... *)
-(* let error msg = Feedback.msg_error msg *)
-let warning msg = Feedback.msg_warning Pp.(str msg)
-
-type arg_source = CmdLine | ProjectFile
-
-type 'a sourced = { thing : 'a; source : arg_source }
-
-type project = {
-  project_file  : string option;
-  makefile : string option;
-  install_kind  : install option;
-  use_ocamlopt : bool;
-
-  v_files : string sourced list;
-  mli_files : string sourced list;
-  ml4_files : string sourced list;
-  ml_files : string sourced list;
-  mllib_files : string sourced list;
-  mlpack_files : string sourced list;
-
-  ml_includes : path sourced list;
-  r_includes  : (path * logic_path) sourced list;
-  q_includes  : (path * logic_path) sourced list;
-  extra_args : string sourced list;
-  defs : (string * string) sourced list;
-
-  (* deprecated in favor of a Makefile.local using :: rules *)
-  extra_targets : extra_target sourced list;
-  subdirs : string sourced 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
-
-(********************* 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
-;;
-
-(* Copy from minisys.ml, since we don't see that file here *)
-let exists_dir dir =
-  let rec strip_trailing_slash dir =
-    let len = String.length dir in
-    if len > 0 && (dir.[len-1] = '/' || dir.[len-1] = '\\')
-    then strip_trailing_slash (String.sub dir 0 (len-1)) else dir in
-  try Sys.is_directory (strip_trailing_slash dir) with Sys_error _ -> false
-
-
-let process_cmd_line orig_dir proj args =
-  let parsing_project_file = ref (proj.project_file <> None) in
-  let sourced x = { thing = x; source = if !parsing_project_file then ProjectFile else CmdLine } in
-  let orig_dir = (* avoids turning foo.v in ./foo.v *)
-    if orig_dir = "." then "" else orig_dir in
-  let error s = (Format.eprintf "Error: @[%s@].@\n%!" 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
-      (warning "-install set more than once.@\n%!");
-    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 @ [sourced tgt] } r
-  | "-extra-phony" :: target :: dependencies :: command :: r ->
-    let tgt = { target; dependencies; phony = true; command } in
-    aux { proj with extra_targets = proj.extra_targets @ [sourced tgt] } r
-
-  | "-Q" :: d :: lp :: r ->
-    aux { proj with q_includes = proj.q_includes @ [sourced (mk_path d,lp)] } r
-  | "-I" :: d :: r ->
-    aux { proj with ml_includes = proj.ml_includes @ [sourced (mk_path d)] } r
-  | "-R" :: d :: lp :: r ->
-    aux { proj with r_includes = proj.r_includes @ [sourced (mk_path d,lp)] } r
-
-  | "-f" :: file :: r ->
-    if !parsing_project_file then
-      raise (Parsing_error ("Invalid option -f in project file " ^ Option.get proj.project_file));
-    let file = CUnix.remove_path_dot (CUnix.correct_path file orig_dir) in
-    let () = match proj.project_file with
-      | None -> ()
-      | Some _ -> warning "Multiple project files are deprecated.@\n%!"
-    in
-    parsing_project_file := true;
-    let proj = aux { proj with project_file = Some file } (parse file) in
-    parsing_project_file := false;
-    aux proj r
-
-  | "-o" :: file :: r ->
-    if !parsing_project_file then
-     raise (Parsing_error ("Invalid option -o in project file " ^ Option.get proj.project_file));
-    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 @ [sourced (v,def)] } r
-  | "-arg" :: a :: r ->
-    aux { proj with extra_args = proj.extra_args @ [sourced a] } r
-  | f :: r ->
-      let f = CUnix.correct_path f orig_dir in
-      let proj =
-        if exists_dir f then { proj with subdirs = proj.subdirs @ [sourced f] }
-        else match CUnix.get_extension f with
-          | ".v" ->
-            { proj with v_files = proj.v_files @ [sourced f] }
-        | ".ml" -> { proj with ml_files = proj.ml_files @ [sourced f] }
-        | ".ml4" -> { proj with ml4_files = proj.ml4_files @ [sourced f] }
-        | ".mli" -> { proj with mli_files = proj.mli_files @ [sourced f] }
-        | ".mllib" -> { proj with mllib_files = proj.mllib_files @ [sourced f] }
-        | ".mlpack" -> { proj with mlpack_files = proj.mlpack_files @ [sourced 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 = from then None
-    else find_project_file ~from:newdir ~projfile_name
-;;
-
-let all_files { v_files; ml_files; mli_files; ml4_files;
-                mllib_files; mlpack_files } =
-  v_files @ mli_files @ ml4_files @ ml_files @ mllib_files @ mlpack_files
-
-let map_sourced_list f l = List.map (fun x -> f x.thing) l
-;;
-
-let map_cmdline f l = CList.map_filter (function
-    | {thing=x; source=CmdLine} -> Some (f x)
-    | {source=ProjectFile} -> None) l
-
-let coqtop_args_from_project
-  { ml_includes; r_includes; q_includes; extra_args }
-=
-  let map = map_sourced_list  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 @
-    [map (fun x -> x) extra_args] in
-  List.flatten args
-;;
-
-let filter_cmdline l = CList.map_filter
-    (function {thing; source=CmdLine} -> Some thing | {source=ProjectFile} -> None)
-    l
-;;
-
-let forget_source {thing} = thing
-
-(* vim:set ft=ocaml: *)
-- 
cgit v1.2.3