diff options
| -rw-r--r-- | Makefile.build | 2 | ||||
| -rw-r--r-- | ide/ide.mllib | 1 | ||||
| -rw-r--r-- | ide/minilib.ml | 28 | ||||
| -rw-r--r-- | ide/minilib.mli | 3 | ||||
| -rw-r--r-- | ide/project_file.ml4 | 121 | ||||
| -rw-r--r-- | tools/coq_makefile.ml (renamed from tools/coq_makefile.ml4) | 129 |
6 files changed, 157 insertions, 127 deletions
diff --git a/Makefile.build b/Makefile.build index 91d73ae25..efebb57df 100644 --- a/Makefile.build +++ b/Makefile.build @@ -492,7 +492,7 @@ $(GALLINA): $(addsuffix $(BESTOBJ), tools/gallina_lexer tools/gallina) $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml,,) -$(COQMAKEFILE): $(addsuffix $(BESTOBJ), config/coq_config tools/coq_makefile) +$(COQMAKEFILE): $(addsuffix $(BESTOBJ),config/coq_config ide/minilib ide/project_file tools/coq_makefile) $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml,,str) diff --git a/ide/ide.mllib b/ide/ide.mllib index 8d3260510..8f3a6c353 100644 --- a/ide/ide.mllib +++ b/ide/ide.mllib @@ -22,4 +22,5 @@ Coq Coq_commands Command_windows Coqide_ui +Project_file Coqide diff --git a/ide/minilib.ml b/ide/minilib.ml index dcadc81f5..71956cf8f 100644 --- a/ide/minilib.ml +++ b/ide/minilib.ml @@ -74,3 +74,31 @@ let home = let coqlib = ref "" let coqtop_path = ref "" + +(* Hints to partially detects if two paths refer to the same repertory *) +let rec remove_path_dot p = + let curdir = Filename.concat Filename.current_dir_name "" in (* Unix: "./" *) + let n = String.length curdir in + if String.length p > n && String.sub p 0 n = curdir then + remove_path_dot (String.sub p n (String.length p - n)) + else + p + +let strip_path p = + let cwd = Filename.concat (Sys.getcwd ()) "" in (* Unix: "`pwd`/" *) + let n = String.length cwd in + if String.length p > n && String.sub p 0 n = cwd then + remove_path_dot (String.sub p n (String.length p - n)) + else + remove_path_dot p + +let canonical_path_name p = + let current = Sys.getcwd () in + try + Sys.chdir p; + let p' = Sys.getcwd () in + Sys.chdir current; + p' + with Sys_error _ -> + (* We give up to find a canonical name and just simplify it... *) + strip_path p diff --git a/ide/minilib.mli b/ide/minilib.mli index 1daa60e1a..2128b7d86 100644 --- a/ide/minilib.mli +++ b/ide/minilib.mli @@ -25,3 +25,6 @@ val home : string val coqlib : string ref val coqtop_path : string ref + +val strip_path : string -> string +val canonical_path_name : string -> string diff --git a/ide/project_file.ml4 b/ide/project_file.ml4 new file mode 100644 index 000000000..ef39b904c --- /dev/null +++ b/ide/project_file.ml4 @@ -0,0 +1,121 @@ +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") *) + | V of string (* V file : foo.v -> (V "foo") *) + | Arg of string + | Special of string * string * string (* file, dependencies, command *) + | Subdir of string + | Def of string * string (* X=foo -> Def ("X","foo") *) + | Include of string + | RInclude of string * string (* -R physicalpath logicalpath *) + + +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) +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 ((project_file,makefile,install,opt) as opts) l = function + | [] -> opts,List.rev l + | ("-h"|"--help") :: _ -> + raise Parsing_error + | ("-no-opt"|"-byte") :: r -> + process_cmd_line (project_file,makefile,install,false) l r + | ("-full"|"-opt") :: r -> + process_cmd_line (project_file,makefile,install,true) l r + | "-impredicative-set" :: r -> + prerr_string "Please now use \"-arg -impredicative-set\" instead of \"-impredicative-set\" alone to be more uniform.\n"; + process_cmd_line opts (Arg "-impredicative_set" :: l) r + | "-no-install" :: r -> + if not install then prerr_string "Warning: -no-install sets more than once.\n"; + process_cmd_line (project_file,makefile,false,opt) l r + | "-custom" :: com :: dependencies :: file :: r -> + process_cmd_line opts (Special (file,dependencies,com) :: l) r + | "-I" :: d :: r -> + process_cmd_line opts (Include d :: l) r + | "-R" :: p :: lp :: r -> + process_cmd_line opts (RInclude (p,lp) :: l) r + | ("-I"|"-custom") :: _ -> + raise Parsing_error + | "-f" :: file :: r -> + let () = match project_file with + | None -> () + | Some _ -> prerr_string + "Warning: Several features will not work with multiple project files.\n" + in process_cmd_line (Some file,makefile,install,opt) l ((parse file)@r) + | ["-f"] -> + raise Parsing_error + | "-o" :: file :: r -> + let () = match makefile with + |None -> () + |Some f -> + prerr_string "Warning: Only one output file in genererated. "; + prerr_string f; prerr_string " will not.\n" + in process_cmd_line (project_file,Some file,install,opt) l r + | v :: "=" :: def :: r -> + process_cmd_line opts (Def (v,def) :: l) r + | "-arg" :: a :: r -> + process_cmd_line opts (Arg a :: l) r + | f :: r -> + process_cmd_line 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 Subdir f) :: l) r + +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),special,subdir),(i_inc,r_inc),(args,defs)) *) +let rec split_arguments = function + | V n :: r -> + let (v,m,o,s),i,d = split_arguments r in ((Minilib.strip_path n::v,m,o,s),i,d) + | ML n :: r -> + let (v,(mli,ml4,ml,mllib),o,s),i,d = split_arguments r in ((v,(mli,ml4,Minilib.strip_path n::ml,mllib),o,s),i,d) + | MLI n :: r -> + let (v,(mli,ml4,ml,mllib),o,s),i,d = split_arguments r in ((v,(Minilib.strip_path n::mli,ml4,ml,mllib),o,s),i,d) + | ML4 n :: r -> + let (v,(mli,ml4,ml,mllib),o,s),i,d = split_arguments r in ((v,(mli,Minilib.strip_path n::ml4,ml,mllib),o,s),i,d) + | MLLIB n :: r -> + let (v,(mli,ml4,ml,mllib),o,s),i,d = split_arguments r in ((v,(mli,ml4,ml,Minilib.strip_path n::mllib),o,s),i,d) + | Special (n,dep,c) :: r -> + let (v,m,o,s),i,d = split_arguments r in ((v,m,(n,dep,c)::o,s),i,d) + | Subdir n :: r -> + let (v,m,o,s),i,d = split_arguments r in ((v,m,o,n::s),i,d) + | Include p :: r -> + let t,(i,r),d = split_arguments r in (t,((post_canonize p,Minilib.canonical_path_name p)::i,r),d) + | RInclude (p,l) :: r -> + let t,(i,r),d = split_arguments r in (t,(i,(post_canonize p,l,Minilib.canonical_path_name p)::r),d) + | Def (v,def) :: r -> + let t,i,(args,defs) = split_arguments r in (t,i,(args,(v,def)::defs)) + | Arg a :: r -> + let t,i,(args,defs) = split_arguments r in (t,i,(a::args,defs)) + | [] -> ([],([],[],[],[]),[],[]),([],[]),([],[]) diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml index edbe22e73..ca31a2bd0 100644 --- a/tools/coq_makefile.ml4 +++ b/tools/coq_makefile.ml @@ -8,19 +8,6 @@ (* créer un Makefile pour un développement Coq automatiquement *) -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") *) - | V of string (* V file : foo.v -> (V "foo") *) - | Arg of string - | Special of string * string * string (* file, dependencies, command *) - | Subdir of string - | Def of string * string (* X=foo -> Def ("X","foo") *) - | Include of string - | RInclude of string * string (* -R physicalpath logicalpath *) - let output_channel = ref stdout let makefile_name = ref "Makefile" let make_name = ref "" @@ -107,17 +94,6 @@ let is_prefix dir1 dir2 = let l2 = String.length dir2 in dir1 = dir2 or (l1 < l2 & String.sub dir2 0 l1 = dir1 & dir2.[l1] = '/') -let pre_canonize f = - let l = String.length f in - if l > 2 && f.[0] = '.' && f.[1] = '/' then - let n = let i = ref 2 in while !i < l && f.[!i] = '/' do incr i done; !i in - String.sub f n (l-n) - else f - -let post_canonize f = - let n = 1 + let i = ref (String.length f - 1) in while !i >= 0 && f.[!i] = '/' do decr i done; !i in - String.sub f 0 n - let physical_dir_of_logical_dir ldir = let le = String.length ldir - 1 in let pdir = if ldir.[le] = '.' then String.sub ldir 0 (le - 1) else String.copy ldir in @@ -407,32 +383,6 @@ let subdirs sds = :: "depend" :: "html" :: sds); print "\n\n" -(* Return: ((v,(mli,ml4,ml,mllib),special,subdir),(i_inc,r_inc),(args,defs)) *) -let rec split_arguments = function - | V n :: r -> - let (v,m,o,s),i,d = split_arguments r in ((pre_canonize n::v,m,o,s),i,d) - | ML n :: r -> - let (v,(mli,ml4,ml,mllib),o,s),i,d = split_arguments r in ((v,(mli,ml4,pre_canonize n::ml,mllib),o,s),i,d) - | MLI n :: r -> - let (v,(mli,ml4,ml,mllib),o,s),i,d = split_arguments r in ((v,(pre_canonize n::mli,ml4,ml,mllib),o,s),i,d) - | ML4 n :: r -> - let (v,(mli,ml4,ml,mllib),o,s),i,d = split_arguments r in ((v,(mli,pre_canonize n::ml4,ml,mllib),o,s),i,d) - | MLLIB n :: r -> - let (v,(mli,ml4,ml,mllib),o,s),i,d = split_arguments r in ((v,(mli,ml4,ml,pre_canonize n::mllib),o,s),i,d) - | Special (n,dep,c) :: r -> - let (v,m,o,s),i,d = split_arguments r in ((v,m,(n,dep,c)::o,s),i,d) - | Subdir n :: r -> - let (v,m,o,s),i,d = split_arguments r in ((v,m,o,n::s),i,d) - | Include p :: r -> - let t,(i,r),d = split_arguments r in (t,((post_canonize p,absolute_dir p)::i,r),d) - | RInclude (p,l) :: r -> - let t,(i,r),d = split_arguments r in (t,(i,(post_canonize p,l,absolute_dir p)::r),d) - | Def (v,def) :: r -> - let t,i,(args,defs) = split_arguments r in (t,i,(args,(v,def)::defs)) - | Arg a :: r -> - let t,i,(args,defs) = split_arguments r in (t,i,(a::args,defs)) - | [] -> ([],([],[],[],[]),[],[]),([],[]),([],[]) - let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles) other_targets inc = begin match vfiles with |[] -> () @@ -547,80 +497,6 @@ let all_target (vfiles, mlfiles, sps, sds) inc = custom sps; subdirs sds -let parse f = - let rec string = parser - | [< '' ' | '\n' | '\t' >] -> "" - | [< 'c; s >] -> (String.make 1 c)^(string s) - | [< >] -> "" - and string2 = parser - | [< ''"' >] -> "" - | [< 'c; s >] -> (String.make 1 c)^(string2 s) - and skip_comment = parser - | [< ''\n'; s >] -> s - | [< 'c; s >] -> skip_comment s - | [< >] -> [< >] - and args = parser - | [< '' ' | '\n' | '\t'; s >] -> args s - | [< ''#'; s >] -> args (skip_comment s) - | [< ''"'; str = string2; s >] -> ("" ^ str) :: args s - | [< 'c; str = string; s >] -> ((String.make 1 c) ^ str) :: (args s) - | [< >] -> [] - in - let c = open_in f in - let res = args (Stream.of_channel c) in - close_in c; - res - -let rec process_cmd_line ((project_file,makefile,install,opt) as opts) l = function - | [] -> opts,List.rev l - | ("-h"|"--help") :: _ -> - usage () - | ("-no-opt"|"-byte") :: r -> - process_cmd_line (project_file,makefile,install,false) l r - | ("-full"|"-opt") :: r -> - process_cmd_line (project_file,makefile,install,true) l r - | "-impredicative-set" :: r -> - prerr_string "Please now use \"-arg -impredicative-set\" instead of \"-impredicative-set\" alone to be more uniform.\n"; - process_cmd_line opts (Arg "-impredicative_set" :: l) r - | "-no-install" :: r -> - if not install then prerr_string "Warning: -no-install sets more than once.\n"; - process_cmd_line (project_file,makefile,false,opt) l r - | "-custom" :: com :: dependencies :: file :: r -> - process_cmd_line opts (Special (file,dependencies,com) :: l) r - | "-I" :: d :: r -> - process_cmd_line opts (Include d :: l) r - | "-R" :: p :: lp :: r -> - process_cmd_line opts (RInclude (p,lp) :: l) r - | ("-I"|"-custom") :: _ -> - usage () - | "-f" :: file :: r -> - let () = match project_file with - | None -> () - | Some _ -> prerr_string - "Warning: Several features will not work with multiple project files.\n" - in process_cmd_line (Some file,makefile,install,opt) l ((parse file)@r) - | ["-f"] -> - usage () - | "-o" :: file :: r -> - let () = match makefile with - |None -> () - |Some f -> - prerr_string "Warning: Only one output file in genererated. "; - prerr_string f; prerr_string " will not.\n" - in process_cmd_line (project_file,Some file,install,opt) l r - | v :: "=" :: def :: r -> - process_cmd_line opts (Def (v,def) :: l) r - | "-arg" :: a :: r -> - process_cmd_line opts (Arg a :: l) r - | f :: r -> - process_cmd_line 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 Subdir f) :: l) r - let banner () = print (Printf.sprintf "############################################################################# @@ -682,9 +558,10 @@ let do_makefile args = |[] -> var := false |_::_ -> var := true in let (project_file,makefile,is_install,opt),l = - process_cmd_line (None,None,true,true) [] args in + try Project_file.process_cmd_line (None,None,true,true) [] args + with Project_file.Parsing_error -> usage () in let (v_f,(mli_f,ml4_f,ml_f,mllib_f),sps,sds as targets), inc, defs = - split_arguments l in + Project_file.split_arguments l in let () = match project_file with |None -> () |Some f -> make_name := f in let () = match makefile with |