diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/CoqMakefile.in | 10 | ||||
| -rw-r--r-- | tools/TimeFileMaker.py | 39 | ||||
| -rw-r--r-- | tools/coq_dune.ml | 18 | ||||
| -rw-r--r-- | tools/coqdep.ml | 8 | ||||
| -rw-r--r-- | tools/coqdep_boot.ml | 4 |
5 files changed, 53 insertions, 26 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index bd9d8c9221..2ec55d1bd0 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -38,6 +38,7 @@ DOCDIR := $(COQMF_DOCDIR) OCAMLFIND := $(COQMF_OCAMLFIND) CAMLFLAGS := $(COQMF_CAMLFLAGS) HASNATDYNLINK := $(COQMF_HASNATDYNLINK) +OCAMLWARN := $(COQMF_WARN) @CONF_FILE@: @PROJECT_FILE@ @COQ_MAKEFILE_INVOCATION@ @@ -176,7 +177,7 @@ COQCHKEXTRAFLAGS?= COQDOCEXTRAFLAGS?= # these flags do NOT contain the libraries, to make them easier to overwrite -COQFLAGS?=-q $(OPT) $(OTHERFLAGS) $(COQEXTRAFLAGS) +COQFLAGS?=-q $(OTHERFLAGS) $(COQEXTRAFLAGS) COQCHKFLAGS?=-silent -o $(COQCHKEXTRAFLAGS) COQDOCFLAGS?=-interpolate -utf8 $(COQDOCEXTRAFLAGS) @@ -190,9 +191,9 @@ COQMAKEFILE_VERSION:=@COQ_VERSION@ COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)/$(d)") CAMLFLAGS+=$(OCAMLLIBS) $(COQSRCLIBS) - # ocamldoc fails with unknown argument otherwise -CAMLDOCFLAGS=$(filter-out -annot, $(filter-out -bin-annot, $(CAMLFLAGS))) +CAMLDOCFLAGS:=$(filter-out -annot, $(filter-out -bin-annot, $(CAMLFLAGS))) +CAMLFLAGS+=$(OCAMLWARN) ifneq (,$(TIMING)) TIMING_ARG=-time @@ -468,6 +469,9 @@ beautify: $(BEAUTYFILES) # Extensions can't assume when they run. install: + $(HIDE)code=0; for f in $(FILESTOINSTALL); do\ + if ! [ -f "$$f" ]; then >&2 echo $$f does not exist; code=1; fi \ + done; exit $$code $(HIDE)for f in $(FILESTOINSTALL); do\ df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`";\ if [ "$$?" != "0" -o -z "$$df" ]; then\ diff --git a/tools/TimeFileMaker.py b/tools/TimeFileMaker.py index 854dd25b75..3d07661d56 100644 --- a/tools/TimeFileMaker.py +++ b/tools/TimeFileMaker.py @@ -34,6 +34,24 @@ def reformat_time_string(time): minutes, seconds = divmod(seconds, 60) return '%dm%02d.%ss' % (minutes, seconds, milliseconds) +def get_file_lines(file_name): + if file_name == '-': + if hasattr(sys.stdin, 'buffer'): + lines = sys.stdin.buffer.readlines() + else: + lines = sys.stdin.readlines() + else: + with open(file_name, 'rb') as f: + lines = f.readlines() + for line in lines: + try: + yield line.decode('utf-8') + except UnicodeDecodeError: # invalid utf-8 + pass + +def get_file(file_name): + return ''.join(get_file_lines(file_name)) + def get_times(file_name): ''' Reads the contents of file_name, which should be the output of @@ -41,11 +59,7 @@ def get_times(file_name): names to compile durations, as strings. Removes common prefixes using STRIP_REG and STRIP_REP. ''' - if file_name == '-': - lines = sys.stdin.read() - else: - with open(file_name, 'r', encoding="utf-8") as f: - lines = f.read() + lines = get_file(file_name) reg = re.compile(r'^([^\s]+) \([^\)]*?user: ([0-9\.]+)[^\)]*?\)\s*$', re.MULTILINE) times = reg.findall(lines) if all(time in ('0.00', '0.01') for name, time in times): @@ -61,11 +75,7 @@ def get_single_file_times(file_name): 'coqc -time', and parses it to construct a dict mapping lines to to compile durations, as strings. ''' - if file_name == '-': - lines = sys.stdin.read() - else: - with open(file_name, 'r', encoding="utf-8") as f: - lines = f.read() + lines = get_file(file_name) reg = re.compile(r'^Chars ([0-9]+) - ([0-9]+) ([^ ]+) ([0-9\.]+) secs (.*)$', re.MULTILINE) times = reg.findall(lines) if len(times) == 0: return dict() @@ -209,11 +219,10 @@ def make_table_string(times_dict, def print_or_write_table(table, files): if len(files) == 0 or '-' in files: - try: - binary_stdout = sys.stdout.buffer - except AttributeError: - binary_stdout = sys.stdout - print(table.encode("utf-8"), file=binary_stdout) + if hasattr(sys.stdout, 'buffer'): + sys.stdout.buffer.write(table.encode("utf-8")) + else: + sys.stdout.write(table.encode("utf-8")) for file_name in files: if file_name != '-': with open(file_name, 'w', encoding="utf-8") as f: diff --git a/tools/coq_dune.ml b/tools/coq_dune.ml index fa8b771a74..6ddc503542 100644 --- a/tools/coq_dune.ml +++ b/tools/coq_dune.ml @@ -214,7 +214,7 @@ let record_dune d ff = if Sys.file_exists sd && Sys.is_directory sd then let out = open_out (bpath [sd;"dune"]) in let fmt = formatter_of_out_channel out in - if List.nth d 0 = "plugins" then + if List.nth d 0 = "plugins" || List.nth d 0 = "user-contrib" then fprintf fmt "(include plugin_base.dune)@\n"; out_install fmt d ff; List.iter (pp_dep d fmt) ff; @@ -224,17 +224,20 @@ let record_dune d ff = eprintf "error in coq_dune, a directory disappeared: %s@\n%!" sd (* File Scanning *) -let scan_mlg m d = - let dir = ["plugins"; d] in +let scan_mlg ~root m d = + let dir = [root; d] in let m = DirMap.add dir [] m in let mlg = Sys.(List.filter (fun f -> Filename.(check_suffix f ".mlg")) Array.(to_list @@ readdir (bpath dir))) in - List.fold_left (fun m f -> add_map_list ["plugins"; d] (MLG f) m) m mlg + List.fold_left (fun m f -> add_map_list [root; d] (MLG f) m) m mlg -let scan_plugins m = +let scan_dir ~root m = let is_plugin_directory dir = Sys.(is_directory dir && file_exists (bpath [dir;"plugin_base.dune"])) in - let dirs = Sys.(List.filter (fun f -> is_plugin_directory @@ bpath ["plugins";f]) Array.(to_list @@ readdir "plugins")) in - List.fold_left scan_mlg m dirs + let dirs = Sys.(List.filter (fun f -> is_plugin_directory @@ bpath [root;f]) Array.(to_list @@ readdir root)) in + List.fold_left (scan_mlg ~root) m dirs + +let scan_plugins m = scan_dir ~root:"plugins" m +let scan_usercontrib m = scan_dir ~root:"user-contrib" m (* This will be removed when we drop support for Make *) let fix_cmo_cma file = @@ -291,5 +294,6 @@ let exec_ifile f = let _ = exec_ifile (fun ic -> let map = scan_plugins DirMap.empty in + let map = scan_usercontrib map in let map = read_vfiles ic map in out_map map) diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 66f1f257b8..8823206252 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -529,6 +529,11 @@ let coqdep () = add_rec_dir_import add_known "plugins" ["Coq"]; add_rec_dir_import (fun _ -> add_caml_known) "theories" ["Coq"]; add_rec_dir_import (fun _ -> add_caml_known) "plugins" ["Coq"]; + let user = "user-contrib" in + if Sys.file_exists user then begin + add_rec_dir_no_import add_known user []; + add_rec_dir_no_import (fun _ -> add_caml_known) user []; + end; end else begin (* option_boot is actually always false in this branch *) Envars.set_coqlib ~fail:(fun msg -> raise (CoqlibError msg)); @@ -563,4 +568,5 @@ let _ = try coqdep () with CoqlibError msg -> - eprintf "*** Error: %s@\n%!" msg + eprintf "*** Error: %s@\n%!" msg; + exit 1 diff --git a/tools/coqdep_boot.ml b/tools/coqdep_boot.ml index aa023e6986..a638906c11 100644 --- a/tools/coqdep_boot.ml +++ b/tools/coqdep_boot.ml @@ -17,6 +17,9 @@ open Coqdep_common options (see for instance [option_natdynlk] below). *) +let split_period = Str.split (Str.regexp (Str.quote ".")) +let add_q_include path l = add_rec_dir_no_import add_known path (split_period l) + let rec parse = function | "-dyndep" :: "no" :: ll -> option_dynlink := No; parse ll | "-dyndep" :: "opt" :: ll -> option_dynlink := Opt; parse ll @@ -33,6 +36,7 @@ let rec parse = function add_caml_dir r; norec_dirs := StrSet.add r !norec_dirs; parse ll + | "-Q" :: r :: ln :: ll -> add_q_include r ln; parse ll | f :: ll -> treat_file None f; parse ll | [] -> () |