diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/CoqMakefile.in | 38 | ||||
| -rw-r--r-- | tools/TimeFileMaker.py | 169 | ||||
| -rw-r--r-- | tools/coq_dune.ml | 9 | ||||
| -rw-r--r-- | tools/coqdep.ml | 11 | ||||
| -rw-r--r-- | tools/coqdep_common.ml | 152 | ||||
| -rw-r--r-- | tools/coqdep_common.mli | 11 | ||||
| -rw-r--r-- | tools/coqdep_lexer.mli | 7 | ||||
| -rw-r--r-- | tools/coqdep_lexer.mll | 83 | ||||
| -rw-r--r-- | tools/dune | 10 | ||||
| -rwxr-xr-x | tools/make-both-single-timing-files.py | 21 | ||||
| -rwxr-xr-x | tools/make-both-time-files.py | 23 | ||||
| -rwxr-xr-x | tools/make-one-time-file.py | 24 | ||||
| -rw-r--r-- | tools/ocamllibdep.mll | 11 |
13 files changed, 249 insertions, 320 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index d3ed5e78b4..1d682218b6 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -91,6 +91,7 @@ COQDEP ?= "$(COQBIN)coqdep" COQDOC ?= "$(COQBIN)coqdoc" COQPP ?= "$(COQBIN)coqpp" COQMKFILE ?= "$(COQBIN)coq_makefile" +OCAMLLIBDEP ?= "$(COQBIN)ocamllibdep" # Timing scripts COQMAKE_ONE_TIME_FILE ?= "$(COQLIB)/tools/make-one-time-file.py" @@ -124,6 +125,10 @@ CAMLPKGS ?= TIMING?= # Option for changing sorting of timing output file TIMING_SORT_BY ?= auto +# Option for changing the fuzz parameter on the output file +TIMING_FUZZ ?= 0 +# Option for changing whether to use real or user time for timing tables +TIMING_REAL?= # Output file names for timed builds TIME_OF_BUILD_FILE ?= time-of-build.log TIME_OF_BUILD_BEFORE_FILE ?= time-of-build-before.log @@ -334,6 +339,19 @@ all.timing.diff: $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" post-all .PHONY: all.timing.diff +ifeq (0,$(TIMING_REAL)) +TIMING_REAL_ARG := +TIMING_USER_ARG := --user +else +ifeq (1,$(TIMING_REAL)) +TIMING_REAL_ARG := --real +TIMING_USER_ARG := +else +TIMING_REAL_ARG := +TIMING_USER_ARG := +endif +endif + make-pretty-timed-before:: TIME_OF_BUILD_FILE=$(TIME_OF_BUILD_BEFORE_FILE) make-pretty-timed-after:: TIME_OF_BUILD_FILE=$(TIME_OF_BUILD_AFTER_FILE) make-pretty-timed make-pretty-timed-before make-pretty-timed-after:: @@ -341,9 +359,9 @@ make-pretty-timed make-pretty-timed-before make-pretty-timed-after:: $(HIDE)($(MAKE) --no-print-directory -f "$(PARENT)" $(TGTS) TIMED=1 2>&1 && touch pretty-timed-success.ok) | tee -a $(TIME_OF_BUILD_FILE) $(HIDE)rm pretty-timed-success.ok # must not be -f; must fail if the touch failed print-pretty-timed:: - $(HIDE)$(COQMAKE_ONE_TIME_FILE) $(TIME_OF_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) + $(HIDE)$(COQMAKE_ONE_TIME_FILE) $(TIMING_REAL_ARG) $(TIME_OF_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) print-pretty-timed-diff:: - $(HIDE)$(COQMAKE_BOTH_TIME_FILES) --sort-by=$(TIMING_SORT_BY) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_PRETTY_BOTH_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) + $(HIDE)$(COQMAKE_BOTH_TIME_FILES) --sort-by=$(TIMING_SORT_BY) $(TIMING_REAL_ARG) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_PRETTY_BOTH_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) ifeq (,$(BEFORE)) print-pretty-single-time-diff:: @echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff AFTER=path/to/file.v.after-timing BEFORE=path/to/file.v.before-timing' @@ -355,7 +373,7 @@ print-pretty-single-time-diff:: $(HIDE)false else print-pretty-single-time-diff:: - $(HIDE)$(COQMAKE_BOTH_SINGLE_TIMING_FILES) --sort-by=$(TIMING_SORT_BY) $(AFTER) $(BEFORE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) + $(HIDE)$(COQMAKE_BOTH_SINGLE_TIMING_FILES) --fuzz=$(TIMING_FUZZ) --sort-by=$(TIMING_SORT_BY) $(TIMING_USER_ARG) $(AFTER) $(BEFORE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) endif endif pretty-timed: @@ -455,13 +473,13 @@ all.ps: $(VFILES) $(SHOW)'COQDOC -ps $(GAL)' $(HIDE)$(COQDOC) \ -toc $(COQDOCFLAGS) -ps $(GAL) $(COQDOCLIBS) \ - -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)` + -o $@ `$(COQDEP) -sort $(VFILES)` all.pdf: $(VFILES) $(SHOW)'COQDOC -pdf $(GAL)' $(HIDE)$(COQDOC) \ -toc $(COQDOCFLAGS) -pdf $(GAL) $(COQDOCLIBS) \ - -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)` + -o $@ `$(COQDEP) -sort $(VFILES)` # FIXME: not quite right, since the output name is different gallinahtml: GAL=-g @@ -694,7 +712,7 @@ $(VFILES:.v=.vok): %.vok: %.v $(HIDE)$(TIMER) $(COQC) -vok $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< $(addsuffix .timing.diff,$(VFILES)): %.timing.diff : %.before-timing %.after-timing - $(SHOW)PYTHON TIMING-DIFF $< + $(SHOW)PYTHON TIMING-DIFF $*.{before,after}-timing $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" print-pretty-single-time-diff BEFORE=$*.before-timing AFTER=$*.after-timing TIME_OF_PRETTY_BUILD_FILE="$@" $(BEAUTYFILES): %.v.beautified: %.v @@ -747,12 +765,12 @@ $(addsuffix .d,$(MLFILES)): %.ml.d: %.ml $(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok) $(addsuffix .d,$(MLLIBFILES)): %.mllib.d: %.mllib - $(SHOW)'COQDEP $<' - $(HIDE)$(COQDEP) $(OCAMLLIBS) -c "$<" $(redir_if_ok) + $(SHOW)'OCAMLLIBDEP $<' + $(HIDE)$(OCAMLLIBDEP) -c $(OCAMLLIBS) "$<" $(redir_if_ok) $(addsuffix .d,$(MLPACKFILES)): %.mlpack.d: %.mlpack - $(SHOW)'COQDEP $<' - $(HIDE)$(COQDEP) $(OCAMLLIBS) -c "$<" $(redir_if_ok) + $(SHOW)'OCAMLLIBDEP $<' + $(HIDE)$(OCAMLLIBDEP) -c $(OCAMLLIBS) "$<" $(redir_if_ok) # If this makefile is created using a _CoqProject we have coqdep get # options from it. This avoids argument length limits for pathological diff --git a/tools/TimeFileMaker.py b/tools/TimeFileMaker.py index 3d07661d56..210901f8a7 100644 --- a/tools/TimeFileMaker.py +++ b/tools/TimeFileMaker.py @@ -4,6 +4,7 @@ from __future__ import unicode_literals from __future__ import print_function import sys import re +import argparse from io import open # This script parses the output of `make TIMED=1` into a dictionary @@ -14,18 +15,76 @@ STRIP_REG = re.compile('^(coq/|contrib/|)(?:theories/|src/)?') STRIP_REP = r'\1' INFINITY = '\u221e' -def parse_args(argv, USAGE, HELP_STRING): - sort_by = 'auto' - if any(arg.startswith('--sort-by=') for arg in argv[1:]): - sort_by = [arg for arg in argv[1:] if arg.startswith('--sort-by=')][-1][len('--sort-by='):] - args = [arg for arg in argv if not arg.startswith('--sort-by=')] - if len(args) < 3 or '--help' in args[1:] or '-h' in args[1:] or sort_by not in ('auto', 'absolute', 'diff'): - print(USAGE) - if '--help' in args[1:] or '-h' in args[1:]: - print(HELP_STRING) - if len(args) == 2: sys.exit(0) - sys.exit(1) - return sort_by, args +def nonnegative(arg): + v = int(arg) + if v < 0: raise argparse.ArgumentTypeError("%s is an invalid non-negative int value" % arg) + return v + +def add_sort_by(parser): + return parser.add_argument( + '--sort-by', type=str, dest='sort_by', choices=('auto', 'absolute', 'diff'), + default='auto', + help=('How to sort the table entries.\n' + + 'The "auto" method sorts by absolute time differences ' + + 'rounded towards zero to a whole-number of seconds, then ' + + 'by times in the "after" column, and finally ' + + 'lexicographically by file name. This will put the ' + + 'biggest changes in either direction first, and will ' + + 'prefer sorting by build-time over subsecond changes in ' + + 'build time (which are frequently noise); lexicographic ' + + 'sorting forces an order on files which take effectively ' + + 'no time to compile.\n' + + 'The "absolute" method sorts by the total time taken.\n' + + 'The "diff" method sorts by the signed difference in time.')) + +def add_fuzz(parser): + return parser.add_argument( + '--fuzz', dest='fuzz', metavar='N', type=nonnegative, default=0, + help=('By default, two lines are only considered the same if ' + + 'the character offsets and initial code strings match. ' + 'This option relaxes this constraint by allowing the ' + + 'character offsets to differ by up to N characters, as long ' + + 'as the total number of characters and initial code strings ' + + 'continue to match. This is useful when there are small changes ' + + 'to a file, and you want to match later lines that have not ' + + 'changed even though the character offsets have changed.')) + +def add_real(parser, single_timing=False): + return parser.add_argument( + '--real', action='store_true', + help=(r'''Use real times rather than user times. + +''' + ('''By default, the input is expected to contain lines in the format: +FILE_NAME (...user: NUMBER_IN_SECONDS...) +If --real is passed, then the lines are instead expected in the format: +FILE_NAME (...real: NUMBER_IN_SECONDS...)''' if not single_timing else +'''The input is expected to contain lines in the format: +Chars START - END COMMAND NUMBER secs (NUMBERu...)'''))) + +def add_user(parser, single_timing=False): + return parser.add_argument( + '--user', dest='real', action='store_false', + help=(r'''Use user times rather than real times. + +''' + ('''By default, the input is expected to contain lines in the format: +FILE_NAME (...real: NUMBER_IN_SECONDS...) +If --user is passed, then the lines are instead expected in the format: +FILE_NAME (...user: NUMBER_IN_SECONDS...)''' if not single_timing else +'''The input is expected to contain lines in the format: +Chars START - END COMMAND NUMBER secs (NUMBERu...)'''))) + +# N.B. We need to include default=None for nargs='*', c.f., https://bugs.python.org/issue28609#msg280180 +def add_file_name_gen(parser, prefix='', descr='file containing the build log', stddir='in', defaults=None, **kwargs): + extra = ('' if defaults is None else ' (defaults to %s if no argument is passed)' % defaults) + return parser.add_argument( + prefix + 'FILE_NAME', type=str, + help=('The name of the %s (use "-" for std%s)%s.' % (descr, stddir, extra)), + **kwargs) + +def add_file_name(parser): return add_file_name_gen(parser) +def add_after_file_name(parser): return add_file_name_gen(parser, 'AFTER_', 'file containing the "after" build log') +def add_before_file_name(parser): return add_file_name_gen(parser, 'BEFORE_', 'file containing the "before" build log') +def add_output_file_name(parser): return add_file_name_gen(parser, 'OUTPUT_', 'file to write the output table to', stddir='out', defaults='-', nargs='*', default=None) def reformat_time_string(time): @@ -45,14 +104,16 @@ def get_file_lines(file_name): lines = f.readlines() for line in lines: try: - yield line.decode('utf-8') + # Since we read the files in binary mode, we have to + # normalize Windows line endings from \r\n to \n + yield line.decode('utf-8').replace('\r\n', '\n') except UnicodeDecodeError: # invalid utf-8 pass def get_file(file_name): return ''.join(get_file_lines(file_name)) -def get_times(file_name): +def get_times(file_name, use_real=False): ''' Reads the contents of file_name, which should be the output of 'make TIMED=1', and parses it to construct a dict mapping file @@ -60,28 +121,96 @@ def get_times(file_name): using STRIP_REG and STRIP_REP. ''' lines = get_file(file_name) - reg = re.compile(r'^([^\s]+) \([^\)]*?user: ([0-9\.]+)[^\)]*?\)\s*$', re.MULTILINE) + reg_user = re.compile(r'^([^\s]+) \([^\)]*?user: ([0-9\.]+)[^\)]*?\)\s*$', re.MULTILINE) + reg_real = re.compile(r'^([^\s]+) \([^\)]*?real: ([0-9\.]+)[^\)]*?\)\s*$', re.MULTILINE) + reg = reg_real if use_real else reg_user times = reg.findall(lines) if all(time in ('0.00', '0.01') for name, time in times): - reg = re.compile(r'^([^\s]*) \([^\)]*?real: ([0-9\.]+)[^\)]*?\)\s*$', re.MULTILINE) + reg = reg_real times = reg.findall(lines) if all(STRIP_REG.search(name.strip()) for name, time in times): times = tuple((STRIP_REG.sub(STRIP_REP, name.strip()), time) for name, time in times) return dict((name, reformat_time_string(time)) for name, time in times) -def get_single_file_times(file_name): +def get_single_file_times(file_name, use_real=False): ''' Reads the contents of file_name, which should be the output of 'coqc -time', and parses it to construct a dict mapping lines to to compile durations, as strings. ''' lines = get_file(file_name) - reg = re.compile(r'^Chars ([0-9]+) - ([0-9]+) ([^ ]+) ([0-9\.]+) secs (.*)$', re.MULTILINE) + reg = re.compile(r'^Chars ([0-9]+) - ([0-9]+) ([^ ]+) ([0-9\.]+) secs \(([0-9\.]+)u(.*)\)$', re.MULTILINE) times = reg.findall(lines) if len(times) == 0: return dict() - longest = max(max((len(start), len(stop))) for start, stop, name, time, extra in times) + longest = max(max((len(start), len(stop))) for start, stop, name, real, user, extra in times) FORMAT = 'Chars %%0%dd - %%0%dd %%s' % (longest, longest) - return dict((FORMAT % (int(start), int(stop), name), reformat_time_string(time)) for start, stop, name, time, extra in times) + return dict((FORMAT % (int(start), int(stop), name), reformat_time_string(real if use_real else user)) for start, stop, name, real, user, extra in times) + +def fuzz_merge(l1, l2, fuzz): + '''Takes two iterables of ((start, end, code), times) and a fuzz + parameter, and yields a single iterable of ((start, stop, code), + times1, times2) + + We only give both left and right if (a) the codes are the same, + (b) the number of characters (stop - start) is the same, and (c) + the difference between left and right code locations is <= fuzz. + + We keep a current guess at the overall offset, and prefer drawing + from whichever list is earliest after correcting for current + offset. + + ''' + assert(fuzz >= 0) + cur_fuzz = 0 + l1 = list(l1) + l2 = list(l2) + cur1, cur2 = None, None + while (len(l1) > 0 or cur1 is not None) and (len(l2) > 0 or cur2 is not None): + if cur1 is None: cur1 = l1.pop(0) + if cur2 is None: cur2 = l2.pop(0) + ((s1, e1, c1), t1), ((s2, e2, c2), t2) = cur1, cur2 + assert(t1 is not None) + assert(t2 is not None) + s2_adjusted, e2_adjusted = s2 + cur_fuzz, e2 + cur_fuzz + if cur1[0] == cur2[0]: + yield (cur1, cur2) + cur1, cur2 = None, None + cur_fuzz = 0 + elif c1 == c2 and e1-s1 == e2-s2 and abs(s1 - s2) <= fuzz: + yield (((s1, e1, c1), t1), ((s2, e2, c2), t2)) + cur1, cur2 = None, None + cur_fuzz = s1 - s2 + elif s1 < s2_adjusted or (s1 == s2_adjusted and e1 <= e2): + yield (((s1, e1, c1), t1), ((s1 - cur_fuzz, e1 - cur_fuzz, c1), None)) + cur1 = None + else: + yield (((s2 + cur_fuzz, e2 + cur_fuzz, c2), None), ((s2, e2, c2), t2)) + cur2 = None + if len(l1) > 0: + for i in l1: yield (i, (i[0], None)) + elif len(l2) > 0: + for i in l2: yield ((i[0], None), i) + +def adjust_fuzz(left_dict, right_dict, fuzz): + reg = re.compile(r'Chars ([0-9]+) - ([0-9]+) (.*)$') + left_dict_list = sorted(((int(s), int(e), c), v) for ((s, e, c), v) in ((reg.match(k).groups(), v) for k, v in left_dict.items())) + right_dict_list = sorted(((int(s), int(e), c), v) for ((s, e, c), v) in ((reg.match(k).groups(), v) for k, v in right_dict.items())) + merged = list(fuzz_merge(left_dict_list, right_dict_list, fuzz)) + if len(merged) == 0: + # assert that both left and right dicts are empty + assert(not left_dict) + assert(not right_dict) + return left_dict, right_dict + longest = max(max((len(str(start1)), len(str(stop1)), len(str(start2)), len(str(stop2)))) for ((start1, stop1, code1), t1), ((start2, stop2, code2), t2) in merged) + FORMAT1 = 'Chars %%0%dd - %%0%dd %%s' % (longest, longest) + FORMAT2 = 'Chars %%0%dd-%%0%dd ~ %%0%dd-%%0%dd %%s' % (longest, longest, longest, longest) + if fuzz == 0: + left_dict = dict((FORMAT1 % k, t1) for (k, t1), _ in merged if t1 is not None) + right_dict = dict((FORMAT1 % k, t2) for _, (k, t2) in merged if t2 is not None) + else: + left_dict = dict((FORMAT2 % (s1, e1, s2, e2, c1), t1) for ((s1, e1, c1), t1), ((s2, e2, c2), t2) in merged if t1 is not None) + right_dict = dict((FORMAT2 % (s1, e1, s2, e2, c1), t2) for ((s1, e1, c1), t1), ((s2, e2, c2), t2) in merged if t2 is not None) + return left_dict, right_dict def fix_sign_for_sorting(num, descending=True): return -num if descending else num diff --git a/tools/coq_dune.ml b/tools/coq_dune.ml index f62947ec67..96fb9710c7 100644 --- a/tools/coq_dune.ml +++ b/tools/coq_dune.ml @@ -213,7 +213,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" || List.nth d 0 = "user-contrib" then + if Sys.file_exists (bpath [sd; "plugin_base.dune"]) then fprintf fmt "(include plugin_base.dune)@\n"; out_install fmt d ff; List.iter (pp_dep d fmt) ff; @@ -285,8 +285,11 @@ let exec_ifile f = begin try let ic = open_in in_file in (try f ic - with _ -> eprintf "Error: exec_ifile@\n%!"; close_in ic) - with _ -> eprintf "Error: cannot open input file %s@\n%!" in_file + with exn -> + eprintf "Error: exec_ifile @[%s@]@\n%!" (Printexc.to_string exn); + close_in ic) + with _ -> + eprintf "Error: cannot open input file %s@\n%!" in_file end | _ -> eprintf "Error: wrong number of arguments@\n%!"; exit 1 diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 950c784325..a96173c057 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -31,7 +31,6 @@ let option_sort = ref false let usage () = eprintf " usage: coqdep [options] <filename>+\n"; eprintf " options:\n"; - eprintf " -c : Also print the dependencies of caml modules (=ocamldep).\n"; eprintf " -boot : For coq developers, prints dependencies over coq library files (omitted by default).\n"; eprintf " -sort : output the given file name ordered by dependencies\n"; eprintf " -noglob | -no-glob : \n"; @@ -44,8 +43,6 @@ let usage () = eprintf " -vos : also output dependencies about .vos files\n"; eprintf " -exclude-dir dir : skip subdirectories named 'dir' during -R/-Q search\n"; eprintf " -coqlib dir : set the coq standard library directory\n"; - eprintf " -suffix s : \n"; - eprintf " -slash : deprecated, no effect\n"; eprintf " -dyndep (opt|byte|both|no|var) : set how dependencies over ML modules are printed\n"; exit 1 @@ -65,8 +62,6 @@ let treat_coqproject f = iter_sourced (fun f -> treat_file None f) (all_files project) let rec parse = function - (* TODO, deprecate option -c *) - | "-c" :: ll -> option_c := true; parse ll | "-boot" :: ll -> option_boot := true; parse ll | "-sort" :: ll -> option_sort := true; parse ll | "-vos" :: ll -> write_vos := true; parse ll @@ -81,8 +76,6 @@ let rec parse = function | "-exclude-dir" :: [] -> usage () | "-coqlib" :: r :: ll -> Envars.set_user_coqlib r; parse ll | "-coqlib" :: [] -> usage () - | "-suffix" :: s :: ll -> suffixe := s ; parse ll - | "-suffix" :: [] -> usage () | "-dyndep" :: "no" :: ll -> option_dynlink := No; parse ll | "-dyndep" :: "opt" :: ll -> option_dynlink := Opt; parse ll | "-dyndep" :: "byte" :: ll -> option_dynlink := Byte; parse ll @@ -114,11 +107,7 @@ let coqdep () = (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; - List.iter (fun (f,d) -> add_mllib_known f d ".mllib") !mllibAccu; - List.iter (fun (f,suff,d) -> add_ml_known f d suff) !mlAccu; if !option_sort then begin sort (); exit 0 end; - if !option_c then mL_dependencies (); coq_dependencies (); () diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index 5ece595f13..683165f026 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -31,15 +31,12 @@ module StrListMap = Map.Make(StrList) type dynlink = Opt | Byte | Both | No | Variable -let option_c = ref false let option_noglob = ref false let option_dynlink = ref Both let option_boot = ref false let norec_dirs = ref StrSet.empty -let suffixe = ref ".vo" - type dir = string option (** [get_extension f l] checks whether [f] has one of the extensions @@ -58,18 +55,6 @@ let basename_noext filename = let fn = Filename.basename filename in try Filename.chop_extension fn with Invalid_argument _ -> fn -(** ML Files specified on the command line. In the entries: - - the first string is the basename of the file, without extension nor - directory part - - the second string of [mlAccu] is the extension (either .ml or .mlg) - - the [dir] part is the directory, with None used as the current directory -*) - -let mlAccu = ref ([] : (string * string * dir) list) -and mliAccu = ref ([] : (string * dir) list) -and mllibAccu = ref ([] : (string * dir) list) -and mlpackAccu = ref ([] : (string * dir) list) - (** Coq files specifies on the command line: - first string is the full filename, with only its extension removed - second string is the absolute version of the previous (via getcwd) @@ -125,8 +110,6 @@ let mkknown () = with Not_found -> None in add, iter, search -let add_ml_known, _, search_ml_known = mkknown () -let add_mli_known, _, search_mli_known = mkknown () let add_mllib_known, _, search_mllib_known = mkknown () let add_mlpack_known, _, search_mlpack_known = mkknown () @@ -231,64 +214,6 @@ let file_name s = function | None -> s | Some d -> d // s -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") - | None, Some mldir -> - 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") - | None, None -> "", "" - -let traite_fichier_ML md ext = - try - let chan = open_in (md ^ ext) in - let buf = Lexing.from_channel chan in - let deja_vu = ref (StrSet.singleton md) in - let a_faire = ref "" in - 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 - done - with Fin_fichier -> () - end; - close_in chan; - (!a_faire, !a_faire_opt) - with Sys_error _ -> ("","") - -let traite_fichier_modules md ext = - try - let chan = open_in (md ^ ext) in - 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 - 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 _ -> [] - | Syntax_error (i,j) -> error_cannot_parse (md^ext) (i,j) - (* Makefile's escaping rules are awful: $ is escaped by doubling and other special characters are escaped by backslash prefixing while backslashes themselves must be escaped only if part of a sequence @@ -418,10 +343,7 @@ let rec find_dependencies basename = | 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 + | None -> warning_declare f str end in List.iter decl sl @@ -449,59 +371,16 @@ let rec find_dependencies basename = with Sys_error _ -> [] (* TODO: report an error? *) -let mL_dependencies () = - List.iter - (fun (name,ext,dirname) -> - 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" - 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) - (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) - (List.rev !mliAccu); - List.iter - (fun (name,dirname) -> - let fullname = file_name name dirname in - let dep = traite_fichier_modules fullname ".mllib" in - 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) - (List.rev !mllibAccu); - List.iter - (fun (name,dirname) -> - let fullname = file_name name dirname in - let dep = traite_fichier_modules fullname ".mlpack" in - let efullname = escape fullname in - printf "%s_MLPACK_DEPENDENCIES:=%s\n" efullname (String.concat " " dep); - printf "%s.cmo:$(addsuffix .cmo,$(%s_MLPACK_DEPENDENCIES))\n" efullname efullname; - printf "%s.cmx:$(addsuffix .cmx,$(%s_MLPACK_DEPENDENCIES))\n" efullname efullname; - let efullname_capital = String.capitalize_ascii (Filename.basename efullname) in - List.iter (fun dep -> - printf "%s.cmx : FOR_PACK=-for-pack %s\n" dep efullname_capital) - dep; - printf "%!") - (List.rev !mlpackAccu) - let write_vos = ref false let coq_dependencies () = List.iter (fun (name,_) -> let ename = escape name in - let glob = if !option_noglob then "" else " "^ename^".glob" in + let glob = if !option_noglob then "" else ename^".glob " in 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.vo %s%s.v.beautified %s.required_vo: %s.v %s\n" ename glob ename ename ename + (string_of_dependency_list ".vo" deps); printf "%s.vio: %s.v %s\n" ename ename (string_of_dependency_list ".vio" deps); if !write_vos then @@ -517,10 +396,8 @@ let rec suffixes = function let add_caml_known phys_dir _ f = let basename,suff = - get_extension f [".ml";".mli";".mlg";".mllib";".mlpack"] in + get_extension f [".mllib"; ".mlpack"] in match suff with - | ".ml"|".mlg" -> add_ml_known basename (Some phys_dir) suff - | ".mli" -> add_mli_known basename (Some phys_dir) suff | ".mllib" -> add_mllib_known basename (Some phys_dir) suff | ".mlpack" -> add_mlpack_known basename (Some phys_dir) suff | _ -> () @@ -605,18 +482,15 @@ let rec treat_file old_dirname old_name = in Array.iter (treat_file (Some newdirname)) (Sys.readdir complete_name)) | S_REG -> - (match get_extension name [".v";".ml";".mli";".mlg";".mllib";".mlpack"] with - | (base,".v") -> - let name = file_name base dirname - and absname = absolute_file_name base dirname in - addQueue vAccu (name, absname) - | (base,(".ml"|".mlg" as ext)) -> addQueue mlAccu (base,ext,dirname) - | (base,".mli") -> addQueue mliAccu (base,dirname) - | (base,".mllib") -> addQueue mllibAccu (base,dirname) - | (base,".mlpack") -> addQueue mlpackAccu (base,dirname) - | _ -> ()) + (match get_extension name [".v"] with + | base,".v" -> + let name = file_name base dirname + and absname = absolute_file_name base dirname in + addQueue vAccu (name, absname) + | _ -> ()) | _ -> () +(* "[sort]" outputs `.v` files required by others *) let sort () = let seen = Hashtbl.create 97 in let rec loop file = @@ -639,7 +513,7 @@ let sort () = done with Fin_fichier -> close_in cin; - printf "%s%s " file !suffixe + printf "%s.v " file end in List.iter (fun (name,_) -> loop name) !vAccu diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli index 1820db4a1e..aca68cc780 100644 --- a/tools/coqdep_common.mli +++ b/tools/coqdep_common.mli @@ -21,11 +21,9 @@ val coqdep_warning : ('a, Format.formatter, unit, unit) format4 -> 'a val find_dir_logpath: string -> string list (** Options *) -val option_c : bool ref val option_noglob : bool ref val option_boot : bool ref val write_vos : bool ref -val suffixe : string ref type dynlink = Opt | Byte | Both | No | Variable val option_dynlink : dynlink ref @@ -36,18 +34,11 @@ type dir = string option val treat_file : dir -> string -> unit (** ML-related manipulation *) -val mlAccu : (string * string * dir) list ref -val mliAccu : (string * dir) list ref -val mllibAccu : (string * dir) list ref -val add_ml_known : string -> dir -> string -> unit -val add_mli_known : string -> dir -> string -> unit -val add_mllib_known : string -> dir -> string -> unit -val mL_dependencies : unit -> unit - val coq_dependencies : unit -> unit val add_known : bool -> string -> string list -> string -> unit val add_coqlib_known : bool -> string -> string list -> string -> unit +(* Used to locate plugins for [Declare ML Module] *) val add_caml_dir : string -> unit (** Simply add this directory and imports it, no subdirs. This is used diff --git a/tools/coqdep_lexer.mli b/tools/coqdep_lexer.mli index 018fc1b7a2..24452f203a 100644 --- a/tools/coqdep_lexer.mli +++ b/tools/coqdep_lexer.mli @@ -8,12 +8,10 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -type mL_token = Use_module of string - type qualid = string list type coq_token = - Require of qualid option * qualid list + | Require of qualid option * qualid list | Declare of string list | Load of string | AddLoadPath of string @@ -23,6 +21,3 @@ exception Fin_fichier exception Syntax_error of int * int val coq_action : Lexing.lexbuf -> coq_token -val caml_action : Lexing.lexbuf -> mL_token -val mllib_list : Lexing.lexbuf -> string list -val ocamldep_parse : Lexing.lexbuf -> string list diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll index 743da535b8..157c2b7dba 100644 --- a/tools/coqdep_lexer.mll +++ b/tools/coqdep_lexer.mll @@ -13,8 +13,6 @@ open Filename open Lexing - type mL_token = Use_module of string - type qualid = string list type coq_token = @@ -152,56 +150,6 @@ and add_loadpath_as path = parse | dot { AddLoadPath path } -and caml_action = parse - | space + - { caml_action lexbuf } - | "open" space* (caml_up_ident as id) - { Use_module (String.uncapitalize_ascii id) } - | "module" space+ caml_up_ident - { caml_action lexbuf } - | caml_low_ident { caml_action lexbuf } - | caml_up_ident - { qual_id (Lexing.lexeme lexbuf) lexbuf } - | ['0'-'9']+ - | '0' ['x' 'X'] ['0'-'9' 'A'-'F' 'a'-'f']+ - | '0' ['o' 'O'] ['0'-'7']+ - | '0' ['b' 'B'] ['0'-'1']+ - { caml_action lexbuf } - | ['0'-'9']+ ('.' ['0'-'9']*)? (['e' 'E'] ['+' '-']? ['0'-'9']+)? - { caml_action lexbuf } - | "\"" - { string lexbuf; caml_action lexbuf } - | "'" [^ '\\' '\''] "'" - { caml_action lexbuf } - | "'" '\\' ['\\' '\'' 'n' 't' 'b' 'r'] "'" - { caml_action lexbuf } - | "'" '\\' ['0'-'9'] ['0'-'9'] ['0'-'9'] "'" - { caml_action lexbuf } - | "(*" - { comment lexbuf; caml_action lexbuf } - | "#" | "&" | "&&" | "'" | "(" | ")" | "*" | "," | "?" | "->" | "." | ".." - | ".(" | ".[" | ":" | "::" | ":=" | ";" | ";;" | "<-" | "=" | "[" | "[|" - | "[<" | "]" | "_" | "{" | "|" | "||" | "|]" | ">]" | "}" | "!=" | "-" - | "-." { caml_action lexbuf } - - | ['!' '?' '~'] - ['!' '$' '%' '&' '*' '+' '-' '.' '/' ':' '<' '=' '>' '?' '@' '^' '|' '~'] * - { caml_action lexbuf } - | ['=' '<' '>' '@' '^' '|' '&' '$'] - ['!' '$' '%' '&' '*' '+' '-' '.' '/' ':' '<' '=' '>' '?' '@' '^' '|' '~'] * - { caml_action lexbuf } - | ['+' '-'] - ['!' '$' '%' '&' '*' '+' '-' '.' '/' ':' '<' '=' '>' '?' '@' '^' '|' '~'] * - { caml_action lexbuf } - | "**" - ['!' '$' '%' '&' '*' '+' '-' '.' '/' ':' '<' '=' '>' '?' '@' '^' '|' '~'] * - { caml_action lexbuf } - | ['*' '/' '%'] - ['!' '$' '%' '&' '*' '+' '-' '.' '/' ':' '<' '=' '>' '?' '@' '^' '|' '~'] * - { caml_action lexbuf } - | eof { raise Fin_fichier } - | _ { caml_action lexbuf } - and comment = parse | "(*" { comment lexbuf; comment lexbuf } @@ -218,20 +166,6 @@ and comment = parse | _ { comment lexbuf } -and string = parse - | '"' (* '"' *) - { () } - | '\\' ("\010" | "\013" | "\010\013") [' ' '\009'] * - { string lexbuf } - | '\\' ['\\' '"' 'n' 't' 'b' 'r'] (*'"'*) - { string lexbuf } - | '\\' ['0'-'9'] ['0'-'9'] ['0'-'9'] - { string lexbuf } - | eof - { raise Fin_fichier } - | _ - { string lexbuf } - and load_file = parse | '"' [^ '"']* '"' (*'"'*) { let s = lexeme lexbuf in @@ -320,20 +254,3 @@ and modules mllist = parse { syntax_error lexbuf } | _ { Declare (List.rev mllist) } - -and qual_id ml_module_name = parse - | '.' [^ '.' '(' '['] - { Use_module (String.uncapitalize_ascii ml_module_name) } - | eof { raise Fin_fichier } - | _ { caml_action lexbuf } - -and mllib_list = parse - | caml_up_ident { let s = String.uncapitalize_ascii (Lexing.lexeme lexbuf) - in s :: mllib_list lexbuf } - | "*predef*" { mllib_list lexbuf } - | space+ { mllib_list lexbuf } - | eof { [] } - | _ { syntax_error lexbuf } - -and ocamldep_parse = parse - | [^ ':' ]* ':' { mllib_list lexbuf } diff --git a/tools/dune b/tools/dune index 204bd09535..c0e4e20f72 100644 --- a/tools/dune +++ b/tools/dune @@ -29,7 +29,15 @@ (modules coqdep_lexer coqdep_common coqdep) (libraries coq.lib)) -(ocamllex coqdep_lexer) +; Bare-bones mllib/mlpack parser +(executable + (name ocamllibdep) + (public_name ocamllibdep) + (modules ocamllibdep) + (package coq) + (libraries unix)) + +(ocamllex coqdep_lexer ocamllibdep) (executable (name coqwc) diff --git a/tools/make-both-single-timing-files.py b/tools/make-both-single-timing-files.py index fddf75f39f..a28da43043 100755 --- a/tools/make-both-single-timing-files.py +++ b/tools/make-both-single-timing-files.py @@ -1,12 +1,17 @@ #!/usr/bin/env python3 -import sys from TimeFileMaker import * if __name__ == '__main__': - USAGE = 'Usage: %s [--sort-by=auto|absolute|diff] AFTER_FILE_NAME BEFORE_FILE_NAME [OUTPUT_FILE_NAME ..]' % sys.argv[0] - HELP_STRING = r'''Formats timing information from the output of two invocations of `coqc -time` into a sorted table''' - sort_by, args = parse_args(sys.argv, USAGE, HELP_STRING) - left_dict = get_single_file_times(args[1]) - right_dict = get_single_file_times(args[2]) - table = make_diff_table_string(left_dict, right_dict, tag="Code", sort_by=sort_by) - print_or_write_table(table, args[3:]) + parser = argparse.ArgumentParser(description=r'''Formats timing information from the output of two invocations of `coqc -time` into a sorted table''') + add_sort_by(parser) + add_user(parser, single_timing=True) + add_fuzz(parser) + add_after_file_name(parser) + add_before_file_name(parser) + add_output_file_name(parser) + args = parser.parse_args() + left_dict = get_single_file_times(args.AFTER_FILE_NAME, use_real=args.real) + right_dict = get_single_file_times(args.BEFORE_FILE_NAME, use_real=args.real) + left_dict, right_dict = adjust_fuzz(left_dict, right_dict, fuzz=args.fuzz) + table = make_diff_table_string(left_dict, right_dict, tag="Code", sort_by=args.sort_by) + print_or_write_table(table, args.OUTPUT_FILE_NAME) diff --git a/tools/make-both-time-files.py b/tools/make-both-time-files.py index 8937d63c2f..5d88548bba 100755 --- a/tools/make-both-time-files.py +++ b/tools/make-both-time-files.py @@ -1,16 +1,15 @@ #!/usr/bin/env python3 -import sys from TimeFileMaker import * if __name__ == '__main__': - USAGE = 'Usage: %s [--sort-by=auto|absolute|diff] AFTER_FILE_NAME BEFORE_FILE_NAME [OUTPUT_FILE_NAME ..]' % sys.argv[0] - HELP_STRING = r'''Formats timing information from the output of two invocations of `make TIMED=1` into a sorted table. - -The input is expected to contain lines in the format: -FILE_NAME (...user: NUMBER_IN_SECONDS...) -''' - sort_by, args = parse_args(sys.argv, USAGE, HELP_STRING) - left_dict = get_times(args[1]) - right_dict = get_times(args[2]) - table = make_diff_table_string(left_dict, right_dict, sort_by=sort_by) - print_or_write_table(table, args[3:]) + parser = argparse.ArgumentParser(description=r'''Formats timing information from the output of two invocations of `make TIMED=1` into a sorted table.''') + add_sort_by(parser) + add_real(parser) + add_after_file_name(parser) + add_before_file_name(parser) + add_output_file_name(parser) + args = parser.parse_args() + left_dict = get_times(args.AFTER_FILE_NAME, use_real=args.real) + right_dict = get_times(args.BEFORE_FILE_NAME, use_real=args.real) + table = make_diff_table_string(left_dict, right_dict, sort_by=args.sort_by) + print_or_write_table(table, args.OUTPUT_FILE_NAME) diff --git a/tools/make-one-time-file.py b/tools/make-one-time-file.py index ad0a04ab07..3df7d7e584 100755 --- a/tools/make-one-time-file.py +++ b/tools/make-one-time-file.py @@ -3,19 +3,11 @@ import sys from TimeFileMaker import * if __name__ == '__main__': - USAGE = 'Usage: %s FILE_NAME [OUTPUT_FILE_NAME ..]' % sys.argv[0] - HELP_STRING = r'''Formats timing information from the output of `make TIMED=1` into a sorted table. - -The input is expected to contain lines in the format: -FILE_NAME (...user: NUMBER_IN_SECONDS...) -''' - if len(sys.argv) < 2 or '--help' in sys.argv[1:] or '-h' in sys.argv[1:]: - print(USAGE) - if '--help' in sys.argv[1:] or '-h' in sys.argv[1:]: - print(HELP_STRING) - if len(sys.argv) == 2: sys.exit(0) - sys.exit(1) - else: - times_dict = get_times(sys.argv[1]) - table = make_table_string(times_dict) - print_or_write_table(table, sys.argv[2:]) + parser = argparse.ArgumentParser(description=r'''Formats timing information from the output of `make TIMED=1` into a sorted table.''') + add_real(parser) + add_file_name(parser) + add_output_file_name(parser) + args = parser.parse_args() + times_dict = get_times(args.FILE_NAME, use_real=args.real) + table = make_table_string(times_dict) + print_or_write_table(table, args.OUTPUT_FILE_NAME) diff --git a/tools/ocamllibdep.mll b/tools/ocamllibdep.mll index 41a4e2a86a..2ecc20f1b0 100644 --- a/tools/ocamllibdep.mll +++ b/tools/ocamllibdep.mll @@ -195,6 +195,14 @@ let mllib_dependencies () = flush stdout) (List.rev !mllibAccu) +let coq_makefile_mode = ref false + +let print_for_pack modname d = + if !coq_makefile_mode then + printf "%s.cmx : FOR_PACK=-for-pack %s\n" d modname + else + printf "%s_FORPACK:= -for-pack %s\n" d modname + let mlpack_dependencies () = List.iter (fun (name,dirname) -> @@ -204,7 +212,7 @@ let mlpack_dependencies () = let sdeps = String.concat " " deps in let efullname = escape fullname in printf "%s_MLPACK_DEPENDENCIES:=%s\n" efullname sdeps; - List.iter (fun d -> printf "%s_FORPACK:= -for-pack %s\n" d modname) deps; + List.iter (print_for_pack modname) deps; printf "%s.cmo:$(addsuffix .cmo,$(%s_MLPACK_DEPENDENCIES))\n" efullname efullname; printf "%s.cmx:$(addsuffix .cmx,$(%s_MLPACK_DEPENDENCIES))\n" @@ -213,6 +221,7 @@ let mlpack_dependencies () = (List.rev !mlpackAccu) let rec parse = function + | "-c" :: r -> coq_makefile_mode := true; parse r | "-I" :: r :: ll -> (* To solve conflict (e.g. same filename in kernel and checker) we allow to state an explicit order *) |