diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/CoqMakefile.in | 2 | ||||
| -rw-r--r-- | tools/coqdep.ml | 53 | ||||
| -rw-r--r-- | tools/coqdep_common.ml | 49 | ||||
| -rw-r--r-- | tools/coqdep_common.mli | 2 | ||||
| -rw-r--r-- | tools/fake_ide.ml | 22 | ||||
| -rwxr-xr-x | tools/make-both-single-timing-files.py | 2 | ||||
| -rwxr-xr-x | tools/make-both-time-files.py | 2 | ||||
| -rwxr-xr-x | tools/make-one-time-file.py | 2 | ||||
| -rw-r--r-- | tools/ocamllibdep.mll | 12 |
9 files changed, 77 insertions, 69 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index f6539d80be..e5f22f25e1 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -382,7 +382,7 @@ real-all: $(VOFILES) $(if $(USEBYTE),bytefiles,optfiles) .PHONY: real-all real-all.timing.diff: $(VOFILES:.vo=.v.timing.diff) -.PHONE: real-all.timing.diff +.PHONY: real-all.timing.diff bytefiles: $(CMOFILES) $(CMAFILES) .PHONY: bytefiles diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 12b5cab0ac..7db0b28908 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -8,15 +8,24 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Printf +open Format open Coqdep_lexer open Coqdep_common -open System +open Minisys (** The basic parts of coqdep (i.e. the parts used by [coqdep -boot]) are now in [Coqdep_common]. The code that remains here concerns the other options. Calling this complete coqdep with the [-boot] option should be equivalent to calling [coqdep_boot]. + + As of today, this module depends on the following Coq modules: + + - Flags + - Envars + - CoqProject_file + + All of it for `coqlib` handling. Ideally we would like to clean + coqlib handling up so this can be bootstrapped earlier. *) let option_D = ref false @@ -31,8 +40,7 @@ let warning_mult suf iter = let d' = Hashtbl.find tab f in if (Filename.dirname (file_name f d)) <> (Filename.dirname (file_name f d')) then begin - eprintf "*** Warning : the file %s is defined twice!\n" (f ^ suf); - flush stderr + coqdep_warning "the file %s is defined twice!" (f ^ suf) end with Not_found -> () end; Hashtbl.add tab f d @@ -80,9 +88,7 @@ let mL_dep_list b f = while true do let (Use_module str) = caml_action buf in if str = b then begin - eprintf "*** Warning : in file %s the" f; - eprintf " notation %s. is useless !\n" b; - flush stderr + coqdep_warning "in file %s the notation %s. is useless !\n" f b end else if not (List.mem str !deja_vu) then addQueue deja_vu str done; [] @@ -98,16 +104,13 @@ let affiche_Declare f dcl = printf "\n*** In file %s: \n" f; printf "Declare ML Module"; List.iter (fun str -> printf " \"%s\"" str) dcl; - printf ".\n"; - flush stdout + printf ".\n%!" let warning_Declare f dcl = - eprintf "*** Warning : in file %s, the ML modules" f; - eprintf " declaration should be\n"; + eprintf "*** Warning : in file %s, the ML modules declaration should be\n" f; eprintf "*** Declare ML Module"; List.iter (fun str -> eprintf " \"%s\"" str) dcl; - eprintf ".\n"; - flush stderr + eprintf ".\n%!" let traite_Declare f = let decl_list = ref ([] : string list) in @@ -149,7 +152,7 @@ let declare_dependencies () = List.iter (fun (name,_) -> traite_Declare (name^".v"); - flush stdout) + pp_print_flush std_formatter ()) (List.rev !vAccu) (** DAGs guaranteed to be transitive reductions *) @@ -426,11 +429,11 @@ let coq_dependencies_dump chan dumpboxes = (DAG.empty, List.fold_left (fun ih (file, _) -> insert_raw_graph file ih) [] !vAccu, List.map fst !vAccu) !vAccu in - fprintf chan "digraph dependencies {\n"; flush chan; + fprintf chan "digraph dependencies {\n"; if dumpboxes then print_graphs chan (pop_common_prefix graphs) else List.iter (fun (name, _) -> fprintf chan "\"%s\"[label=\"%s\"]\n" name (basename_noext name)) !vAccu; DAG.iter (fun name dep -> fprintf chan "\"%s\" -> \"%s\"\n" dep name) deps; - fprintf chan "}\n" + fprintf chan "}\n%!" end @@ -498,7 +501,7 @@ let rec parse = function | "-suffix" :: s :: ll -> suffixe := s ; parse ll | "-suffix" :: [] -> usage () | "-slash" :: ll -> - Printf.eprintf "warning: option -slash has no effect and is deprecated.\n"; + coqdep_warning "warning: option -slash has no effect and is deprecated."; parse ll | "-dyndep" :: "no" :: ll -> option_dynlink := No; parse ll | "-dyndep" :: "opt" :: ll -> option_dynlink := Opt; parse ll @@ -509,6 +512,9 @@ let rec parse = function | f :: ll -> treat_file None f; parse ll | [] -> () +(* Exception to be raised by Envars *) +exception CoqlibError of string + let coqdep () = if Array.length Sys.argv < 2 then usage (); if not Coq_config.has_natdynlink then option_dynlink := No; @@ -520,18 +526,17 @@ let coqdep () = if !option_boot then begin add_rec_dir_import add_known "theories" ["Coq"]; add_rec_dir_import add_known "plugins" ["Coq"]; - add_caml_dir "tactics"; add_rec_dir_import (fun _ -> add_caml_known) "theories" ["Coq"]; add_rec_dir_import (fun _ -> add_caml_known) "plugins" ["Coq"]; end else begin - Envars.set_coqlib ~fail:(fun msg -> CErrors.user_err Pp.(str msg)); + Envars.set_coqlib ~fail:(fun msg -> raise (CoqlibError msg)); let coqlib = Envars.coqlib () in add_rec_dir_import add_coqlib_known (coqlib//"theories") ["Coq"]; add_rec_dir_import add_coqlib_known (coqlib//"plugins") ["Coq"]; let user = coqlib//"user-contrib" in if Sys.file_exists user then add_rec_dir_no_import add_coqlib_known user []; List.iter (fun s -> add_rec_dir_no_import add_coqlib_known s []) - (Envars.xdg_dirs ~warn:(fun x -> Feedback.msg_warning (Pp.str x))); + (Envars.xdg_dirs ~warn:(fun x -> coqdep_warning "%s" x)); List.iter (fun s -> add_rec_dir_no_import add_coqlib_known s []) Envars.coqpath; end; List.iter (fun (f,d) -> add_mli_known f d ".mli") !mliAccu; @@ -547,13 +552,13 @@ let coqdep () = | None -> () | Some (box, file) -> let chan = open_out file in - try Graph.coq_dependencies_dump chan box; close_out chan + let chan_fmt = formatter_of_out_channel chan in + try Graph.coq_dependencies_dump chan_fmt box; close_out chan with e -> close_out chan; raise e end let _ = try coqdep () - with CErrors.UserError(s,p) -> - let pp = (match s with | None -> p | Some s -> Pp.(str s ++ str ": " ++ p)) in - Format.eprintf "%a@\n%!" Pp.pp_with pp + with CoqlibError msg -> + eprintf "*** Error: %s@\n%!" msg diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index 70c983175d..23b8bc112e 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -8,9 +8,9 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Printf -open Coqdep_lexer +open Format open Unix +open Coqdep_lexer open Minisys (** [coqdep_boot] is a stripped-down version of [coqdep], whose @@ -20,14 +20,15 @@ open Minisys options (see for instance [option_dynlink] below). *) +let coqdep_warning args = + eprintf "*** Warning: @["; + kfprintf (fun fmt -> fprintf fmt "@]\n%!") err_formatter args + module StrSet = Set.Make(String) module StrList = struct type t = string list let compare = compare end module StrListMap = Map.Make(StrList) -let stderr = Pervasives.stderr -let stdout = Pervasives.stdout - type dynlink = Opt | Byte | Both | No | Variable let option_c = ref false @@ -102,10 +103,19 @@ let safe_hash_add cmp clq q (k, (v, b)) = For the ML files, the string is the basename without extension. *) +let same_path_opt s s' = + let nf s = (* ./foo/a.ml and foo/a.ml are the same file *) + if Filename.is_implicit s + then "." // s + else s + in + let s = match s with None -> "." | Some s -> nf s in + let s' = match s' with None -> "." | Some s' -> nf s' in + s = s' + let warning_ml_clash x s suff s' suff' = - if suff = suff' then - eprintf - "*** Warning: %s%s already found in %s (discarding %s%s)\n" x suff + if suff = suff' && not (same_path_opt s s') then + coqdep_warning "%s%s already found in %s (discarding %s%s)\n" x suff (match s with None -> "." | Some d -> d) ((match s' with None -> "." | Some d -> d) // x) suff @@ -170,13 +180,11 @@ let error_cannot_parse s (i,j) = exit 1 let warning_module_notfound f s = - eprintf "*** Warning: in file %s, library %s is required and has not been found in the loadpath!\n%!" + coqdep_warning "in file %s, library %s is required and has not been found in the loadpath!" f (String.concat "." s) let warning_declare f s = - eprintf "*** Warning: in file %s, declared ML module " f; - eprintf "%s has not been found!\n" s; - flush stderr + coqdep_warning "in file %s, declared ML module %s has not been found!" f s let warning_clash file dir = match StrListMap.find dir !clash_v with @@ -193,8 +201,7 @@ let warning_clash file dir = | _ -> assert false let warning_cannot_open_dir dir = - eprintf "*** Warning: cannot open %s\n" dir; - flush stderr + coqdep_warning "cannot open %s" dir let safe_assoc from verbose file k = if verbose && StrListMap.mem k !clash_v then warning_clash file k; @@ -441,15 +448,13 @@ let mL_dependencies () = in let efullname = escape fullname in printf "%s.cmo:%s%s\n" efullname dep intf; - printf "%s.cmx:%s%s\n" efullname dep_opt intf; - flush stdout) + printf "%s.cmx:%s%s\n%!" efullname dep_opt intf) (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\n" (escape fullname) dep; - flush stdout) + printf "%s.cmi:%s\n%!" (escape fullname) dep) (List.rev !mliAccu); List.iter (fun (name,dirname) -> @@ -458,8 +463,7 @@ let mL_dependencies () = let efullname = escape fullname in printf "%s_MLLIB_DEPENDENCIES:=%s\n" efullname (String.concat " " dep); printf "%s.cma:$(addsuffix .cmo,$(%s_MLLIB_DEPENDENCIES))\n" efullname efullname; - printf "%s.cmxa:$(addsuffix .cmx,$(%s_MLLIB_DEPENDENCIES))\n" efullname efullname; - flush stdout) + printf "%s.cmxa:$(addsuffix .cmx,$(%s_MLLIB_DEPENDENCIES))\n%!" efullname efullname) (List.rev !mllibAccu); List.iter (fun (name,dirname) -> @@ -473,7 +477,7 @@ let mL_dependencies () = List.iter (fun dep -> printf "%s.cmx : FOR_PACK=-for-pack %s\n" dep efullname_capital) dep; - flush stdout) + printf "%!") (List.rev !mlpackAccu) let coq_dependencies () = @@ -486,8 +490,7 @@ let coq_dependencies () = printf "\n"; printf "%s.vio: %s.v" ename ename; traite_fichier_Coq ".vio" true (name ^ ".v"); - printf "\n"; - flush stdout) + printf "\n%!") (List.rev !vAccu) let rec suffixes = function diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli index d0d7932435..91d2b45876 100644 --- a/tools/coqdep_common.mli +++ b/tools/coqdep_common.mli @@ -10,6 +10,8 @@ module StrSet : Set.S with type elt = string +val coqdep_warning : ('a, Format.formatter, unit, unit) format4 -> 'a + (** [find_dir_logpath dir] Return the logical path of directory [dir] if it has been given one. Raise [Not_found] otherwise. In particular we can check if "." has been attributed a logical path diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml index d48c6d0af5..0162011289 100644 --- a/tools/fake_ide.ml +++ b/tools/fake_ide.ml @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -(** Fake_ide : Simulate a [coqide] talking to a [coqtop -ideslave] *) +(** Fake_ide : Simulate a [coqide] talking to a [coqidetop] *) let error s = prerr_endline ("fake_id: error: "^s); @@ -284,7 +284,7 @@ let read_command inc = Parser.parse grammar inc let usage () = error (Printf.sprintf - "A fake coqide process talking to a coqtop -ideslave.\n\ + "A fake coqide process talking to a coqtop -toploop coqidetop.\n\ Usage: %s (file|-) [<coqtop>]\n\ Input syntax is the following:\n%s\n" (Filename.basename Sys.argv.(0)) @@ -296,20 +296,8 @@ let main = if Sys.os_type = "Unix" then Sys.set_signal Sys.sigpipe (Sys.Signal_handle (fun _ -> prerr_endline "Broken Pipe (coqtop died ?)"; exit 1)); - let def_args = ["--xml_format=Ppcmds"; "-ideslave"] in - let coqtop_name = (* from ide/ideutils.ml *) - let prog_name = "fake_ide" in - let len_prog_name = String.length prog_name in - let fake_ide_path = Sys.executable_name in - let fake_ide_path_len = String.length fake_ide_path in - let pos = fake_ide_path_len - len_prog_name in - let rex = Str.regexp_string prog_name in - try - let i = Str.search_backward rex fake_ide_path pos in - String.sub fake_ide_path 0 i ^ "coqtop" ^ - String.sub fake_ide_path (i + len_prog_name) - (fake_ide_path_len - i - len_prog_name) - with Not_found -> assert false in + let def_args = ["--xml_format=Ppcmds"] in + let idetop_name = System.get_toplevel_path "coqidetop" in let coqtop_args, input_file = match Sys.argv with | [| _; f |] -> Array.of_list def_args, f | [| _; f; ct |] -> @@ -318,7 +306,7 @@ let main = | _ -> usage () in let inc = if input_file = "-" then stdin else open_in input_file in let coq = - let _p, cin, cout = Coqide.spawn coqtop_name coqtop_args in + let _p, cin, cout = Coqide.spawn idetop_name coqtop_args in let ip = Xml_parser.make (Xml_parser.SChannel cin) in let op = Xml_printer.make (Xml_printer.TChannel cout) in Xml_parser.check_eof ip false; diff --git a/tools/make-both-single-timing-files.py b/tools/make-both-single-timing-files.py index 32c52c7a17..c6af2ff1f8 100755 --- a/tools/make-both-single-timing-files.py +++ b/tools/make-both-single-timing-files.py @@ -1,4 +1,4 @@ -#!/usr/bin/env python +#!/usr/bin/env python2 import sys from TimeFileMaker import * diff --git a/tools/make-both-time-files.py b/tools/make-both-time-files.py index f730a8d6bd..6434296793 100755 --- a/tools/make-both-time-files.py +++ b/tools/make-both-time-files.py @@ -1,4 +1,4 @@ -#!/usr/bin/env python +#!/usr/bin/env python2 import sys from TimeFileMaker import * diff --git a/tools/make-one-time-file.py b/tools/make-one-time-file.py index e66136df9d..c9905249e6 100755 --- a/tools/make-one-time-file.py +++ b/tools/make-one-time-file.py @@ -1,4 +1,4 @@ -#!/usr/bin/env python +#!/usr/bin/env python2 import sys from TimeFileMaker import * diff --git a/tools/ocamllibdep.mll b/tools/ocamllibdep.mll index 125c1452d5..382c39d3f2 100644 --- a/tools/ocamllibdep.mll +++ b/tools/ocamllibdep.mll @@ -116,8 +116,18 @@ let error_cannot_parse s (i,j) = Printf.eprintf "File \"%s\", characters %i-%i: Syntax error\n" s i j; exit 1 +let same_path_opt s s' = + let nf s = (* ./foo/a.ml and foo/a.ml are the same file *) + if Filename.is_implicit s + then "." // s + else s + in + let s = match s with None -> "." | Some s -> nf s in + let s' = match s' with None -> "." | Some s' -> nf s' in + s = s' + let warning_ml_clash x s suff s' suff' = - if suff = suff' then + if suff = suff' && not (same_path_opt s s') then eprintf "*** Warning: %s%s already found in %s (discarding %s%s)\n" x suff (match s with None -> "." | Some d -> d) |