diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/coqProject_file.ml4 | 320 | ||||
| -rw-r--r-- | lib/coqProject_file.mli | 91 |
2 files changed, 196 insertions, 215 deletions
diff --git a/lib/coqProject_file.ml4 b/lib/coqProject_file.ml4 index d32273bc2..9327f173e 100644 --- a/lib/coqProject_file.ml4 +++ b/lib/coqProject_file.ml4 @@ -6,29 +6,77 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -type target = - | ML of string (* ML file : foo.ml -> (ML "foo.ml") *) - | MLI of string (* MLI file : foo.mli -> (MLI "foo.mli") *) - | ML4 of string (* ML4 file : foo.ml4 -> (ML4 "foo.ml4") *) - | MLLIB of string (* MLLIB file : foo.mllib -> (MLLIB "foo.mllib") *) - | MLPACK of string (* MLLIB file : foo.mlpack -> (MLLIB "foo.mlpack") *) - | V of string (* V file : foo.v -> (V "foo") *) - | Arg of string - | Special of string * string * bool * string - (* file, dependencies, is_phony, command *) - | Subdir of string - | Def of string * string (* X=foo -> Def ("X","foo") *) - | MLInclude of string (* -I physicalpath *) - | Include of string * string (* -Q physicalpath logicalpath *) - | RInclude of string * string (* -R physicalpath logicalpath *) - -type install = +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; + + extra_targets : extra_target list; + subdirs : 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; +} +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 - | UnspecInstall -exception Parsing_error +(* 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) @@ -36,7 +84,7 @@ let rec parse_string = parser and parse_string2 = parser | [< ''"' >] -> "" | [< 'c; s >] -> (String.make 1 c)^(parse_string2 s) - | [< >] -> raise Parsing_error + | [< >] -> raise (Parsing_error "unterminated string") and parse_skip_comment = parser | [< ''\n'; s >] -> s | [< 'c; s >] -> parse_skip_comment s @@ -48,165 +96,117 @@ and parse_args = parser | [< '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 rec process_cmd_line orig_dir ((project_file,makefile,install,opt) as opts) l = function - | [] -> opts, l - | ("-h"|"--help") :: _ -> - raise Parsing_error - | ("-no-opt"|"-byte") :: r -> - process_cmd_line orig_dir (project_file,makefile,install,false) l r - | ("-full"|"-opt") :: r -> - process_cmd_line orig_dir (project_file,makefile,install,true) l r - | "-impredicative-set" :: r -> - Feedback.msg_warning (Pp.str "Please now use \"-arg -impredicative-set\" instead of \"-impredicative-set\" alone to be more uniform."); - process_cmd_line orig_dir opts (Arg "-impredicative-set" :: l) r - | "-no-install" :: r -> - Feedback.msg_warning (Pp.(++) (Pp.str "Option -no-install is deprecated.") (Pp.(++) (Pp.spc ()) (Pp.str "Use \"-install none\" instead"))); - process_cmd_line orig_dir (project_file,makefile,NoInstall,opt) l r + close_in c; + res +;; + +let process_cmd_line orig_dir proj args = + 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 install <> UnspecInstall then Feedback.msg_warning (Pp.str "-install sets more than once."); - let install = - match d with - | "user" -> UserInstall - | "none" -> NoInstall - | "global" -> TraditionalInstall - | _ -> Feedback.msg_warning (Pp.(++) (Pp.str "invalid option '") (Pp.(++) (Pp.str d) (Pp.str "' passed to -install."))); - install - in - process_cmd_line orig_dir (project_file,makefile,install,opt) l r - | "-custom" :: com :: dependencies :: file :: r -> - Feedback.msg_warning (Pp.app - (Pp.str "Please now use \"-extra[-phony] result deps command\" instead of \"-custom command deps result\".") - (Pp.pr_arg Pp.str "It follows makefile target declaration order and has a clearer semantic.") - ); - process_cmd_line orig_dir opts (Special (file,dependencies,false,com) :: l) r - | "-extra" :: file :: dependencies :: com :: r -> - process_cmd_line orig_dir opts (Special (file,dependencies,false,com) :: l) r - | "-extra-phony" :: target :: dependencies :: com :: r -> - process_cmd_line orig_dir opts (Special (target,dependencies,true,com) :: l) 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 -> - process_cmd_line orig_dir opts ((Include (CUnix.correct_path d orig_dir, lp)) :: l) r + aux { proj with q_includes = proj.q_includes @ [mk_path d,lp] } r | "-I" :: d :: r -> - process_cmd_line orig_dir opts ((MLInclude (CUnix.correct_path d orig_dir)) :: l) r - | "-R" :: p :: lp :: r -> - process_cmd_line orig_dir opts (RInclude (CUnix.correct_path p orig_dir,lp) :: l) r - | ("-Q"|"-R"|"-I"|"-custom"|"-extra"|"-extra-phony") :: _ -> - raise Parsing_error + 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 project_file with + let () = match proj.project_file with | None -> () | Some _ -> Feedback.msg_warning (Pp.str - "Several features will not work with multiple project files.") + "Multiple project files are deprecated.") in - let (opts',l') = process_cmd_line (Filename.dirname file) (Some file,makefile,install,opt) l (parse file) in - process_cmd_line orig_dir opts' l' r - | ["-f"] -> - raise Parsing_error + let proj = aux { proj with project_file = Some file } (parse file) in + aux proj r + | "-o" :: file :: r -> - begin try - let _ = String.index file '/' in - raise Parsing_error - with Not_found -> - let () = match makefile with - |None -> () - |Some f -> - Feedback.msg_warning (Pp.(++) (Pp.str "Only one output file is genererated. ") (Pp.(++) (Pp.str f) (Pp.str " will not be."))) - in process_cmd_line orig_dir (project_file,Some file,install,opt) l r - end + 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 -> - process_cmd_line orig_dir opts (Def (v,def) :: l) r + aux { proj with defs = proj.defs @ [v,def] } r | "-arg" :: a :: r -> - process_cmd_line orig_dir opts (Arg a :: l) r + aux { proj with extra_args = proj.extra_args @ [a] } r | f :: r -> let f = CUnix.correct_path f orig_dir in - process_cmd_line orig_dir opts (( - if Filename.check_suffix f ".v" then V f - else if (Filename.check_suffix f ".ml") then ML f - else if (Filename.check_suffix f ".ml4") then ML4 f - else if (Filename.check_suffix f ".mli") then MLI f - else if (Filename.check_suffix f ".mllib") then MLLIB f - else if (Filename.check_suffix f ".mlpack") then MLPACK f - else Subdir f) :: l) r - -let process_cmd_line orig_dir opts l args = - let (opts, l) = process_cmd_line orig_dir opts l args in - opts, List.rev l + 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 -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 + (******************************* API ************************************) -(* Return: ((v,(mli,ml4,ml,mllib,mlpack),special,subdir),(ml_inc,q_inc,r_inc),(args,defs)) *) -let split_arguments args = - List.fold_right - (fun a ((v,(mli,ml4,ml,mllib,mlpack as m),o,s as t), - (ml_inc,q_inc,r_inc as i),(args,defs as d)) -> - match a with - | V n -> - ((CUnix.remove_path_dot n::v,m,o,s),i,d) - | ML n -> - ((v,(mli,ml4,CUnix.remove_path_dot n::ml,mllib,mlpack),o,s),i,d) - | MLI n -> - ((v,(CUnix.remove_path_dot n::mli,ml4,ml,mllib,mlpack),o,s),i,d) - | ML4 n -> - ((v,(mli,CUnix.remove_path_dot n::ml4,ml,mllib,mlpack),o,s),i,d) - | MLLIB n -> - ((v,(mli,ml4,ml,CUnix.remove_path_dot n::mllib,mlpack),o,s),i,d) - | MLPACK n -> - ((v,(mli,ml4,ml,mllib,CUnix.remove_path_dot n::mlpack),o,s),i,d) - | Special (n,dep,is_phony,c) -> - ((v,m,(n,dep,is_phony,c)::o,s),i,d) - | Subdir n -> - ((v,m,o,n::s),i,d) - | MLInclude p -> - let ml_new = (CUnix.remove_path_dot (post_canonize p), - CUnix.canonical_path_name p) in - (t,(ml_new::ml_inc,q_inc,r_inc),d) - | Include (p,l) -> - let q_new = (CUnix.remove_path_dot (post_canonize p),l, - CUnix.canonical_path_name p) in - (t,(ml_inc,q_new::q_inc,r_inc),d) - | RInclude (p,l) -> - let r_new = (CUnix.remove_path_dot (post_canonize p),l, - CUnix.canonical_path_name p) in - (t,(ml_inc,q_inc,r_new::r_inc),d) - | Def (v,def) -> - (t,i,(args,(v,def)::defs)) - | Arg a -> - (t,i,(a::args,defs))) - args (([],([],[],[],[],[]),[],[]),([],[],[]),([],[])) +let cmdline_args_to_project ~curdir args = + process_cmd_line curdir (mk_project None None None true) args let read_project_file f = - split_arguments - (snd (process_cmd_line (Filename.dirname f) (Some f, None, NoInstall, true) [] (parse f))) - -let args_from_project file project_files default_name = - let build_cmd_line ml_inc i_inc r_inc args = - List.fold_right (fun (_,i) o -> "-I" :: i :: o) ml_inc - (List.fold_right (fun (_,l,i) o -> "-Q" :: i :: l :: o) i_inc - (List.fold_right (fun (_,l,p) o -> "-R" :: p :: l :: o) r_inc - (List.fold_right (fun a o -> parse_args (Stream.of_string a) @ o) args []))) - in try - let (fname,(_,(ml_inc,i_inc,r_inc),(args,_))) = List.hd project_files in - fname, build_cmd_line ml_inc i_inc r_inc args - with Failure _ -> - let rec find_project_file dir = try - let fname = Filename.concat dir default_name in - let ((v_files,_,_,_),(ml_inc,i_inc,r_inc),(args,_)) = - read_project_file fname in - fname, build_cmd_line ml_inc i_inc r_inc args - with Sys_error s -> - let newdir = Filename.dirname dir in - if dir = newdir then "",[] else find_project_file newdir - in find_project_file (Filename.dirname file) + 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 index 36513dbde..2bcf658fc 100644 --- a/lib/coqProject_file.mli +++ b/lib/coqProject_file.mli @@ -6,63 +6,44 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -type target = - | ML of string (* ML file : foo.ml -> (ML "foo.ml") *) - | MLI of string (* MLI file : foo.mli -> (MLI "foo.mli") *) - | ML4 of string (* ML4 file : foo.ml4 -> (ML4 "foo.ml4") *) - | MLLIB of string (* MLLIB file : foo.mllib -> (MLLIB "foo.mllib") *) - | MLPACK of string (* MLLIB file : foo.mlpack -> (MLLIB "foo.mlpack") *) - | V of string (* V file : foo.v -> (V "foo") *) - | Arg of string - | Special of string * string * bool * string - (* file, dependencies, is_phony, command *) - | Subdir of string - | Def of string * string (* X=foo -> Def ("X","foo") *) - | MLInclude of string (* -I physicalpath *) - | Include of string * string (* -Q physicalpath logicalpath *) - | RInclude of string * string (* -R physicalpath logicalpath *) - -type install = +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; + + extra_targets : extra_target list; + subdirs : 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; +} +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 - | UnspecInstall - -exception Parsing_error - -val args_from_project : - string -> - (string * - ('a * - (('b * string) list * ('c * string * string) list * - ('d * string * string) list) * - (string list * 'e))) - list -> string -> string * string list - -val read_project_file : - string -> - (string list * - (string list * string list * string list * string list * - string list) * - (string * string * bool * string) list * string list) * - ((string * string) list * (string * string * string) list * - (string * string * string) list) * - (string list * (string * string) list) - -val process_cmd_line : - string -> - string option * string option * install * bool -> - target list -> - string list -> - (string option * string option * install * bool) * target list -val split_arguments : - target list -> - (string list * - (string list * string list * string list * string list * - string list) * - (string * string * bool * string) list * string list) * - ((string * string) list * (string * string * string) list * - (string * string * string) list) * - (string list * (string * string) list) +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 |