From 79bb444169f0ac919cf9672fb371ee42d98ead2e Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 3 Jan 2017 10:53:59 +0100 Subject: ide/project_file.ml4 -> lib/coqProject_file.ml4 + .mli The .mli only acknowledges the current API. I'm not guilty your honor! --- .gitignore | 2 +- Makefile.build | 2 +- ide/coqide.ml | 4 +- ide/ide.mllib | 2 + ide/project_file.ml4 | 212 ------------------------------------------------ lib/clib.mllib | 1 + lib/coqProject_file.ml4 | 212 ++++++++++++++++++++++++++++++++++++++++++++++++ lib/coqProject_file.mli | 68 ++++++++++++++++ tools/coq_makefile.ml | 22 ++--- 9 files changed, 298 insertions(+), 227 deletions(-) delete mode 100644 ide/project_file.ml4 create mode 100644 lib/coqProject_file.ml4 create mode 100644 lib/coqProject_file.mli diff --git a/.gitignore b/.gitignore index 8bbfce5d8..6e6f01a43 100644 --- a/.gitignore +++ b/.gitignore @@ -128,7 +128,7 @@ ide/xml_lexer.ml g_*.ml -ide/project_file.ml +lib/coqProject_file.ml parsing/cLexer.ml plugins/ltac/coretactics.ml plugins/ltac/extratactics.ml diff --git a/Makefile.build b/Makefile.build index 56f1fb8b4..8aedd9cec 100644 --- a/Makefile.build +++ b/Makefile.build @@ -377,7 +377,7 @@ $(GALLINA): $(call bestobj, tools/gallina_lexer.cmo tools/gallina.cmo) $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml,,) -COQMAKEFILECMO:=lib/clib.cma ide/project_file.cmo tools/coq_makefile.cmo +COQMAKEFILECMO:=lib/clib.cma tools/coq_makefile.cmo $(COQMAKEFILE): $(call bestobj,$(COQMAKEFILECMO)) $(SHOW)'OCAMLBEST -o $@' diff --git a/ide/coqide.ml b/ide/coqide.ml index 0b7567a5a..e47db8d19 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -84,7 +84,7 @@ let pr_exit_status = function let make_coqtop_args = function |None -> "", !sup_args |Some the_file -> - let get_args f = Project_file.args_from_project f + let get_args f = CoqProject_file.args_from_project f !custom_project_files project_file_name#get in match read_project#get with @@ -1346,7 +1346,7 @@ let read_coqide_args argv = else (output_string stderr "Error: multiple -coqtop options"; exit 1) |"-f" :: file :: args -> let d = CUnix.canonical_path_name (Filename.dirname file) in - let p = Project_file.read_project_file file in + let p = CoqProject_file.read_project_file file in filter_coqtop coqtop ((d,p) :: project_files) out args |"-f" :: [] -> output_string stderr "Error: missing project file name"; exit 1 diff --git a/ide/ide.mllib b/ide/ide.mllib index 78b4c01e8..57e9fe5ad 100644 --- a/ide/ide.mllib +++ b/ide/ide.mllib @@ -9,6 +9,8 @@ Config_lexer Utf8_convert Preferences Project_file +Serialize +Richprinter Xml_lexer Xml_parser Xml_printer diff --git a/ide/project_file.ml4 b/ide/project_file.ml4 deleted file mode 100644 index d32273bc2..000000000 --- a/ide/project_file.ml4 +++ /dev/null @@ -1,212 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* (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 = - | NoInstall - | TraditionalInstall - | UserInstall - | UnspecInstall - -exception Parsing_error -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 -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 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 - | "-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 - | "-Q" :: d :: lp :: r -> - process_cmd_line orig_dir opts ((Include (CUnix.correct_path d orig_dir, lp)) :: l) 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 - | "-f" :: file :: r -> - let file = CUnix.remove_path_dot (CUnix.correct_path file orig_dir) in - let () = match project_file with - | None -> () - | Some _ -> Feedback.msg_warning (Pp.str - "Several features will not work with multiple project files.") - 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 - | "-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 - | v :: "=" :: def :: r -> - process_cmd_line orig_dir opts (Def (v,def) :: l) r - | "-arg" :: a :: r -> - process_cmd_line orig_dir opts (Arg a :: l) 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 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 - -(* 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 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) - -(* vim:set ft=ocaml: *) diff --git a/lib/clib.mllib b/lib/clib.mllib index c73ae9b90..71f728291 100644 --- a/lib/clib.mllib +++ b/lib/clib.mllib @@ -32,3 +32,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..d32273bc2 --- /dev/null +++ b/lib/coqProject_file.ml4 @@ -0,0 +1,212 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* (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 = + | NoInstall + | TraditionalInstall + | UserInstall + | UnspecInstall + +exception Parsing_error +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 +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 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 + | "-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 + | "-Q" :: d :: lp :: r -> + process_cmd_line orig_dir opts ((Include (CUnix.correct_path d orig_dir, lp)) :: l) 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 + | "-f" :: file :: r -> + let file = CUnix.remove_path_dot (CUnix.correct_path file orig_dir) in + let () = match project_file with + | None -> () + | Some _ -> Feedback.msg_warning (Pp.str + "Several features will not work with multiple project files.") + 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 + | "-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 + | v :: "=" :: def :: r -> + process_cmd_line orig_dir opts (Def (v,def) :: l) r + | "-arg" :: a :: r -> + process_cmd_line orig_dir opts (Arg a :: l) 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 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 + +(* 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 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) + +(* vim:set ft=ocaml: *) diff --git a/lib/coqProject_file.mli b/lib/coqProject_file.mli new file mode 100644 index 000000000..36513dbde --- /dev/null +++ b/lib/coqProject_file.mli @@ -0,0 +1,68 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* (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 = + | 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) + diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 4875cb62b..d72916232 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -282,7 +282,7 @@ let where_put_doc = function "$(INSTALLDEFAULTROOT)" let install (vfiles,(mlis,ml4s,mls,mllibs,mlpacks),_,sds) inc = function - |Project_file.NoInstall -> () + |CoqProject_file.NoInstall -> () |is_install -> let not_empty = function |[] -> false |_::_ -> true in let cmos = List.rev_append mlpacks (List.rev_append mls ml4s) in @@ -295,7 +295,7 @@ let install (vfiles,(mlis,ml4s,mls,mllibs,mlpacks),_,sds) inc = function ("CMOFILES",cmos);("CMIFILES",cmis);("CMAFILES",mllibs)] inc in let doc_dir = where_put_doc inc in - if is_install = Project_file.UnspecInstall then begin + if is_install = CoqProject_file.UnspecInstall then begin print "userinstall:\n\t+$(MAKE) USERINSTALL=true install\n\n" end; if not_empty cmxss then begin @@ -533,8 +533,8 @@ let variables is_install opt (args,defs) = \n $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl'\n\n"; end; match is_install with - | Project_file.NoInstall -> () - | Project_file.UnspecInstall -> + | CoqProject_file.NoInstall -> () + | CoqProject_file.UnspecInstall -> section "Install Paths."; print "ifdef USERINSTALL\n"; print "XDG_DATA_HOME?=\"$(HOME)/.local/share\"\n"; @@ -545,13 +545,13 @@ let variables is_install opt (args,defs) = print "COQDOCINSTALL=\"${DOCDIR}user-contrib\"\n"; print "COQTOPINSTALL=\"${COQLIB}toploop\"\n"; print "endif\n\n" - | Project_file.TraditionalInstall -> + | CoqProject_file.TraditionalInstall -> section "Install Paths."; print "COQLIBINSTALL=\"${COQLIB}user-contrib\"\n"; print "COQDOCINSTALL=\"${DOCDIR}user-contrib\"\n"; print "COQTOPINSTALL=\"${COQLIB}toploop\"\n"; print "\n" - | Project_file.UserInstall -> + | CoqProject_file.UserInstall -> section "Install Paths."; print "XDG_DATA_HOME?=\"$(HOME)/.local/share\"\n"; print "COQLIBINSTALL=$(XDG_DATA_HOME)/coq\n"; @@ -895,11 +895,11 @@ let do_makefile args = |_::_ -> var := true in let (project_file,makefile,is_install,opt),l = try - Project_file.process_cmd_line Filename.current_dir_name - (None,None,Project_file.UnspecInstall,true) [] args - with Project_file.Parsing_error -> usage () in + CoqProject_file.process_cmd_line Filename.current_dir_name + (None,None,CoqProject_file.UnspecInstall,true) [] args + with CoqProject_file.Parsing_error -> usage () in let (v_f,(mli_f,ml4_f,ml_f,mllib_f,mlpack_f),sps,sds as targets), inc, defs = - Project_file.split_arguments l in + CoqProject_file.split_arguments l in let () = match project_file with |None -> () |Some f -> make_name := f in let () = match makefile with @@ -920,7 +920,7 @@ let do_makefile args = List.iter check_dep (Str.split (Str.regexp "[ \t]+") dependencies)) sps; let inc = ensure_root_dir targets inc in - if is_install <> Project_file.NoInstall then begin + if is_install <> CoqProject_file.NoInstall then begin warn_install_at_root_directory targets inc; end; check_overlapping_include inc; -- cgit v1.2.3