diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/CoqMakefile.in | 29 | ||||
| -rw-r--r-- | tools/TimeFileMaker.py | 257 | ||||
| -rw-r--r-- | tools/coq_dune.ml | 301 | ||||
| -rw-r--r-- | tools/coqdoc/coqdoc.css | 9 | ||||
| -rw-r--r-- | tools/coqdoc/coqdoc.sty | 1 | ||||
| -rw-r--r-- | tools/coqdoc/cpretty.mll | 239 | ||||
| -rw-r--r-- | tools/coqdoc/index.ml | 3 | ||||
| -rw-r--r-- | tools/coqdoc/index.mli | 1 | ||||
| -rw-r--r-- | tools/coqdoc/output.ml | 37 | ||||
| -rw-r--r-- | tools/coqdoc/output.mli | 3 | ||||
| -rw-r--r-- | tools/dune | 6 | ||||
| -rwxr-xr-x | tools/make-both-time-files.py | 8 | ||||
| -rwxr-xr-x | tools/make-one-time-file.py | 6 |
13 files changed, 431 insertions, 469 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index b8e498898b..57ba036a62 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -54,7 +54,7 @@ OCAMLWARN := $(COQMF_WARN) # # Parameters are make variable assignments. # They can be passed to (each call to) make on the command line. -# They can also be put in @LOCAL_FILE@ once an for all. +# They can also be put in @LOCAL_FILE@ once and for all. # For retro-compatibility reasons they can be put in the _CoqProject, but this # practice is discouraged since _CoqProject better not contain make specific # code (be nice to user interfaces). @@ -66,12 +66,12 @@ VERBOSE ?= TIMED?= TIMECMD?= # Use command time on linux, gtime on Mac OS -TIMEFMT?="$* (real: %e, user: %U, sys: %S, mem: %M ko)" +TIMEFMT?="$@ (real: %e, user: %U, sys: %S, mem: %M ko)" ifneq (,$(TIMED)) -ifeq (0,$(shell command time -f $(TIMEFMT) true >/dev/null 2>/dev/null; echo $$?)) +ifeq (0,$(shell command time -f "" true >/dev/null 2>/dev/null; echo $$?)) STDTIME?=command time -f $(TIMEFMT) else -ifeq (0,$(shell gtime -f $(TIMEFMT) true >/dev/null 2>/dev/null; echo $$?)) +ifeq (0,$(shell gtime -f "" true >/dev/null 2>/dev/null; echo $$?)) STDTIME?=gtime -f $(TIMEFMT) else STDTIME?=command time @@ -132,6 +132,10 @@ TIMING_SORT_BY ?= auto TIMING_FUZZ ?= 0 # Option for changing whether to use real or user time for timing tables TIMING_REAL?= +# Option for including the memory column(s) +TIMING_INCLUDE_MEM?= +# Option for sorting by the memory column +TIMING_SORT_BY_MEM?= # Output file names for timed builds TIME_OF_BUILD_FILE ?= time-of-build.log TIME_OF_BUILD_BEFORE_FILE ?= time-of-build-before.log @@ -355,6 +359,18 @@ TIMING_USER_ARG := endif endif +ifeq (0,$(TIMING_INCLUDE_MEM)) +TIMING_INCLUDE_MEM_ARG := --no-include-mem +else +TIMING_INCLUDE_MEM_ARG := +endif + +ifeq (1,$(TIMING_SORT_BY_MEM)) +TIMING_SORT_BY_MEM_ARG := --sort-by-mem +else +TIMING_SORT_BY_MEM_ARG := +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:: @@ -362,9 +378,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) $(TIMING_REAL_ARG) $(TIME_OF_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) + $(HIDE)$(COQMAKE_ONE_TIME_FILE) $(TIMING_INCLUDE_MEM_ARG) $(TIMING_SORT_BY_MEM_ARG) $(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) $(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) + $(HIDE)$(COQMAKE_BOTH_TIME_FILES) --sort-by=$(TIMING_SORT_BY) $(TIMING_INCLUDE_MEM_ARG) $(TIMING_SORT_BY_MEM_ARG) $(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' @@ -616,6 +632,7 @@ cleanall:: clean $(HIDE)rm -f $(VOFILES:.vo=.v.before-timing) $(HIDE)rm -f $(VOFILES:.vo=.v.after-timing) $(HIDE)rm -f $(VOFILES:.vo=.v.timing.diff) + $(HIDE)rm -f .lia.cache .nia.cache .PHONY: cleanall archclean:: diff --git a/tools/TimeFileMaker.py b/tools/TimeFileMaker.py index 210901f8a7..c4620f5b50 100644 --- a/tools/TimeFileMaker.py +++ b/tools/TimeFileMaker.py @@ -15,6 +15,9 @@ STRIP_REG = re.compile('^(coq/|contrib/|)(?:theories/|src/)?') STRIP_REP = r'\1' INFINITY = '\u221e' +TIME_KEY = 'time' +MEM_KEY = 'mem' + def nonnegative(arg): v = int(arg) if v < 0: raise argparse.ArgumentTypeError("%s is an invalid non-negative int value" % arg) @@ -37,6 +40,11 @@ def add_sort_by(parser): 'The "absolute" method sorts by the total time taken.\n' + 'The "diff" method sorts by the signed difference in time.')) +def add_sort_by_mem(parser): + return parser.add_argument( + '--sort-by-mem', action='store_true', dest='sort_by_mem', + help=('Sort the table entries by memory rather than time.')) + def add_fuzz(parser): return parser.add_argument( '--fuzz', dest='fuzz', metavar='N', type=nonnegative, default=0, @@ -55,9 +63,9 @@ def add_real(parser, single_timing=False): 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...) +FILE_NAME (...user: NUMBER_IN_SECONDS...mem: NUMBER ko...) If --real is passed, then the lines are instead expected in the format: -FILE_NAME (...real: NUMBER_IN_SECONDS...)''' if not single_timing else +FILE_NAME (...real: NUMBER_IN_SECONDS...mem: NUMBER ko...)''' if not single_timing else '''The input is expected to contain lines in the format: Chars START - END COMMAND NUMBER secs (NUMBERu...)'''))) @@ -67,12 +75,17 @@ def add_user(parser, single_timing=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...) +FILE_NAME (...real: NUMBER_IN_SECONDS...mem: NUMBER ko...) If --user is passed, then the lines are instead expected in the format: -FILE_NAME (...user: NUMBER_IN_SECONDS...)''' if not single_timing else +FILE_NAME (...user: NUMBER_IN_SECONDS...mem: NUMBER ko...)''' if not single_timing else '''The input is expected to contain lines in the format: Chars START - END COMMAND NUMBER secs (NUMBERu...)'''))) +def add_include_mem(parser): + return parser.add_argument( + '--no-include-mem', dest='include_mem', default=True, action='store_false', + help=(r'''Don't include memory in the table.''')) + # 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) @@ -113,14 +126,24 @@ def get_file_lines(file_name): def get_file(file_name): return ''.join(get_file_lines(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 - names to compile durations, as strings. Removes common prefixes - using STRIP_REG and STRIP_REP. - ''' - lines = get_file(file_name) +def merge_dicts(d1, d2): + if d2 is None: return d1 + if d1 is None: return d2 + assert(isinstance(d1, dict)) + assert(isinstance(d2, dict)) + ret = {} + for k in set(list(d1.keys()) + list(d2.keys())): + ret[k] = merge_dicts(d1.get(k), d2.get(k)) + return ret + +def get_mems_of_lines(lines): + reg = re.compile(r'^([^\s]+) \([^\)]*?mem: ([0-9]+) ko[^\)]*?\)\s*$', re.MULTILINE) + mems = reg.findall(lines) + if all(STRIP_REG.search(name.strip()) for name, mem in mems): + mems = tuple((STRIP_REG.sub(STRIP_REP, name.strip()), mem) for name, mem in mems) + return dict((name, {MEM_KEY:int(mem)}) for name, mem in mems) + +def get_times_of_lines(lines, use_real=False): 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 @@ -130,7 +153,31 @@ def get_times(file_name, use_real=False): 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) + return dict((name, {TIME_KEY:reformat_time_string(time)}) for name, time in times) + +def get_times_and_mems(file_name, use_real=False, include_mem=True): + # we only get the file once, in case it is a stream like stdin + lines = get_file(file_name) + return merge_dicts(get_times_of_lines(lines, use_real=use_real), + (get_mems_of_lines(lines) if include_mem else None)) + +def get_mems(file_name): + ''' + Reads the contents of file_name, which should be the output of + 'make TIMED=1', and parses it to construct a dict mapping file + names to peak memory usage, as integers. Removes common prefixes + using STRIP_REG and STRIP_REP. + ''' + return get_mems_of_lines(get_file(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 + names to compile durations, as strings. Removes common prefixes + using STRIP_REG and STRIP_REP. + ''' + return get_times_of_lines(get_file(file_name)) def get_single_file_times(file_name, use_real=False): ''' @@ -144,7 +191,7 @@ def get_single_file_times(file_name, use_real=False): if len(times) == 0: return dict() 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(real if use_real else user)) for start, stop, name, real, user, extra in times) + return dict((FORMAT % (int(start), int(stop), name), {TIME_KEY: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 @@ -215,20 +262,30 @@ def adjust_fuzz(left_dict, right_dict, fuzz): def fix_sign_for_sorting(num, descending=True): return -num if descending else num -def make_sorting_key(times_dict, descending=True): - def get_key(name): - minutes, seconds = times_dict[name].replace('s', '').split('m') - return (fix_sign_for_sorting(int(minutes), descending=descending), - fix_sign_for_sorting(float(seconds), descending=descending), - name) +def make_sorting_key(stats_dict, descending=True, sort_by_mem=False): + if sort_by_mem: + def get_key(name): + if MEM_KEY not in stats_dict[name].keys(): + print('WARNING: %s has no mem key: %s' % (name, repr(stats_dict[name])), file=sys.stderr) + mem = stats_dict[name].get(MEM_KEY, '0') + return (fix_sign_for_sorting(int(mem), descending=descending), + name) + else: + def get_key(name): + if TIME_KEY not in stats_dict[name].keys(): + print('WARNING: %s has no time key: %s' % (name, repr(stats_dict[name])), file=sys.stderr) + minutes, seconds = stats_dict[name].get(TIME_KEY, '0m00s').replace('s', '').split('m') + return (fix_sign_for_sorting(int(minutes), descending=descending), + fix_sign_for_sorting(float(seconds), descending=descending), + name) return get_key -def get_sorted_file_list_from_times_dict(times_dict, descending=True): +def get_sorted_file_list_from_stats_dict(stats_dict, descending=True, sort_by_mem=False): ''' Takes the output dict of get_times and returns the list of keys, sorted by duration. ''' - return sorted(times_dict.keys(), key=make_sorting_key(times_dict, descending=descending)) + return sorted(stats_dict.keys(), key=make_sorting_key(stats_dict, descending=descending, sort_by_mem=sort_by_mem)) def to_seconds(time): ''' @@ -265,85 +322,149 @@ def format_percentage(num, signed=True): frac_part = int(100 * (num * 100 - whole_part)) return sign + '%d.%02d%%' % (whole_part, frac_part) -def make_diff_table_string(left_times_dict, right_times_dict, +def make_diff_table_string(left_dict, right_dict, sort_by='auto', - descending=True, - left_tag="After", tag="File Name", right_tag="Before", with_percent=True, - change_tag="Change", percent_change_tag="% Change"): + descending=True, sort_by_mem=False, + left_tag='After', tag='File Name', right_tag='Before', with_percent=True, + left_mem_tag='Peak Mem', right_mem_tag='Peak Mem', + include_mem=False, + change_tag='Change', percent_change_tag='% Change', + change_mem_tag='Change (mem)', percent_change_mem_tag='% Change (mem)', + mem_fmt='%d ko'): # We first get the names of all of the compiled files: all files # that were compiled either before or after. all_names_dict = dict() - all_names_dict.update(right_times_dict) - all_names_dict.update(left_times_dict) # do the left (after) last, so that we give precedence to those ones + all_names_dict.update(right_dict) + all_names_dict.update(left_dict) # do the left (after) last, so that we give precedence to those ones if len(all_names_dict.keys()) == 0: return 'No timing data' - prediff_times = tuple((name, to_seconds(left_times_dict.get(name,'0m0.0s')), to_seconds(right_times_dict.get(name,'0m0.0s'))) + get_time = (lambda d, name: to_seconds(d.get(name, {}).get(TIME_KEY, '0m0.0s'))) + prediff_times = tuple((name, get_time(left_dict, name), get_time(right_dict, name)) for name in all_names_dict.keys()) diff_times_dict = dict((name, from_seconds(lseconds - rseconds, signed=True)) for name, lseconds, rseconds in prediff_times) percent_diff_times_dict = dict((name, ((format_percentage((lseconds - rseconds) / rseconds)) if rseconds != 0 else (INFINITY if lseconds > 0 else 'N/A'))) for name, lseconds, rseconds in prediff_times) + + get_mem = (lambda d, name: d.get(name, {}).get(MEM_KEY, 0)) + prediff_mems = tuple((name, get_mem(left_dict, name), get_mem(right_dict, name)) + for name in all_names_dict.keys()) + diff_mems_dict = dict((name, lmem - rmem) for name, lmem, rmem in prediff_mems) + percent_diff_mems_dict = dict((name, ((format_percentage((lmem - rmem) / float(rmem))) + if rmem != 0 else (INFINITY if lmem > 0 else 'N/A'))) + for name, lmem, rmem in prediff_mems) + # update to sort by approximate difference, first - get_key_abs = make_sorting_key(all_names_dict, descending=descending) - get_key_diff_float = (lambda name: fix_sign_for_sorting(to_seconds(diff_times_dict[name]), descending=descending)) - get_key_diff_absint = (lambda name: fix_sign_for_sorting(int(abs(to_seconds(diff_times_dict[name]))), descending=descending)) + if sort_by_mem: + get_prekey = (lambda name: diff_mems_dict[name]) + else: + get_prekey = (lambda name: to_seconds(diff_times_dict[name])) + get_key_abs = make_sorting_key(all_names_dict, descending=descending, sort_by_mem=sort_by_mem) + get_key_diff_float = (lambda name: fix_sign_for_sorting(get_prekey(name), descending=descending)) + get_key_diff_absint = (lambda name: fix_sign_for_sorting(int(abs(get_prekey(name))), descending=descending)) + get_key_with_name = (lambda get_key: lambda name: (get_key(name), name)) if sort_by == 'absolute': - get_key = get_key_abs + get_key = get_key_with_name(get_key_abs) elif sort_by == 'diff': - get_key = get_key_diff_float + get_key = get_key_with_name(get_key_diff_float) else: # sort_by == 'auto' - get_key = (lambda name: (get_key_diff_absint(name), get_key_abs(name))) + get_key = get_key_with_name((lambda name: (get_key_diff_absint(name), get_key_abs(name)))) names = sorted(all_names_dict.keys(), key=get_key) - #names = get_sorted_file_list_from_times_dict(all_names_dict, descending=descending) + #names = get_sorted_file_list_from_stats_dict(all_names_dict, descending=descending) # set the widths of each of the columns by the longest thing to go in that column - left_sum = sum_times(left_times_dict.values()) - right_sum = sum_times(right_times_dict.values()) - left_sum_float = sum(sorted(map(to_seconds, left_times_dict.values()))) - right_sum_float = sum(sorted(map(to_seconds, right_times_dict.values()))) + left_sum = sum_times(v[TIME_KEY] for v in left_dict.values() if TIME_KEY in v.keys()) + right_sum = sum_times(v[TIME_KEY] for v in right_dict.values() if TIME_KEY in v.keys()) + left_sum_float = sum(sorted(to_seconds(v[TIME_KEY]) for v in left_dict.values() if TIME_KEY in v.keys())) + right_sum_float = sum(sorted(to_seconds(v[TIME_KEY]) for v in right_dict.values() if TIME_KEY in v.keys())) diff_sum = from_seconds(left_sum_float - right_sum_float, signed=True) percent_diff_sum = (format_percentage((left_sum_float - right_sum_float) / right_sum_float) if right_sum_float > 0 else 'N/A') - left_width = max(max(map(len, ['N/A'] + list(left_times_dict.values()))), len(left_sum)) - right_width = max(max(map(len, ['N/A'] + list(right_times_dict.values()))), len(right_sum)) + + left_width = max(max(map(len, ['N/A', left_tag] + [v[TIME_KEY] for v in left_dict.values() if TIME_KEY in v.keys()])), len(left_sum)) + right_width = max(max(map(len, ['N/A', right_tag] + [v[TIME_KEY] for v in right_dict.values() if TIME_KEY in v.keys()])), len(right_sum)) far_right_width = max(max(map(len, ['N/A', change_tag] + list(diff_times_dict.values()))), len(diff_sum)) far_far_right_width = max(max(map(len, ['N/A', percent_change_tag] + list(percent_diff_times_dict.values()))), len(percent_diff_sum)) - middle_width = max(map(len, names + [tag, "Total"])) - format_string = ("%%(left)-%ds | %%(middle)-%ds | %%(right)-%ds || %%(far_right)-%ds" - % (left_width, middle_width, right_width, far_right_width)) + total_string = 'Total' if not include_mem else 'Total Time / Peak Mem' + middle_width = max(map(len, names + [tag, total_string])) + + left_peak = max(v.get(MEM_KEY, 0) for v in left_dict.values()) + right_peak = max(v.get(MEM_KEY, 0) for v in right_dict.values()) + diff_peak = left_peak - right_peak + percent_diff_peak = (format_percentage((left_peak - right_peak) / float(right_peak)) + if right_peak != 0 else (INFINITY if left_peak > 0 else 'N/A')) + + left_mem_width = max(max(map(len, ['N/A', left_mem_tag] + [mem_fmt % v.get(MEM_KEY, 0) for v in left_dict.values()])), len(mem_fmt % left_peak)) + right_mem_width = max(max(map(len, ['N/A', right_mem_tag] + [mem_fmt % v.get(MEM_KEY, 0) for v in right_dict.values()])), len(mem_fmt % right_peak)) + far_right_mem_width = max(max(map(len, ['N/A', change_mem_tag] + [mem_fmt % v for v in diff_mems_dict.values()])), len(mem_fmt % diff_peak)) + far_far_right_mem_width = max(max(map(len, ['N/A', percent_change_mem_tag] + list(percent_diff_mems_dict.values()))), len(percent_diff_peak)) + + if include_mem: + format_string = ("%%(left)%ds | %%(left_mem)%ds | %%(middle)-%ds | %%(right)%ds | %%(right_mem)%ds || %%(far_right)%ds || %%(far_right_mem)%ds" + % (left_width, left_mem_width, middle_width, right_width, right_mem_width, far_right_width, far_right_mem_width)) + else: + format_string = ("%%(left)%ds | %%(middle)-%ds | %%(right)%ds || %%(far_right)%ds" + % (left_width, middle_width, right_width, far_right_width)) + if with_percent: - format_string += " | %%(far_far_right)-%ds" % far_far_right_width - header = format_string % {'left': left_tag, 'middle': tag, 'right': right_tag, 'far_right': change_tag, 'far_far_right': percent_change_tag} - total = format_string % {'left': left_sum, 'middle': "Total", 'right': right_sum, 'far_right': diff_sum, 'far_far_right': percent_diff_sum} + format_string += " | %%(far_far_right)%ds" % far_far_right_width + if include_mem: + format_string += " | %%(far_far_right_mem)%ds" % far_far_right_mem_width + + header = format_string % {'left': left_tag, 'left_mem': left_mem_tag, + 'middle': tag, + 'right': right_tag, 'right_mem': right_mem_tag, + 'far_right': change_tag, 'far_right_mem': change_mem_tag, + 'far_far_right': percent_change_tag, 'far_far_right_mem': percent_change_mem_tag} + total = format_string % {'left': left_sum, 'left_mem': mem_fmt % left_peak, + 'middle': total_string, + 'right': right_sum, 'right_mem': mem_fmt % right_peak, + 'far_right': diff_sum, 'far_right_mem': mem_fmt % diff_peak, + 'far_far_right': percent_diff_sum, 'far_far_right_mem': percent_diff_peak} # separator to go between headers and body sep = '-' * len(header) # the representation of the default value (0), to get replaced by N/A - left_rep, right_rep, far_right_rep, far_far_right_rep = ("%%-%ds | " % left_width) % 0, (" | %%-%ds || " % right_width) % 0, ("|| %%-%ds" % far_right_width) % 0, ("| %%-%ds" % far_far_right_width) % 0 + left_rep, right_rep, far_right_rep, far_far_right_rep = ("%%%ds | " % left_width) % 'N/A', (" | %%%ds |" % right_width) % 'N/A', ("|| %%%ds" % far_right_width) % 'N/A', ("| %%%ds" % far_far_right_width) % 'N/A' + left_mem_rep, right_mem_rep, far_right_mem_rep, far_far_right_mem_rep = ("%%%ds | " % left_mem_width) % 'N/A', (" | %%%ds |" % right_mem_width) % 'N/A', ("|| %%%ds" % far_right_mem_width) % 'N/A', ("| %%%ds" % far_far_right_mem_width) % 'N/A' + get_formatted_mem = (lambda k, v: (mem_fmt % v[k]) if k in v.keys() else 'N/A') return '\n'.join([header, sep, total, sep] + - [format_string % {'left': left_times_dict.get(name, 0), + [format_string % {'left': left_dict.get(name, {}).get(TIME_KEY, 'N/A'), + 'left_mem': get_formatted_mem(MEM_KEY, left_dict.get(name, {})), 'middle': name, - 'right': right_times_dict.get(name, 0), - 'far_right': diff_times_dict.get(name, 0), - 'far_far_right': percent_diff_times_dict.get(name, 0)} - for name in names]).replace(left_rep, 'N/A'.center(len(left_rep) - 3) + ' | ').replace(right_rep, ' | ' + 'N/A'.center(len(right_rep) - 7) + ' || ').replace(far_right_rep, '|| ' + 'N/A'.center(len(far_right_rep) - 3)).replace(far_far_right_rep, '| ' + 'N/A'.center(len(far_far_right_rep) - 2)) - -def make_table_string(times_dict, - descending=True, - tag="Time"): - if len(times_dict.keys()) == 0: return 'No timing data' + 'right': right_dict.get(name, {}).get(TIME_KEY, 'N/A'), + 'right_mem': get_formatted_mem(MEM_KEY, right_dict.get(name, {})), + 'far_right': diff_times_dict.get(name, 'N/A'), + 'far_right_mem': get_formatted_mem(name, diff_mems_dict), + 'far_far_right': percent_diff_times_dict.get(name, 'N/A'), + 'far_far_right_mem': percent_diff_mems_dict.get(name, 'N/A')} + for name in names]).replace(left_rep, 'N/A'.center(len(left_rep) - 3) + ' | ').replace(right_rep, ' | ' + 'N/A'.center(len(right_rep) - 5) + ' |').replace(far_right_rep, '|| ' + 'N/A'.center(len(far_right_rep) - 3)).replace(far_far_right_rep, '| ' + 'N/A'.center(len(far_far_right_rep) - 2)).replace(left_mem_rep, 'N/A'.center(len(left_mem_rep) - 3) + ' | ').replace(right_mem_rep, ' | ' + 'N/A'.center(len(right_mem_rep) - 5) + ' |').replace(far_right_mem_rep, '|| ' + 'N/A'.center(len(far_right_mem_rep) - 3)).replace(far_far_right_mem_rep, '| ' + 'N/A'.center(len(far_far_right_mem_rep) - 2)) + +def make_table_string(stats_dict, + descending=True, sort_by_mem=False, + tag="Time", mem_tag="Peak Mem", mem_fmt='%d ko', + include_mem=False): + if len(stats_dict.keys()) == 0: return 'No timing data' # We first get the names of all of the compiled files, sorted by # duration - names = get_sorted_file_list_from_times_dict(times_dict, descending=descending) + names = get_sorted_file_list_from_stats_dict(stats_dict, descending=descending, sort_by_mem=sort_by_mem) # compute the widths of the columns - times_width = max(max(map(len, times_dict.values())), len(sum_times(times_dict.values()))) - names_width = max(map(len, names + ["File Name", "Total"])) - format_string = "%%-%ds | %%-%ds" % (times_width, names_width) - header = format_string % (tag, "File Name") - total = format_string % (sum_times(times_dict.values()), - "Total") + times_width = max(len('N/A'), len(tag), max(len(v[TIME_KEY]) for v in stats_dict.values() if TIME_KEY in v.keys()), len(sum_times(v[TIME_KEY] for v in stats_dict.values() if TIME_KEY in v.keys()))) + mems_width = max(len('N/A'), len(mem_tag), max(len(mem_fmt % v.get(MEM_KEY, 0)) for v in stats_dict.values()), len(mem_fmt % (max(v.get(MEM_KEY, 0) for v in stats_dict.values())))) + total_string = 'Total' if not include_mem else 'Total Time / Peak Mem' + names_width = max(map(len, names + ["File Name", total_string])) + if include_mem: + format_string = "%%(time)%ds | %%(mem)%ds | %%(name)-%ds" % (times_width, mems_width, names_width) + else: + format_string = "%%(time)%ds | %%(name)-%ds" % (times_width, names_width) + get_formatted_mem = (lambda k, v: (mem_fmt % v[k]) if k in v.keys() else 'N/A') + header = format_string % {'time': tag, 'mem': mem_tag, 'name': 'File Name'} + total = format_string % {'time': sum_times(v[TIME_KEY] for v in stats_dict.values() if TIME_KEY in v.keys()), + 'mem': ((mem_fmt % max(v[MEM_KEY] for v in stats_dict.values() if MEM_KEY in v.keys())) if any(MEM_KEY in v.keys() for v in stats_dict.values()) else 'N/A'), + 'name': total_string} sep = '-' * len(header) return '\n'.join([header, sep, total, sep] + - [format_string % (times_dict[name], - name) + [format_string % {'time': stats_dict[name].get(TIME_KEY, 'N/A'), + 'mem': get_formatted_mem(MEM_KEY, stats_dict[name]), + 'name': name} for name in names]) def print_or_write_table(table, files): diff --git a/tools/coq_dune.ml b/tools/coq_dune.ml deleted file mode 100644 index 472e6b4948..0000000000 --- a/tools/coq_dune.ml +++ /dev/null @@ -1,301 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* <O___,, * (see version control and CREDITS file for authors & dates) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -(* LICENSE NOTE: This file is dually MIT/LGPL 2.1+ licensed. MIT license: - * - * Permission is hereby granted, free of charge, to any person obtaining a copy - * of this software and associated documentation files (the "Software"), to deal - * in the Software without restriction, including without limitation the rights - * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell - * copies of the Software, and to permit persons to whom the Software is - * furnished to do so, subject to the following conditions: - * - * The above copyright notice and this permission notice shall be included in all - * copies or substantial portions of the Software. - * - * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR - * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, - * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE - * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER - * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, - * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE - * SOFTWARE. - *) - -(* coq_dune: generate dune build rules for .vo files *) -(* *) -(* At some point this file will become a Dune plugin, so it is very *) -(* important that this file can be bootstrapped with: *) -(* *) -(* ocamlfind ocamlopt -linkpkg -package str coq_dune.ml -o coq_dune *) - -open Format - -(* Keeping this file self-contained as it is a "bootstrap" utility *) -(* Is OCaml missing these basic functions in the stdlib? *) -module Aux = struct - - let option_iter f o = match o with - | Some x -> f x - | None -> () - - let option_cata d f o = match o with - | Some x -> f x - | None -> d - - let list_compare f = let rec lc x y = match x, y with - | [], [] -> 0 - | [], _ -> -1 - | _, [] -> 1 - | x::xs, y::ys -> let r = f x y in if r = 0 then lc xs ys else r - in lc - - let rec pp_list pp sep fmt l = match l with - | [] -> () - | [l] -> fprintf fmt "%a" pp l - | x::xs -> fprintf fmt "%a%a%a" pp x sep () (pp_list pp sep) xs - - let rec pmap f l = match l with - | [] -> [] - | x :: xs -> - begin match f x with - | None -> pmap f xs - | Some r -> r :: pmap f xs - end - - let sep fmt () = fprintf fmt "@;" - - (* Creation of paths, aware of the platform separator. *) - let bpath l = String.concat Filename.dir_sep l - - module DirOrd = struct - type t = string list - let compare = list_compare String.compare - end - - module DirMap = Map.Make(DirOrd) - - (* Functions available in newer OCaml versions *) - (* Taken from the OCaml std library (c) INRIA / LGPL-2.1 *) - module Legacy = struct - - - (* Fix once we move to OCaml >= 4.06.0 *) - let list_init len f = - let rec init_aux i n f = - if i >= n then [] - else let r = f i in r :: init_aux (i+1) n f - in init_aux 0 len f - - (* Slower version of DirMap.update, waiting for OCaml 4.06.0 *) - let dirmap_update key f map = - match begin - try f (Some (DirMap.find key map)) - with Not_found -> f None - end with - | None -> DirMap.remove key map - | Some x -> DirMap.add key x map - - end - - let add_map_list key elem map = - (* Move to Dirmap.update once we require OCaml >= 4.06.0 *) - Legacy.dirmap_update key (fun l -> Some (option_cata [elem] (fun ll -> elem :: ll) l)) map - - let replace_ext ~file ~newext = - Filename.(remove_extension file) ^ newext - -end - -open Aux - -(* Once this is a Dune plugin the flags will be taken from the env *) -module Options = struct - - type flag = { - enabled : bool; - cmd : string; - } - - let all_opts = - [ { enabled = false; cmd = "-debug"; } - ; { enabled = false; cmd = "-native_compiler"; } - ; { enabled = true; cmd = "-w +default"; } - ] - - let build_coq_flags () = - let popt o = if o.enabled then Some o.cmd else None in - String.concat " " @@ pmap popt all_opts -end - -type vodep = { - target: string; - deps : string list; -} - -type ldep = | VO of vodep | MLG of string -type ddir = ldep list DirMap.t - -(* Filter `.vio` etc... *) -let filter_no_vo = - List.filter (fun f -> Filename.check_suffix f ".vo") - -(* We could have coqdep to output dune files directly *) - -let gen_sub n = - (* Move to List.init once we can depend on OCaml >= 4.06.0 *) - bpath @@ Legacy.list_init n (fun _ -> "..") - -let pp_rule fmt targets deps action = - (* Special printing of the first rule *) - let ppl = pp_list pp_print_string sep in - let pp_deps fmt l = match l with - | [] -> - () - | x :: xs -> - fprintf fmt "(:pp-file %s)%a" x sep (); - pp_list pp_print_string sep fmt xs - in - fprintf fmt - "@[(rule@\n @[(targets @[%a@])@\n(deps @[%a@])@\n(action @[%a@])@])@]@\n" - ppl targets pp_deps deps pp_print_string action - -let gen_coqc_targets vo = - [ vo.target - ; replace_ext ~file:vo.target ~newext:".glob" - ; replace_ext ~file:vo.target ~newext:".vos" - ; "." ^ replace_ext ~file:vo.target ~newext:".aux"] - -(* Generate the dune rule: *) -let pp_vo_dep dir fmt vo = - let depth = List.length dir in - let sdir = gen_sub depth in - (* All files except those in Init implicitly depend on the Prelude, we account for it here. *) - let eflag, edep = if List.tl dir = ["Init"] then "-noinit -R theories Coq", [] else "", [bpath ["theories";"Init";"Prelude.vo"]] in - (* Coq flags *) - let cflag = Options.build_coq_flags () in - (* Correct path from global to local "theories/Init/Decimal.vo" -> "../../theories/Init/Decimal.vo" *) - let deps = List.map (fun s -> bpath [sdir;s]) (edep @ vo.deps) in - (* The source file is also corrected as we will call coqtop from the top dir *) - let source = bpath (dir @ [replace_ext ~file:vo.target ~newext:".v"]) in - (* We explicitly include the location of coqlib to avoid tricky issues with coqlib location *) - let libflag = "-coqlib %{project_root}" in - (* The final build rule *) - let action = sprintf "(chdir %%{project_root} (run coqc -q %s %s %s %s))" libflag eflag cflag source in - let all_targets = gen_coqc_targets vo in - pp_rule fmt all_targets deps action - -let pp_mlg_dep _dir fmt ml = - fprintf fmt "@[(coq.pp (modules %s))@]@\n" (Filename.remove_extension ml) - -let pp_dep dir fmt oo = match oo with - | VO vo -> pp_vo_dep dir fmt vo - | MLG f -> pp_mlg_dep dir fmt f - -let out_install fmt dir ff = - let itarget = String.concat "/" dir in - let ff = List.concat @@ pmap (function | VO vo -> Some (gen_coqc_targets vo) | _ -> None) ff in - let pp_ispec fmt tg = fprintf fmt "(%s as coq/%s)" tg (bpath [itarget;tg]) in - fprintf fmt "(install@\n @[(section lib_root)@\n(package coq)@\n(files @[%a@])@])@\n" - (pp_list pp_ispec sep) ff - -(* For each directory, we must record two things, the build rules and - the install specification. *) -let record_dune d ff = - let sd = bpath d in - 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 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; - fprintf fmt "%!"; - close_out out - else - eprintf "error in coq_dune, a directory disappeared: %s@\n%!" sd - -(* File Scanning *) -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 [root; d] (MLG f) m) m mlg - -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 [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 = - if String.equal Filename.(extension file) ".cmo" - then replace_ext ~file ~newext:".cma" - else file - -(* Process .vfiles.d and generate a skeleton for the dune file *) -let parse_coqdep_line l = - match Str.(split (regexp ":") l) with - | [targets;deps] -> - let targets = Str.(split (regexp "[ \t]+") targets) in - let deps = Str.(split (regexp "[ \t]+") deps) in - let targets = filter_no_vo targets in - begin match targets with - | [target] -> - let dir, target = Filename.(dirname target, basename target) in - (* coqdep outputs with the '/' directory separator regardless of - the platform. Anyways, I hope we can link to coqdep instead - of having to parse its output soon, that should solve this - kind of issues *) - let deps = List.map fix_cmo_cma deps in - Some (String.split_on_char '/' dir, VO { target; deps; }) - (* Otherwise a vio file, we ignore *) - | _ -> None - end - (* Strange rule, we ignore *) - | _ -> None - -let rec read_vfiles ic map = - try - let rule = parse_coqdep_line (input_line ic) in - (* Add vo_entry to its corresponding map entry *) - let map = option_cata map (fun (dir, vo) -> add_map_list dir vo map) rule in - read_vfiles ic map - with End_of_file -> map - -let out_map map = - DirMap.iter record_dune map - -let exec_ifile f = - match Array.length Sys.argv with - | 1 -> f stdin - | 2 -> - let in_file = Sys.argv.(1) in - begin try - let ic = open_in in_file in - (try f ic - 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 - -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/coqdoc/coqdoc.css b/tools/coqdoc/coqdoc.css index dbc930f5ec..48096e555a 100644 --- a/tools/coqdoc/coqdoc.css +++ b/tools/coqdoc/coqdoc.css @@ -230,6 +230,10 @@ tr.infrulemiddle hr { color: rgb(40%,0%,40%); } +.id[title="binder"] { + color: rgb(40%,0%,40%); +} + .id[type="definition"] { color: rgb(0%,40%,0%); } @@ -327,3 +331,8 @@ ul.doclist { margin-top: 0em; margin-bottom: 0em; } + +.code :target { + border: 2px solid #D4D4D4; + background-color: #e5eecc; +} diff --git a/tools/coqdoc/coqdoc.sty b/tools/coqdoc/coqdoc.sty index f49f9f0066..aa9c414761 100644 --- a/tools/coqdoc/coqdoc.sty +++ b/tools/coqdoc/coqdoc.sty @@ -72,6 +72,7 @@ \newcommand{\coqdocinductive}[1]{\coqdocind{#1}} \newcommand{\coqdocdefinition}[1]{\coqdoccst{#1}} \newcommand{\coqdocvariable}[1]{\coqdocvar{#1}} +\newcommand{\coqdocbinder}[1]{\coqdocvar{#1}} \newcommand{\coqdocconstructor}[1]{\coqdocconstr{#1}} \newcommand{\coqdoclemma}[1]{\coqdoccst{#1}} \newcommand{\coqdocclass}[1]{\coqdocind{#1}} diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll index 210ac754a1..86d213453b 100644 --- a/tools/coqdoc/cpretty.mll +++ b/tools/coqdoc/cpretty.mll @@ -32,6 +32,19 @@ in count 0 0 + let count_newlines s = + let len = String.length s in + let n = ref 0 in + String.iteri (fun i c -> + match c with (* skip "\r\n" *) + | '\r' when i + 1 = len || s.[i+1] = '\n' -> incr n + | '\n' -> incr n + | _ -> ()) s; + !n + + (* Whether a string starts with a newline (used on strings that might match the [nl] regexp) *) + let is_nl s = String.length s = 0 || let c = s.[0] in c = '\n' || c = '\r' + let remove_newline s = let n = String.length s in let rec count i = if i == n || s.[i] <> '\n' then i else count (i + 1) in @@ -65,8 +78,12 @@ let eol = s.[String.length s - 1] = '\n' in (eol, if eol then String.sub s 1 (String.length s - 1) else s) + let is_none x = + match x with + | None -> true + | Some _ -> false - let formatted = ref false + let formatted : position option ref = ref None let brackets = ref 0 let comment_level = ref 0 let in_proof = ref None @@ -116,10 +133,15 @@ let begin_show () = save_state (); Cdglobals.gallina := false; Cdglobals.light := false let end_show () = restore_state () + let begin_details s = + save_state (); Cdglobals.gallina := false; Cdglobals.light := false; + Output.start_details s + let end_details () = Output.stop_details (); restore_state () + (* Reset the globals *) let reset () = - formatted := false; + formatted := None; brackets := 0; comment_level := 0 @@ -247,13 +269,28 @@ let parse_comments () = !Cdglobals.parse_comments && not (only_gallina ()) + (* Advance lexbuf by n lines. Equivalent to calling [Lexing.new_line lexbuf] n times *) + let new_lines n lexbuf = + let lcp = lexbuf.lex_curr_p in + if lcp != dummy_pos then + lexbuf.lex_curr_p <- + { lcp with + pos_lnum = lcp.pos_lnum + n; + pos_bol = lcp.pos_cnum } + + let print_position chan p = + Printf.fprintf chan "%s:%d:%d" p.pos_fname p.pos_lnum (p.pos_cnum - p.pos_bol) + + exception MismatchPreformatted of position + + (* let debug lexbuf msg = Printf.printf "%a %s\n" print_position lexbuf.lex_start_p msg *) } (*s Regular expressions *) let space = [' ' '\t'] -let space_nl = [' ' '\t' '\n' '\r'] -let nl = "\r\n" | '\n' +let nl = "\r\n" | '\n' | '\r' +let space_nl = space | nl let firstchar = ['A'-'Z' 'a'-'z' '_'] | @@ -430,10 +467,12 @@ let section = "*" | "**" | "***" | "****" let item_space = " " -let begin_hide = "(*" space* "begin" space+ "hide" space* "*)" space* nl -let end_hide = "(*" space* "end" space+ "hide" space* "*)" space* nl -let begin_show = "(*" space* "begin" space+ "show" space* "*)" space* nl -let end_show = "(*" space* "end" space+ "show" space* "*)" space* nl +let begin_hide = "(*" space* "begin" space+ "hide" space* "*)" space* +let end_hide = "(*" space* "end" space+ "hide" space* "*)" space* +let begin_show = "(*" space* "begin" space+ "show" space* "*)" space* +let end_show = "(*" space* "end" space+ "show" space* "*)" space* +let begin_details = "(*" space* "begin" space+ "details" space* +let end_details = "(*" space* "end" space+ "details" space* "*)" space* (* let begin_verb = "(*" space* "begin" space+ "verb" space* "*)" let end_verb = "(*" space* "end" space+ "verb" space* "*)" @@ -442,24 +481,36 @@ let end_verb = "(*" space* "end" space+ "verb" space* "*)" (*s Scanning Coq, at beginning of line *) rule coq_bol = parse - | space* nl+ - { if not (!in_proof <> None && (!Cdglobals.gallina || !Cdglobals.light)) + | space* (nl+ as s) + { new_lines (String.length s) lexbuf; + if not (!in_proof <> None && (!Cdglobals.gallina || !Cdglobals.light)) then Output.empty_line_of_code (); coq_bol lexbuf } - | space* "(**" space_nl - { Output.end_coq (); Output.start_doc (); + | space* "(**" (space_nl as s) + { if is_nl s then Lexing.new_line lexbuf; + Output.end_coq (); Output.start_doc (); let eol = doc_bol lexbuf in Output.end_doc (); Output.start_coq (); if eol then coq_bol lexbuf else coq lexbuf } - | space* "Comments" space_nl - { Output.end_coq (); Output.start_doc (); comments lexbuf; Output.end_doc (); - Output.start_coq (); coq lexbuf } - | space* begin_hide - { skip_hide lexbuf; coq_bol lexbuf } - | space* begin_show - { begin_show (); coq_bol lexbuf } - | space* end_show - { end_show (); coq_bol lexbuf } + | space* "Comments" (space_nl as s) + { if is_nl s then Lexing.new_line lexbuf; + Output.end_coq (); Output.start_doc (); + comments lexbuf; + Output.end_doc (); Output.start_coq (); + coq lexbuf } + | space* begin_hide nl + { Lexing.new_line lexbuf; skip_hide lexbuf; coq_bol lexbuf } + | space* begin_show nl + { Lexing.new_line lexbuf; begin_show (); coq_bol lexbuf } + | space* end_show nl + { Lexing.new_line lexbuf; end_show (); coq_bol lexbuf } + | space* begin_details nl + { Lexing.new_line lexbuf; + let s = details_body lexbuf in + Output.end_coq (); begin_details s; Output.start_coq (); coq_bol lexbuf } + | space* end_details nl + { Lexing.new_line lexbuf; + Output.end_coq (); end_details (); Output.start_coq (); coq_bol lexbuf } | space* (("Local"|"Global") space+)? gallina_kw_to_hide { let s = lexeme lexbuf in if !Cdglobals.light && section_or_end s then @@ -565,9 +616,10 @@ rule coq_bol = parse and coq = parse | nl - { if not (only_gallina ()) then Output.line_break(); coq_bol lexbuf } - | "(**" space_nl - { Output.end_coq (); Output.start_doc (); + { Lexing.new_line lexbuf; if not (only_gallina ()) then Output.line_break(); coq_bol lexbuf } + | "(**" (space_nl as s) + { if is_nl s then Lexing.new_line lexbuf; + Output.end_coq (); Output.start_doc (); let eol = doc_bol lexbuf in Output.end_doc (); Output.start_coq (); if eol then coq_bol lexbuf else coq lexbuf } @@ -579,8 +631,9 @@ and coq = parse comment lexbuf end else skipped_comment lexbuf in if eol then coq_bol lexbuf else coq lexbuf } - | nl+ space* "]]" - { if not !formatted then + | (nl+ as s) space* "]]" + { new_lines (count_newlines s) lexbuf; + if is_none !formatted then begin (* Isn't this an anomaly *) let s = lexeme lexbuf in @@ -665,8 +718,9 @@ and coq = parse (*s Scanning documentation, at beginning of line *) and doc_bol = parse - | space* section space+ ([^'\n' '*'] | '*'+ [^'\n' ')' '*'])* ('*'+ '\n')? - { let eol, lex = strip_eol (lexeme lexbuf) in + | space* section space+ ([^'\n' '\r' '*'] | '*'+ [^'\n' '\r' ')' '*'])* ('*'+ (nl as s))? + { if not (is_none s) then Lexing.new_line lexbuf; + let eol, lex = strip_eol (lexeme lexbuf) in let lev, s = sec_title lex in if (!Cdglobals.lib_subtitles) && (subtitle (Output.get_module false) s) then @@ -674,24 +728,20 @@ and doc_bol = parse else Output.section lev (fun () -> ignore (doc None (from_string s))); if eol then doc_bol lexbuf else doc None lexbuf } - | space_nl* '-'+ - { let buf' = lexeme lexbuf in - let bufs = Str.split_delim (Str.regexp "['\n']") buf' in - let lines = (List.length bufs) - 1 in - let line = - match bufs with - | [] -> eprintf "Internal error bad_split1 - please report\n"; - exit 1 - | _ -> List.nth bufs lines - in - match check_start_list line with - | Neither -> backtrack_past_newline lexbuf; doc None lexbuf - | List n -> if lines > 0 then Output.paragraph (); - Output.item 1; doc (Some [n]) lexbuf - | Rule -> Output.rule (); doc None lexbuf + | (space_nl* as s) ('-'+ as line) + { let nl_count = count_newlines s in + match check_start_list line with + | Neither -> backtrack_past_newline lexbuf; Lexing.new_line lexbuf; doc None lexbuf + | List n -> + new_lines nl_count lexbuf; + if nl_count > 0 then Output.paragraph (); + Output.item 1; doc (Some [n]) lexbuf + | Rule -> + new_lines nl_count lexbuf; + Output.rule (); doc None lexbuf } - | space* nl+ - { Output.paragraph (); doc_bol lexbuf } + | (space_nl* nl) as s + { new_lines (count_newlines s) lexbuf; Output.paragraph (); doc_bol lexbuf } | "<<" space* { Output.start_verbatim false; verbatim 0 false lexbuf; doc_bol lexbuf } | eof @@ -699,8 +749,7 @@ and doc_bol = parse | '_' { if !Cdglobals.plain_comments then Output.char '_' else start_emph (); doc None lexbuf } - | _ - { backtrack lexbuf; doc None lexbuf } + | "" { doc None lexbuf } (*s Scanning lists - using whitespace *) and doc_list_bol indents = parse @@ -721,11 +770,11 @@ and doc_list_bol indents = parse verbatim 0 false lexbuf; doc_list_bol indents lexbuf } | "[[" nl - { formatted := true; + { formatted := Some lexbuf.lex_start_p; Output.start_inline_coq_block (); ignore(body_bol lexbuf); Output.end_inline_coq_block (); - formatted := false; + formatted := None; doc_list_bol indents lexbuf } | "[[[" nl { inf_rules (Some indents) lexbuf } @@ -788,10 +837,10 @@ and doc indents = parse | "[[" nl { if !Cdglobals.plain_comments then (Output.char '['; Output.char '['; doc indents lexbuf) - else (formatted := true; + else (formatted := Some lexbuf.lex_start_p; Output.start_inline_coq_block (); let eol = body_bol lexbuf in - Output.end_inline_coq_block (); formatted := false; + Output.end_inline_coq_block (); formatted := None; if eol then match indents with | Some ls -> doc_list_bol ls lexbuf @@ -816,16 +865,15 @@ and doc indents = parse if !Cdglobals.parse_comments then comment lexbuf else skipped_comment lexbuf in if eol then bol_parse lexbuf else doc indents lexbuf } - | '*'* "*)" space_nl* "(**" - {(match indents with + | '*'* "*)" (space_nl* as s) "(**" + { let nl_count = count_newlines s in + new_lines nl_count lexbuf; + (match indents with | Some _ -> Output.stop_item () | None -> ()); (* this says - if there is a blank line between the two comments, insert one in the output too *) - let lines = List.length (Str.split_delim (Str.regexp "['\n']") - (lexeme lexbuf)) - in - if lines > 2 then Output.paragraph (); + if nl_count > 1 then Output.paragraph (); doc_bol lexbuf } | '*'* "*)" space* nl @@ -1017,10 +1065,10 @@ and comment = parse comment lexbuf } | "[[" nl { if !Cdglobals.plain_comments then (Output.char '['; Output.char '[') - else (formatted := true; + else (formatted := Some lexbuf.lex_start_p; Output.start_inline_coq_block (); let _ = body_bol lexbuf in - Output.end_inline_coq_block (); formatted := false); + Output.end_inline_coq_block (); formatted := None); comment lexbuf } | "$" { if !Cdglobals.plain_comments then Output.char '$' @@ -1083,13 +1131,14 @@ and skip_to_dot_or_brace = parse and body_bol = parse | space+ { Output.indentation (fst (count_spaces (lexeme lexbuf))); body lexbuf } - | _ { backtrack lexbuf; Output.indentation 0; body lexbuf } + | "" { Output.indentation 0; body lexbuf } and body = parse | nl {Tokens.flush_sublexer(); Output.line_break(); Lexing.new_line lexbuf; body_bol lexbuf} - | nl+ space* "]]" space* nl - { Tokens.flush_sublexer(); - if not !formatted then + | (nl+ as s) space* "]]" space* nl + { new_lines (count_newlines s + 1) lexbuf; + Tokens.flush_sublexer(); + if is_none !formatted then begin let s = lexeme lexbuf in let nlsp,s = remove_newline s in @@ -1107,7 +1156,8 @@ and body = parse end } | "]]" space* nl { Tokens.flush_sublexer(); - if not !formatted then + Lexing.new_line lexbuf; + if is_none !formatted then begin let loc = lexeme_start lexbuf in Output.sublexer ']' loc; @@ -1121,13 +1171,19 @@ and body = parse Output.paragraph (); true end } - | eof { Tokens.flush_sublexer(); false } - | '.' space* nl | '.' space* eof - { Tokens.flush_sublexer(); Output.char '.'; Output.line_break(); - if not !formatted then true else body_bol lexbuf } + | eof + { Tokens.flush_sublexer(); + match !formatted with + | None -> false + | Some p -> raise (MismatchPreformatted p) } + | '.' space* (nl as s | eof) + { if not (is_none s) then new_line lexbuf; + Tokens.flush_sublexer(); Output.char '.'; Output.line_break(); + if is_none !formatted then true else body_bol lexbuf } | '.' space* nl "]]" space* nl - { Tokens.flush_sublexer(); Output.char '.'; - if not !formatted then + { new_lines 2 lexbuf; + Tokens.flush_sublexer(); Output.char '.'; + if is_none !formatted then begin eprintf "Error: stray ]] at %d\n" (lexeme_start lexbuf); flush stderr; @@ -1141,9 +1197,10 @@ and body = parse } | '.' space+ { Tokens.flush_sublexer(); Output.char '.'; Output.char ' '; - if not !formatted then false else body lexbuf } - | "(**" space_nl - { Tokens.flush_sublexer(); Output.end_coq (); Output.start_doc (); + if is_none !formatted then false else body lexbuf } + | "(**" (space_nl as s) + { if is_nl s then new_line lexbuf; + Tokens.flush_sublexer(); Output.end_coq (); Output.start_doc (); let eol = doc_bol lexbuf in Output.end_doc (); Output.start_coq (); if eol then body_bol lexbuf else body lexbuf } @@ -1208,19 +1265,37 @@ and string = parse | _ { let c = lexeme_char lexbuf 0 in Output.char c; string lexbuf } and skip_hide = parse - | eof | end_hide { () } + | eof | end_hide nl { Lexing.new_line lexbuf; () } | _ { skip_hide lexbuf } (*s Reading token pretty-print *) and printing_token_body = parse - | "*)" nl? | eof - { let s = Buffer.contents token_buffer in + | "*)" (nl as s)? | eof + { if not (is_none s) then Lexing.new_line lexbuf; + let s = Buffer.contents token_buffer in Buffer.clear token_buffer; s } - | _ { Buffer.add_string token_buffer (lexeme lexbuf); + | (nl | _) as s + { if is_nl s then Lexing.new_line lexbuf; + Buffer.add_string token_buffer (lexeme lexbuf); printing_token_body lexbuf } +and details_body = parse + | "*)" space* (nl as s)? | eof + { if not (is_none s) then Lexing.new_line lexbuf; + None } + | ":" space* { details_body_rec lexbuf } + +and details_body_rec = parse + | "*)" space* (nl as s)? | eof + { if not (is_none s) then Lexing.new_line lexbuf; + let s = Buffer.contents token_buffer in + Buffer.clear token_buffer; + Some s } + | _ { Buffer.add_string token_buffer (lexeme lexbuf); + details_body_rec lexbuf } + (*s These handle inference rules, parsing the body segments of things enclosed in [[[ ]]] brackets *) and inf_rules indents = parse @@ -1318,6 +1393,14 @@ and st_subtitle = parse (*s Applying the scanners to files *) { + (* coq_bol with error handling *) + let coq_bol' f lb = + Lexing.new_line lb; (* Start numbering lines from 1 *) + try coq_bol lb with + | MismatchPreformatted p -> + Printf.eprintf "%a: mismatched \"[[\"\n" print_position { p with pos_fname = f }; + exit 1 + let coq_file f m = reset (); let c = open_in f in @@ -1325,7 +1408,7 @@ and st_subtitle = parse (Index.current_library := m; Output.initialize (); Output.start_module (); - Output.start_coq (); coq_bol lb; Output.end_coq (); + Output.start_coq (); coq_bol' f lb; Output.end_coq (); close_in c) let detect_subtitle f m = diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml index 4cc82726f1..723918525d 100644 --- a/tools/coqdoc/index.ml +++ b/tools/coqdoc/index.ml @@ -31,6 +31,7 @@ type entry_type = | Abbreviation | Notation | Section + | Binder type index_entry = | Def of string * entry_type @@ -177,6 +178,7 @@ let type_name = function | Abbreviation -> "abbreviation" | Notation -> "notation" | Section -> "section" + | Binder -> "binder" let prepare_entry s = function | Notation -> @@ -268,6 +270,7 @@ let type_of_string = function | "mod" | "modtype" -> Module | "tac" -> TacticDefinition | "sec" -> Section + | "binder" -> Binder | s -> invalid_arg ("type_of_string:" ^ s) let ill_formed_glob_file f = diff --git a/tools/coqdoc/index.mli b/tools/coqdoc/index.mli index 3426fdd3d3..7a3d401fd7 100644 --- a/tools/coqdoc/index.mli +++ b/tools/coqdoc/index.mli @@ -30,6 +30,7 @@ type entry_type = | Abbreviation | Notation | Section + | Binder val type_name : entry_type -> string diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 862715753d..def1cbbcf8 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -337,11 +337,8 @@ module Latex = struct let id = if fid <> "" then (m ^ "." ^ fid) else m in match find_module m with | Local -> - if typ = Variable then - printf "\\coqdoc%s{%s}" (type_name typ) s - else - (printf "\\coqref{"; label_ident id; - printf "}{\\coqdoc%s{%s}}" (type_name typ) s) + printf "\\coqref{"; label_ident id; + printf "}{\\coqdoc%s{%s}}" (type_name typ) s | External m when !externals -> printf "\\coqexternalref{"; label_ident fid; printf "}{%s}{\\coqdoc%s{%s}}" (escaped m) (type_name typ) s @@ -469,6 +466,11 @@ module Latex = struct let stop_emph () = printf "}" + let start_details _ = () + + let stop_details () = () + + let start_comment () = printf "\\begin{coqdoccomment}\n" let end_comment () = printf "\\end{coqdoccomment}\n" @@ -610,6 +612,7 @@ module Html = struct else match s.[i] with | 'a'..'z' | 'A'..'Z' | '0'..'9' | '.' | '_' -> loop esc (i-1) | '<' | '>' | '&' | '\'' | '\"' -> loop true (i-1) + | '-' | ':' -> loop esc (i-1) (* should be safe in HTML5 attribute name syntax *) | _ -> (* This name contains complex characters: this is probably a notation string, we simply hash it. *) @@ -656,7 +659,8 @@ module Html = struct let reference s r = match r with | Def (fullid,ty) -> - printf "<a name=\"%s\">" (sanitize_name fullid); + let s' = sanitize_name fullid in + printf "<a id=\"%s\" class=\"idref\" href=\"#%s\">" s' s'; printf "<span class=\"id\" title=\"%s\">%s</span></a>" (type_name ty) s | Ref (m,fullid,ty) -> ident_ref m fullid (type_name ty) s @@ -740,6 +744,12 @@ module Html = struct let stop_emph () = printf "</i>" + let start_details = function + | Some s -> printf "<details><summary>%s</summary>" s + | _ -> printf "<details>" + + let stop_details () = printf "</details>" + let start_comment () = printf "<span class=\"comment\">(*" let end_comment () = printf "*)</span>" @@ -811,7 +821,7 @@ module Html = struct | Some n -> if lev <= n then add_toc_entry (Toc_section (lev, f, r)) else ()); stop_item (); - printf "<a name=\"%s\"></a><h%d class=\"section\">" lab lev; + printf "<a id=\"%s\"></a><h%d class=\"section\">" lab lev; f (); printf "</h%d>\n" lev @@ -825,7 +835,7 @@ module Html = struct let letter_index category idx (c,l) = if l <> [] then begin let cat = if category && idx <> "global" then "(" ^ idx ^ ")" else "" in - printf "<a name=\"%s_%c\"></a><h2>%s %s</h2>\n" idx c (display_letter c) cat; + printf "<a id=\"%s_%c\"></a><h2>%s %s</h2>\n" idx c (display_letter c) cat; List.iter (fun (id,(text,link,t)) -> let id' = prepare_entry id t in @@ -1053,6 +1063,9 @@ module TeXmacs = struct let start_emph () = printf "<with|font shape|italic|" let stop_emph () = printf ">" + let start_details _ = () + let stop_details () = () + let start_comment () = () let end_comment () = () @@ -1159,6 +1172,9 @@ module Raw = struct let start_emph () = printf "_" let stop_emph () = printf "_" + let start_details _ = () + let stop_details () = () + let start_comment () = printf "(*" let end_comment () = printf "*)" @@ -1272,6 +1288,11 @@ let start_emph = let stop_emph = select Latex.stop_emph Html.stop_emph TeXmacs.stop_emph Raw.stop_emph +let start_details = + select Latex.start_details Html.start_details TeXmacs.start_details Raw.start_details +let stop_details = + select Latex.stop_details Html.stop_details TeXmacs.stop_details Raw.stop_details + let start_latex_math = select Latex.start_latex_math Html.start_latex_math TeXmacs.start_latex_math Raw.start_latex_math let stop_latex_math = diff --git a/tools/coqdoc/output.mli b/tools/coqdoc/output.mli index 485183a4ed..b7a8d4d858 100644 --- a/tools/coqdoc/output.mli +++ b/tools/coqdoc/output.mli @@ -29,6 +29,9 @@ val start_module : unit -> unit val start_doc : unit -> unit val end_doc : unit -> unit +val start_details : string option -> unit +val stop_details : unit -> unit + val start_emph : unit -> unit val stop_emph : unit -> unit diff --git a/tools/dune b/tools/dune index c0e4e20f72..d591bb0c37 100644 --- a/tools/dune +++ b/tools/dune @@ -49,8 +49,8 @@ (ocamllex coqwc) (executables - (names coq_tex coq_dune) - (public_names coq-tex coq_dune) + (names coq_tex) + (public_names coq-tex) (package coq) - (modules coq_tex coq_dune) + (modules coq_tex) (libraries str)) diff --git a/tools/make-both-time-files.py b/tools/make-both-time-files.py index 5d88548bba..3959ff5c2a 100755 --- a/tools/make-both-time-files.py +++ b/tools/make-both-time-files.py @@ -5,11 +5,13 @@ if __name__ == '__main__': 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_include_mem(parser) + add_sort_by_mem(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) + left_dict = get_times_and_mems(args.AFTER_FILE_NAME, use_real=args.real, include_mem=args.include_mem) + right_dict = get_times_and_mems(args.BEFORE_FILE_NAME, use_real=args.real, include_mem=args.include_mem) + table = make_diff_table_string(left_dict, right_dict, sort_by=args.sort_by, include_mem=args.include_mem, sort_by_mem=args.sort_by_mem) 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 3df7d7e584..df02383724 100755 --- a/tools/make-one-time-file.py +++ b/tools/make-one-time-file.py @@ -7,7 +7,9 @@ if __name__ == '__main__': add_real(parser) add_file_name(parser) add_output_file_name(parser) + add_include_mem(parser) + add_sort_by_mem(parser) args = parser.parse_args() - times_dict = get_times(args.FILE_NAME, use_real=args.real) - table = make_table_string(times_dict) + stats_dict = get_times_and_mems(args.FILE_NAME, use_real=args.real, include_mem=args.include_mem) + table = make_table_string(stats_dict, include_mem=args.include_mem, sort_by_mem=args.sort_by_mem) print_or_write_table(table, args.OUTPUT_FILE_NAME) |