From dffb6159812757ba59e02419b451e6135d1e3502 Mon Sep 17 00:00:00 2001 From: letouzey Date: Fri, 20 Mar 2009 20:50:44 +0000 Subject: Many changes in the Makefile infrastructure + a beginning of ocamlbuild * generalize the use of .mllib to build all cma, not only in plugins/ * the .mllib in plugins/ now mention Bruno's new _mod.ml files * lots of .cmo enumerations in Makefile.common are removed, since they are now in .mllib * the list of .cmo/.cmi can be retreive via a shell script line, see for instance rule install-library * Tolink.core_objs and Tolink.ide now contains ocaml _modules_, not _files_ * a -I option to coqdep_boot allows to control piority of includes (some files with the same names in kernel and checker ...) This is quite a lot of changes, you know who to blame / report to if something breaks. ... and last but not least I've started playing with ocamlbuild. The myocamlbuild.ml is far from complete now, but it already allows to build coqtop.{opt,byte} here. See comments at the top of myocamlbuild.ml, and don't hesitate to contribute, either for completing or simplifying it ! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12002 85f007b7-540e-0410-9357-904b9bb8a0f7 --- tools/coqdep_boot.ml | 19 ++++++++++++------- tools/coqdep_common.ml | 35 +++++++++++++++++++++++------------ tools/coqdep_lexer.mll | 29 +++++++++++++---------------- 3 files changed, 48 insertions(+), 35 deletions(-) (limited to 'tools') diff --git a/tools/coqdep_boot.ml b/tools/coqdep_boot.ml index 59fe701aa..d259c3be5 100644 --- a/tools/coqdep_boot.ml +++ b/tools/coqdep_boot.ml @@ -22,19 +22,24 @@ let rec parse = function | "-natdynlink" :: "no" :: ll -> option_natdynlk := false; parse ll | "-c" :: ll -> option_c := true; parse ll | "-boot" :: ll -> parse ll (* We're already in boot mode by default *) + | "-I" :: r :: ll -> + (* To solve conflict (e.g. same filename in kernel and checker) + we allow to state an explicit order *) + add_dir add_known r []; + norecdir_list:=r::!norecdir_list; + parse ll | f :: ll -> treat_file None f; parse ll | [] -> () let coqdep_boot () = if Array.length Sys.argv < 2 then exit 1; parse (List.tl (Array.to_list Sys.argv)); - add_rec_dir add_known "theories" ["Coq"]; - add_rec_dir add_known "plugins" ["Coq"]; - List.iter (fun (f,d) -> add_mli_known f d) !mliAccu; - List.iter (fun (f,d) -> add_mllib_known f d) !mllibAccu; - List.iter (fun (f,_,d) -> add_ml_known f d) !mlAccu; - warning_mult ".mli" iter_mli_known; - warning_mult ".ml" iter_ml_known; + if !option_c then + add_rec_dir add_known "." [] + else begin + add_rec_dir add_known "theories" ["Coq"]; + add_rec_dir add_known "plugins" ["Coq"]; + end; if !option_c then mL_dependencies (); coq_dependencies () diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index 67a200921..7ac57a4f5 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -27,6 +27,8 @@ let option_noglob = ref false let option_slash = ref false let option_natdynlk = ref true +let norecdir_list = ref ([]:string list) + let suffixe = ref ".vo" type dir = string option @@ -98,7 +100,7 @@ let safe_hash_add clq q (k,v) = let mkknown () = let h = (Hashtbl.create 19 : (string, dir) Hashtbl.t) in - let add x s = Hashtbl.add h x s + let add x s = if Hashtbl.mem h x then () else Hashtbl.add h x s and iter f = Hashtbl.iter f h and search x = try Some (Hashtbl.find h (String.uncapitalize x)) @@ -302,27 +304,32 @@ let mL_dependencies () = (fun (name,ext,dirname) -> let fullname = file_name name dirname in let (dep,dep_opt) = traite_fichier_ML fullname ext in - let intf = - if List.mem (name,dirname) !mliAccu then " "^fullname^".cmi" else "" + let intf = match search_mli_known name with + | None -> "" + | Some mldir -> " "^(file_name name mldir)^".cmi" in - printf "%s.cmo: %s%s%s%s\n" fullname fullname ext intf dep; - printf "%s.cmx: %s%s%s%s\n" fullname fullname ext intf dep_opt; - flush stdout) + if dep<>"" || intf<>"" then begin + printf "%s.cmo:%s%s\n" fullname dep intf; + printf "%s.cmx:%s%s\n" fullname dep_opt intf; + flush stdout; + end) (List.rev !mlAccu); List.iter (fun (name,dirname) -> let fullname = file_name name dirname in let (dep,_) = traite_fichier_ML fullname ".mli" in - printf "%s.cmi: %s.mli%s\n" fullname fullname dep; + if dep<>"" then printf "%s.cmi:%s\n" fullname dep; flush stdout) (List.rev !mliAccu); List.iter (fun (name,dirname) -> let fullname = file_name name dirname in let (dep,dep_opt) = traite_fichier_mllib fullname ".mllib" in - printf "%s.cma:%s\n" fullname dep; - printf "%s.cmxa %s.cmxs:%s\n" fullname fullname dep_opt; - flush stdout) + if dep<>"" then begin + printf "%s.cma:%s\n" fullname dep; + printf "%s.cmxa %s.cmxs:%s\n" fullname fullname dep_opt; + flush stdout + end) (List.rev !mllibAccu) let coq_dependencies () = @@ -382,9 +389,13 @@ let rec add_directory recur add_file phys_dir log_dir = let f = readdir dirh in (* we avoid . .. and all hidden files and subdirs (e.g. .svn, _darcs) *) if f.[0] <> '.' && f.[0] <> '_' then - let phys_f = phys_dir//f in + let phys_f = if phys_dir = "." then f else phys_dir//f in match try (stat phys_f).st_kind with _ -> S_BLK with - | S_DIR when recur -> add_directory recur add_file phys_f (log_dir@[f]) + | S_DIR when recur -> + if List.mem phys_f !norecdir_list then () + else + let log_dir' = if log_dir = [] then ["Coq"] else log_dir@[f] in + add_directory recur add_file phys_f log_dir' | S_REG -> add_file phys_dir log_dir f | _ -> () done diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll index 6d6a804da..3c7d09e1f 100755 --- a/tools/coqdep_lexer.mll +++ b/tools/coqdep_lexer.mll @@ -34,15 +34,18 @@ let mllist = ref ([] : string list) let field_name s = String.sub s 1 (String.length s - 1) + } let space = [' ' '\t' '\n' '\r'] let lowercase = ['a'-'z' '\223'-'\246' '\248'-'\255'] let uppercase = ['A'-'Z' '\192'-'\214' '\216'-'\222'] -let identchar = +let identchar = ['A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255' '\'' '0'-'9'] let coq_ident = ['a'-'z' '_' '0'-'9' 'A'-'Z']+ let coq_field = '.'['a'-'z' '_' '0'-'9' 'A'-'Z']+ +let caml_up_ident = uppercase identchar* +let caml_low_ident = lowercase identchar* let dot = '.' ( space+ | eof) rule coq_action = parse @@ -66,13 +69,14 @@ rule coq_action = parse { coq_action lexbuf } and caml_action = parse - | [' ' '\010' '\013' '\009' '\012'] + - { caml_action lexbuf } - | "open" [' ' '\010' '\013' '\009' '\012']* - { caml_opened_file lexbuf } - | lowercase identchar* + | space + { caml_action lexbuf } - | uppercase identchar* + | "open" space* (caml_up_ident as id) + { Use_module (String.uncapitalize id) } + | "module" space+ caml_up_ident + { caml_action lexbuf } + | caml_low_ident { caml_action lexbuf } + | caml_up_ident { ml_module_name := Lexing.lexeme lexbuf; qual_id lexbuf } | ['0'-'9']+ @@ -213,18 +217,11 @@ and modules = parse | _ { (Declare (List.rev !mllist)) } and qual_id = parse - | '.' [^ '.' '(' '['] { Use_module (String.uncapitalize !ml_module_name) } + | '.' [^ '.' '(' '['] { + Use_module (String.uncapitalize !ml_module_name) } | eof { raise Fin_fichier } | _ { caml_action lexbuf } -and caml_opened_file = parse - | uppercase identchar* - { let lex = (Lexing.lexeme lexbuf) in - let str = String.sub lex 0 (String.length lex) in - (Use_module (String.uncapitalize str)) } - | eof {raise Fin_fichier } - | _ { caml_action lexbuf } - and mllib_list = parse | coq_ident { let s = String.uncapitalize (Lexing.lexeme lexbuf) in s :: mllib_list lexbuf } -- cgit v1.2.3