diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/CoqMakefile.in | 16 | ||||
| -rw-r--r-- | tools/coqdep_common.ml | 277 |
2 files changed, 176 insertions, 117 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 626ac0fe67..1cceed79a4 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -408,6 +408,12 @@ checkproofs: -schedule-vio-checking $(J) $(VOFILES:%.vo=%.vio) .PHONY: checkproofs +vos: $(VOFILES:%.vo=%.vos) +.PHONY: vos + +vok: $(VOFILES:%.vo=%.vok) +.PHONY: vok + validate: $(VOFILES) $(TIMER) $(COQCHK) $(COQCHKFLAGS) $(COQLIBS) $^ .PHONY: validate @@ -558,6 +564,8 @@ clean:: $(HIDE)find . -name .coq-native -type d -empty -delete $(HIDE)rm -f $(VOFILES) $(HIDE)rm -f $(VOFILES:.vo=.vio) + $(HIDE)rm -f $(VOFILES:.vo=.vos) + $(HIDE)rm -f $(VOFILES:.vo=.vok) $(HIDE)rm -f $(BEAUTYFILES) $(VFILES:=.old) $(HIDE)rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob all-mli.tex $(HIDE)rm -f $(VFILES:.v=.glob) @@ -666,6 +674,14 @@ $(VFILES:.v=.vio): %.vio: %.v $(SHOW)COQC -quick $< $(HIDE)$(TIMER) $(COQC) -quick $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< +$(VFILES:.v=.vos): %.vos: %.v + $(SHOW)COQC -vos $< + $(HIDE)$(TIMER) $(COQC) -vos $(COQDEBUG) $(COQFLAGS) $< + +$(VFILES:.v=.vok): %.vok: %.v + $(SHOW)COQC -vok $< + $(HIDE)$(TIMER) $(COQC) -vok $(COQDEBUG) $(COQFLAGS) $< + $(addsuffix .timing.diff,$(VFILES)): %.timing.diff : %.before-timing %.after-timing $(SHOW)PYTHON TIMING-DIFF $< $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" print-pretty-single-time-diff BEFORE=$*.before-timing AFTER=$*.after-timing TIME_OF_PRETTY_BUILD_FILE="$@" diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index 8beb314046..ddedec12f8 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -235,15 +235,15 @@ let file_name s = function let depend_ML str = match search_mli_known str, search_ml_known str with | Some mlidir, Some mldir -> - let mlifile = file_name str mlidir - and mlfile = file_name str mldir in - (" "^mlifile^".cmi"," "^mlfile^".cmx") + let mlifile = file_name str mlidir + and mlfile = file_name str mldir in + (" "^mlifile^".cmi"," "^mlfile^".cmx") | None, Some mldir -> - let mlfile = file_name str mldir in - (" "^mlfile^".cmo"," "^mlfile^".cmx") + let mlfile = file_name str mldir in + (" "^mlfile^".cmo"," "^mlfile^".cmx") | Some mlidir, None -> - let mlifile = file_name str mlidir in - (" "^mlifile^".cmi"," "^mlifile^".cmi") + let mlifile = file_name str mlidir in + (" "^mlifile^".cmi"," "^mlifile^".cmi") | None, None -> "", "" let soustraite_fichier_ML dep md ext = @@ -254,9 +254,9 @@ let soustraite_fichier_ML dep md ext = let a_faire_opt = ref "" in List.iter (fun str -> - let byte,opt = depend_ML str in - a_faire := !a_faire ^ byte; - a_faire_opt := !a_faire_opt ^ opt) + let byte,opt = depend_ML str in + a_faire := !a_faire ^ byte; + a_faire_opt := !a_faire_opt ^ opt) (List.rev list); (!a_faire, !a_faire_opt) with @@ -274,15 +274,15 @@ let autotraite_fichier_ML md ext = let a_faire_opt = ref "" in begin try while true do - let (Use_module str) = caml_action buf in - if StrSet.mem str !deja_vu then - () - else begin - deja_vu := StrSet.add str !deja_vu; - let byte,opt = depend_ML str in - a_faire := !a_faire ^ byte; - a_faire_opt := !a_faire_opt ^ opt - end + let (Use_module str) = caml_action buf in + if StrSet.mem str !deja_vu then + () + else begin + deja_vu := StrSet.add str !deja_vu; + let byte,opt = depend_ML str in + a_faire := !a_faire ^ byte; + a_faire_opt := !a_faire_opt ^ opt + end done with Fin_fichier -> () end; @@ -301,14 +301,14 @@ let traite_fichier_modules md ext = let list = mllib_list (Lexing.from_channel chan) in List.fold_left (fun a_faire str -> match search_mlpack_known str with - | Some mldir -> - let file = file_name str mldir in + | Some mldir -> + let file = file_name str mldir in a_faire @ [file] - | None -> - match search_ml_known str with - | Some mldir -> - let file = file_name str mldir in - a_faire @ [file] + | None -> + match search_ml_known str with + | Some mldir -> + let file = file_name str mldir in + a_faire @ [file] | None -> a_faire) [] list with | Sys_error _ -> [] @@ -329,16 +329,16 @@ let escape = let c = s.[i] in if c = ' ' || c = '#' || c = ':' (* separators and comments *) || c = '%' (* pattern *) - || c = '?' || c = '[' || c = ']' || c = '*' (* expansion in filenames *) - || i=0 && c = '~' && (String.length s = 1 || s.[1] = '/' || - 'A' <= s.[1] && s.[1] <= 'Z' || - 'a' <= s.[1] && s.[1] <= 'z') (* homedir expansion *) + || c = '?' || c = '[' || c = ']' || c = '*' (* expansion in filenames *) + || i=0 && c = '~' && (String.length s = 1 || s.[1] = '/' || + 'A' <= s.[1] && s.[1] <= 'Z' || + 'a' <= s.[1] && s.[1] <= 'z') (* homedir expansion *) then begin - let j = ref (i-1) in - while !j >= 0 && s.[!j] = '\\' do - Buffer.add_char s' '\\'; decr j (* escape all preceding '\' *) - done; - Buffer.add_char s' '\\'; + let j = ref (i-1) in + while !j >= 0 && s.[!j] = '\\' do + Buffer.add_char s' '\\'; decr j (* escape all preceding '\' *) + done; + Buffer.add_char s' '\\'; end; if c = '$' then Buffer.add_char s' '$'; Buffer.add_char s' c @@ -362,75 +362,116 @@ end module VCache = Set.Make(VData) -let rec traite_fichier_Coq suffixe verbose f = +(** To avoid reading .v files several times for computing dependencies, + once for .vo, once for .vio, and once for .vos extensions, the + following code performs a single pass and produces a structured + list of dependencies, separating dependencies on compiled Coq files + (those loaded by [Require]) from other dependencies, e.g. dependencies + on ".v" files (for [Load]) or ".cmx", ".cmo", etc... (for [Declare]). *) + +type dependency = + | DepRequire of string (* one basename, to which we later append .vo or .vio or .vos *) + | DepOther of string (* filenames of dependencies, separated by spaces *) + +let string_of_dependency_list suffix_for_require deps = + let string_of_dep = function + | DepRequire basename -> basename ^ suffix_for_require + | DepOther s -> s + in + String.concat " " (List.map string_of_dep deps) + +let rec find_dependencies basename = + let verbose = true in (* for past/future use? *) try + (* Visited marks *) + let visited_ml = ref StrSet.empty in + let visited_v = ref VCache.empty in + let should_visit_v_and_mark from str = + if not (VCache.mem (from, str) !visited_v) then begin + visited_v := VCache.add (from, str) !visited_v; + true + end else false + in + (* Output: dependencies found *) + let dependencies = ref [] in + let add_dep dep = + dependencies := dep::!dependencies in + let add_dep_other s = + add_dep (DepOther s) in + + (* Reading file contents *) + let f = basename ^ ".v" in let chan = open_in f in let buf = Lexing.from_channel chan in - let deja_vu_v = ref VCache.empty in - let deja_vu_ml = ref StrSet.empty in try while true do - let tok = coq_action buf in - match tok with - | Require (from, strl) -> - List.iter (fun str -> - if not (VCache.mem (from, str) !deja_vu_v) then begin - deja_vu_v := VCache.add (from, str) !deja_vu_v; - try - let file_str = safe_assoc from verbose f str in - printf " %s%s" (canonize file_str) suffixe - with Not_found -> - if verbose && not (is_in_coqlib ?from str) then - let str = - match from with - | None -> str - | Some pth -> pth @ str - in - warning_module_notfound f str - end) strl - | Declare sl -> - let declare suff dir s = - let base = escape (file_name s dir) in - match !option_dynlink with - | No -> () - | Byte -> printf " %s%s" base suff - | Opt -> printf " %s.cmxs" base - | Both -> printf " %s%s %s.cmxs" base suff base - | Variable -> - printf " %s%s" base - (if suff=".cmo" then "$(DYNOBJ)" else "$(DYNLIB)") + let tok = coq_action buf in + match tok with + | Require (from, strl) -> + List.iter (fun str -> + if should_visit_v_and_mark from str then begin + try + let file_str = safe_assoc from verbose f str in + add_dep (DepRequire (canonize file_str)) + with Not_found -> + if verbose && not (is_in_coqlib ?from str) then + let str = + match from with + | None -> str + | Some pth -> pth @ str + in + warning_module_notfound f str + end) strl + | Declare sl -> + let declare suff dir s = + let base = escape (file_name s dir) in + match !option_dynlink with + | No -> () + | Byte -> add_dep_other (sprintf "%s%s" base suff) + | Opt -> add_dep_other (sprintf "%s.cmxs" base) + | Both -> add_dep_other (sprintf "%s%s" base suff); + add_dep_other (sprintf "%s.cmxs" base) + | Variable -> add_dep_other (sprintf "%s%s" base + (if suff=".cmo" then "$(DYNOBJ)" else "$(DYNLIB)")) in - let decl str = - let s = basename_noext str in - if not (StrSet.mem s !deja_vu_ml) then begin - deja_vu_ml := StrSet.add s !deja_vu_ml; - match search_mllib_known s with - | Some mldir -> declare ".cma" mldir s - | None -> - match search_mlpack_known s with - | Some mldir -> declare ".cmo" mldir s - | None -> - match search_ml_known s with - | Some mldir -> declare ".cmo" mldir s - | None -> warning_declare f str - end - in List.iter decl sl - | Load str -> - let str = Filename.basename str in - if not (VCache.mem (None, [str]) !deja_vu_v) then begin - deja_vu_v := VCache.add (None, [str]) !deja_vu_v; - try - let (file_str, _) = Hashtbl.find vKnown [str] in - let canon = canonize file_str in - printf " %s.v" canon; - traite_fichier_Coq suffixe true (canon ^ ".v") - with Not_found -> () - end - | AddLoadPath _ | AddRecLoadPath _ -> (* TODO *) () - done - with Fin_fichier -> close_in chan - | Syntax_error (i,j) -> close_in chan; error_cannot_parse f (i,j) - with Sys_error _ -> () + let decl str = + let s = basename_noext str in + if not (StrSet.mem s !visited_ml) then begin + visited_ml := StrSet.add s !visited_ml; + match search_mllib_known s with + | Some mldir -> declare ".cma" mldir s + | None -> + match search_mlpack_known s with + | Some mldir -> declare ".cmo" mldir s + | None -> + match search_ml_known s with + | Some mldir -> declare ".cmo" mldir s + | None -> warning_declare f str + end + in + List.iter decl sl + | Load str -> + let str = Filename.basename str in + if should_visit_v_and_mark None [str] then begin + try + let (file_str, _) = Hashtbl.find vKnown [str] in + let canon = canonize file_str in + add_dep_other (sprintf "%s.v" canon); + let deps = find_dependencies canon in + List.iter add_dep deps + with Not_found -> () + end + | AddLoadPath _ | AddRecLoadPath _ -> (* TODO: will this be handled? *) () + done; + List.rev !dependencies + with + | Fin_fichier -> + close_in chan; + List.rev !dependencies + | Syntax_error (i,j) -> + close_in chan; + error_cannot_parse f (i,j) + with Sys_error _ -> [] (* TODO: report an error? *) let mL_dependencies () = @@ -439,8 +480,8 @@ let mL_dependencies () = let fullname = file_name name dirname in let (dep,dep_opt) = traite_fichier_ML fullname ext in let intf = match search_mli_known name with - | None -> "" - | Some mldir -> " "^(file_name name mldir)^".cmi" + | None -> "" + | Some mldir -> " "^(file_name name mldir)^".cmi" in let efullname = escape fullname in printf "%s.cmo:%s%s\n" efullname dep intf; @@ -481,12 +522,14 @@ let coq_dependencies () = (fun (name,_) -> let ename = escape name in let glob = if !option_noglob then "" else " "^ename^".glob" in - printf "%s%s%s %s.v.beautified: %s.v" ename !suffixe glob ename ename; - traite_fichier_Coq !suffixe true (name ^ ".v"); - printf "\n"; - printf "%s.vio: %s.v" ename ename; - traite_fichier_Coq ".vio" true (name ^ ".v"); - printf "\n%!") + let deps = find_dependencies name in + printf "%s%s%s %s.v.beautified %s.required_vo: %s.v %s\n" ename !suffixe glob ename ename ename + (string_of_dependency_list !suffixe deps); + printf "%s.vio: %s.v %s\n" ename ename + (string_of_dependency_list ".vio" deps); + printf "%s.vos %s.vok %s.required_vos: %s.v %s\n" ename ename ename ename + (string_of_dependency_list ".vos" deps); + printf "%!") (List.rev !vAccu) let rec suffixes = function @@ -505,26 +548,26 @@ let add_caml_known phys_dir _ f = | _ -> () let add_coqlib_known recur phys_dir log_dir f = - match get_extension f [".vo"; ".vio"] with - | (basename, (".vo" | ".vio")) -> + match get_extension f [".vo"; ".vio"; ".vos"] with + | (basename, (".vo" | ".vio" | ".vos")) -> let name = log_dir@[basename] in let paths = if recur then suffixes name else [name] in List.iter (fun f -> Hashtbl.add coqlibKnown f ()) paths | _ -> () let add_known recur phys_dir log_dir f = - match get_extension f [".v"; ".vo"; ".vio"] with + match get_extension f [".v"; ".vo"; ".vio"; ".vos"] with | (basename,".v") -> - let name = log_dir@[basename] in - let file = phys_dir//basename in - let () = safe_hash_add compare_file clash_v vKnown (name, (file, true)) in - if recur then + let name = log_dir@[basename] in + let file = phys_dir//basename in + let () = safe_hash_add compare_file clash_v vKnown (name, (file, true)) in + if recur then let paths = List.tl (suffixes name) in let iter n = safe_hash_add compare_file clash_v vKnown (n, (file, false)) in List.iter iter paths - | (basename, (".vo" | ".vio")) when not(!option_boot) -> + | (basename, (".vo" | ".vio" | ".vos")) when not(!option_boot) -> let name = log_dir@[basename] in - let paths = if recur then suffixes name else [name] in + let paths = if recur then suffixes name else [name] in List.iter (fun f -> Hashtbl.add coqlibKnown f ()) paths | _ -> () @@ -576,12 +619,12 @@ let rec treat_file old_dirname old_name = let complete_name = file_name name dirname in match try (stat complete_name).st_kind with _ -> S_BLK with | S_DIR -> - (if name.[0] <> '.' then + (if name.[0] <> '.' then let newdirname = match dirname with | None -> name | Some d -> d//name - in + in Array.iter (treat_file (Some newdirname)) (Sys.readdir complete_name)) | S_REG -> (match get_extension name [".v";".ml";".mli";".mlg";".mllib";".mlpack"] with |