diff options
Diffstat (limited to 'tools')
33 files changed, 461 insertions, 92 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 7b01c1b663..f1e519d038 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -10,6 +10,7 @@ INITIAL_VARS := $(.VARIABLES) # To implement recursion we save the name of the main Makefile SELF := $(lastword $(MAKEFILE_LIST)) +PARENT := $(firstword $(MAKEFILE_LIST)) # This file is generated by coq_makefile and contains many variable # definitions, like the list of .v files or the path to Coq @@ -62,22 +63,46 @@ VERBOSE ?= # Time the Coq process (set to non empty), and how (see default value) TIMED?= TIMECMD?= -STDTIME?=/usr/bin/time -f "$* (user: %U mem: %M ko)" +# Use /usr/bin/time on linux, gtime on Mac OS +TIMEFMT?="$* (real: %e, user: %U, sys: %S, mem: %M ko)" +ifneq (,$(TIMED)) +ifeq (0,$(shell /usr/bin/time -f $(TIMEFMT) true >/dev/null 2>/dev/null; echo $$?)) +STDTIME?=/usr/bin/time -f $(TIMEFMT) +else +ifeq (0,$(shell gtime -f $(TIMEFMT) true >/dev/null 2>/dev/null; echo $$?)) +STDTIME?=gtime -f $(TIMEFMT) +else +STDTIME?=time +endif +endif +else +STDTIME?=/usr/bin/time -f $(TIMEFMT) +endif # Coq binaries COQC ?= "$(COQBIN)coqc" +COQTOP ?= "$(COQBIN)coqtop" COQCHK ?= "$(COQBIN)coqchk" COQDEP ?= "$(COQBIN)coqdep" GALLINA ?= "$(COQBIN)gallina" COQDOC ?= "$(COQBIN)coqdoc" COQMKTOP ?= "$(COQBIN)coqmktop" +COQMKFILE ?= "$(COQBIN)coq_makefile" + +# Timing scripts +COQMAKE_ONE_TIME_FILE ?= "$(COQLIB)/tools/make-one-time-file.py" +COQMAKE_BOTH_TIME_FILES ?= "$(COQLIB)/tools/make-both-time-files.py" +COQMAKE_BOTH_SINGLE_TIMING_FILES ?= "$(COQLIB)/tools/make-both-single-timing-files.py" +BEFORE ?= +AFTER ?= # OCaml binaries -CAMLC ?= $(OCAMLFIND) ocamlc -c -rectypes -thread -CAMLOPTC ?= $(OCAMLFIND) opt -c -rectypes -thread -CAMLLINK ?= $(OCAMLFIND) ocamlc -rectypes -thread -CAMLOPTLINK ?= $(OCAMLFIND) opt -rectypes -thread -CAMLDEP ?= $(OCAMLFIND) ocamldep -slash -ml-synonym .ml4 -ml-synonym .mlpack +CAMLC ?= "$(OCAMLFIND)" ocamlc -c -rectypes -thread +CAMLOPTC ?= "$(OCAMLFIND)" opt -c -rectypes -thread +CAMLLINK ?= "$(OCAMLFIND)" ocamlc -rectypes -thread +CAMLOPTLINK ?= "$(OCAMLFIND)" opt -rectypes -thread +CAMLDOC ?= "$(OCAMLFIND)" ocamldoc -rectypes +CAMLDEP ?= "$(OCAMLFIND)" ocamldep -slash -ml-synonym .ml4 -ml-synonym .mlpack # DESTDIR is prepended to all installation paths DESTDIR ?= @@ -86,7 +111,15 @@ DESTDIR ?= CAMLDEBUG ?= COQDEBUG ?= - +# Option for making timing files +TIMING?= +# Output file names for timed builds +TIME_OF_BUILD_FILE ?= time-of-build.log +TIME_OF_BUILD_BEFORE_FILE ?= time-of-build-before.log +TIME_OF_BUILD_AFTER_FILE ?= time-of-build-after.log +TIME_OF_PRETTY_BUILD_FILE ?= time-of-build-pretty.log +TIME_OF_PRETTY_BOTH_BUILD_FILE ?= time-of-build-both.log +TIME_OF_PRETTY_BUILD_EXTRA_FILES ?= - # also output to the command line ########## End of parameters ################################################## # What follows may be relevant to you only if you need to @@ -139,7 +172,7 @@ COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)$(d)") CAMLFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB) -CAMLLIB:=$(shell $(OCAMLFIND) printconf stdlib) +CAMLLIB:=$(shell "$(OCAMLFIND)" printconf stdlib) # FIXME This should be generated by Coq GRAMMARS:=grammar.cma @@ -149,17 +182,34 @@ else CAMLP4EXTEND= endif -PP:=-pp '$(CAMLP4O) -I $(CAMLLIB) -I $(COQLIB)/grammar compat5.cmo $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl' +PP:=-pp '$(CAMLP4O) -I $(CAMLLIB) -I "$(COQLIB)/grammar" compat5.cmo $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl' -COQLIBINSTALL = $(COQLIB)user-contrib -COQDOCINSTALL = $(DOCDIR)user-contrib -COQTOPINSTALL = $(COQLIB)toploop +ifneq (,$(TIMING)) +TIMING_ARG=-time +ifeq (after,$(TIMING)) +TIMING_EXT=after-timing +else +ifeq (before,$(TIMING)) +TIMING_EXT=before-timing +else +TIMING_EXT=timing +endif +endif +else +TIMING_ARG= +endif # Retro compatibility (DESTDIR is standard on Unix, DESTROOT is not) ifneq "$(DSTROOT)" "" DESTDIR := $(DSTROOT) endif +concat_path = $(if $(1),$(1)/$(subst $(COQMF_WINDRIVE),/,$(2)),$(2)) + +COQLIBINSTALL = $(call concat_path,$(DESTDIR),$(COQLIB)user-contrib) +COQDOCINSTALL = $(call concat_path,$(DESTDIR),$(DOCDIR)user-contrib) +COQTOPINSTALL = $(call concat_path,$(DESTDIR),$(COQLIB)toploop) + # Files ####################################################################### # # We here define a bunch of variables about the files being part of the @@ -176,7 +226,7 @@ ALLSRCFILES := \ # helpers vo_to_obj = $(addsuffix .o,\ $(filter-out Warning: Error:,\ - $(shell $(COQBIN)coqtop -q -noinit -batch -quiet -print-mod-uid $(1)))) + $(shell $(COQTOP) -q -noinit -batch -quiet -print-mod-uid $(1)))) strip_dotslash = $(patsubst ./%,%,$(1)) VO = vo @@ -254,6 +304,41 @@ all: $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" post-all .PHONY: all +all.timing.diff: + $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" pre-all + $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" real-all.timing.diff TIME_OF_PRETTY_BUILD_EXTRA_FILES="" + $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" post-all +.PHONY: all.timing.diff + +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:: + $(HIDE)rm -f pretty-timed-success.ok + $(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) +print-pretty-timed-diff:: + $(HIDE)$(COQMAKE_BOTH_TIME_FILES) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_BUILD_AFTER_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 BEFORE=path/to/file.v.before-timing AFTER=path/to/file.v.after-timing' + $(HIDE)false +else +ifeq (,$(AFTER)) +print-pretty-single-time-diff:: + @echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff BEFORE=path/to/file.v.before-timing AFTER=path/to/file.v.after-timing' + $(HIDE)false +else +print-pretty-single-time-diff:: + $(HIDE)$(COQMAKE_BOTH_SINGLE_TIMING_FILES) $(BEFORE) $(AFTER) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) +endif +endif +pretty-timed: + $(HIDE)$(MAKE) --no-print-directory -f "$(PARENT)" make-pretty-timed + $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" print-pretty-timed +.PHONY: pretty-timed make-pretty-timed make-pretty-timed-before make-pretty-timed-after print-pretty-timed print-pretty-timed-diff print-pretty-single-time-diff + # Extension points for actions to be performed before/after the all target pre-all:: @# Extension point @@ -270,6 +355,9 @@ post-all:: real-all: $(VOFILES) $(if $(USEBYTE),bytefiles,optfiles) .PHONY: real-all +real-all.timing.diff: $(VOFILES:.vo=.v.timing.diff) +.PHONE: real-all.timing.diff + bytefiles: $(CMOFILES) $(CMAFILES) .PHONY: bytefiles @@ -306,14 +394,14 @@ html: $(GLOBFILES) $(VFILES) -toc $(COQDOCFLAGS) -html $(GAL) $(COQDOCLIBS) -d html $(VFILES) mlihtml: $(MLIFILES:.mli=.cmi) - $(SHOW)'OCAMLDOC -d $@' + $(SHOW)'CAMLDOC -d $@' $(HIDE)mkdir $@ || rm -rf $@/* - $(HIDE)$(OCAMLFIND) ocamldoc -html -rectypes \ + $(HIDE)$(CAMLDOC) -html \ -d $@ -m A $(CAMLDEBUG) $(CAMLFLAGS) $(MLIFILES) all-mli.tex: $(MLIFILES:.mli=.cmi) - $(SHOW)'OCAMLDOC -latex $@' - $(OCAMLFIND) ocamldoc -latex -rectypes \ + $(SHOW)'CAMLDOC -latex $@' + $(HIDE)$(CAMLDOC) -latex \ -o $@ -m A $(CAMLDEBUG) $(CAMLFLAGS) $(MLIFILES) gallina: $(GFILES) @@ -354,13 +442,13 @@ beautify: $(BEAUTYFILES) install: install-extra $(HIDE)for f in $(FILESTOINSTALL); do\ - df="`$(COQMF_MAKEFILE) -destination-of "$$f" $(COQLIBS)`";\ - if [ -z "$$df" ]; then\ + df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`";\ + if [ "$$?" != "0" -o -z "$$df" ]; then\ echo SKIP "$$f" since it has no logical path;\ else\ - install -d "$(DESTDIR)$(COQLIBINSTALL)/$$df"; \ - install -m 0644 "$$f" "$(DESTDIR)$(COQLIBINSTALL)/$$df"; \ - echo INSTALL "$$f" "$(DESTDIR)$(COQLIBINSTALL)/$$df";\ + install -d "$(COQLIBINSTALL)/$$df" &&\ + install -m 0644 "$$f" "$(COQLIBINSTALL)/$$df" &&\ + echo INSTALL "$$f" "$(COQLIBINSTALL)/$$df";\ fi;\ done install-extra:: @@ -369,28 +457,28 @@ install-extra:: install-byte: $(HIDE)for f in $(BYTEFILESTOINSTALL); do\ - df="`$(COQMF_MAKEFILE) -destination-of "$$f" $(COQLIBS)`";\ - if [ -z "$$df" ]; then\ + df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`";\ + if [ "$$?" != "0" -o -z "$$df" ]; then\ echo SKIP "$$f" since it has no logical path;\ else\ - install -d "$(DESTDIR)$(COQLIBINSTALL)/$$df"; \ - install -m 0644 "$$f" "$(DESTDIR)$(COQLIBINSTALL)/$$df"; \ - echo INSTALL "$$f" "$(DESTDIR)$(COQLIBINSTALL)/$$df";\ + install -d "$(COQLIBINSTALL)/$$df" &&\ + install -m 0644 "$$f" "$(COQLIBINSTALL)/$$df" &&\ + echo INSTALL "$$f" "$(COQLIBINSTALL)/$$df";\ fi;\ done install-doc:: html mlihtml @# Extension point - $(HIDE)install -d "$(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html" + $(HIDE)install -d "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html" $(HIDE)for i in html/*; do \ - dest="$(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/$$i";\ + dest="$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/$$i";\ install -m 0644 "$$i" "$$dest";\ echo INSTALL "$$i" "$$dest";\ done $(HIDE)install -d \ - "$(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml" + "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml" $(HIDE)for i in mlihtml/*; do \ - dest="$(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/$$i";\ + dest="$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/$$i";\ install -m 0644 "$$i" "$$dest";\ echo INSTALL "$$i" "$$dest";\ done @@ -399,21 +487,21 @@ install-doc:: html mlihtml uninstall:: @# Extension point $(HIDE)for f in $(FILESTOINSTALL); do \ - df="`$(COQMF_MAKEFILE) -destination-of "$$f" $(COQLIBS)`";\ - instf="$(DESTDIR)$(COQLIBINSTALL)/$$df/`basename $$f`"; \ - rm -f "$$instf";\ - echo RM "$$instf"; \ - rmdir "$(DESTDIR)$(COQLIBINSTALL)/$$df/" || true; \ + df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`" &&\ + instf="$(COQLIBINSTALL)/$$df/`basename $$f`" &&\ + rm -f "$$instf" &&\ + echo RM "$$instf" &&\ + (rmdir "$(call concat_path,,$(COQLIBINSTALL)/$$df/)" || true); \ done .PHONY: uninstall uninstall-doc:: @# Extension point - $(SHOW)'RM $(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html' - $(HIDE)rm -rf "$(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html" - $(SHOW)'RM $(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml' - $(HIDE)rm -rf "$(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml" - $(HIDE) rmdir "$(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/" || true + $(SHOW)'RM $(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html' + $(HIDE)rm -rf "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html" + $(SHOW)'RM $(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml' + $(HIDE)rm -rf "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml" + $(HIDE) rmdir "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/" || true .PHONY: uninstall-doc # Cleaning #################################################################### @@ -443,13 +531,19 @@ clean:: $(HIDE)rm -f $(VFILES:.v=.glob) $(HIDE)rm -f $(VFILES:.v=.tex) $(HIDE)rm -f $(VFILES:.v=.g.tex) + $(HIDE)rm -f pretty-timed-success.ok $(HIDE)rm -rf html mlihtml .PHONY: clean cleanall:: clean @# Extension point - $(SHOW)'CLEAN *.aux' + $(SHOW)'CLEAN *.aux *.timing' $(HIDE)rm -f $(foreach f,$(VFILES:.v=),$(dir $(f)).$(notdir $(f)).aux) + $(HIDE)rm -f $(TIME_OF_BUILD_FILE) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BOTH_BUILD_FILE) + $(HIDE)rm -f $(VOFILES:.vo=.v.timing) + $(HIDE)rm -f $(VOFILES:.vo=.v.before-timing) + $(HIDE)rm -f $(VOFILES:.vo=.v.after-timing) + $(HIDE)rm -f $(VOFILES:.vo=.v.timing.diff) .PHONY: cleanall archclean:: @@ -518,9 +612,15 @@ $(filter-out $(MLLIBFILES:.mllib=.cmxs) $(MLPACKFILES:.mlpack=.cmxs) $(addsuffix $(SHOW)'[deprecated,use-mllib-or-mlpack] CAMLOPT -shared -o $@' $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -shared -o $@ $< +ifneq (,$(TIMING)) +TIMING_EXTRA = > $<.$(TIMING_EXT) +else +TIMING_EXTRA = +endif + $(VOFILES): %.vo: %.v $(SHOW)COQC $< - $(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $< + $(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(TIMING_ARG) $(COQFLAGS) $< $(TIMING_EXTRA) # FIXME ?merge with .vo / .vio ? $(GLOBFILES): %.glob: %.v @@ -530,6 +630,10 @@ $(VFILES:.v=.vio): %.vio: %.v $(SHOW)COQC -quick $< $(HIDE)$(TIMER) $(COQC) -quick $(COQDEBUG) $(COQFLAGS) $< +$(addsuffix .timing.diff,$(VFILES)): %.timing.diff : %.before-timing %.after-timing + $(SHOW)PYTHON TIMING-DIFF $< + $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" print-pretty-single-time-diff BEFORE=$*.before-timing AFTER=$*.after-timing TIME_OF_PRETTY_BUILD_FILE="$@" + $(BEAUTYFILES): %.v.beautified: %.v $(SHOW)'BEAUTIFY $<' $(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $< @@ -556,7 +660,7 @@ $(GHTMLFILES): %.g.html: %.v %.glob # Dependency files ############################################################ -ifneq ($(filter-out archclean clean cleanall printenv,$(MAKECMDGOALS)),) +ifneq ($(filter-out archclean clean cleanall printenv make-pretty-timed make-pretty-timed-before make-pretty-timed-after print-pretty-timed print-pretty-timed-diff print-pretty-single-time-diff,$(MAKECMDGOALS)),) -include $(ALLDFILES) else ifeq ($(MAKECMDGOALS),) @@ -631,14 +735,14 @@ printenv:: .merlin: $(SHOW)'FILL .merlin' $(HIDE)echo 'FLG -rectypes' > .merlin - $(HIDE)echo "B $(COQLIB)" >> .merlin - $(HIDE)echo "S $(COQLIB)" >> .merlin + $(HIDE)echo 'B $(COQLIB)' >> .merlin + $(HIDE)echo 'S $(COQLIB)' >> .merlin $(HIDE)$(foreach d,$(COQ_SRC_SUBDIRS), \ - echo "B $(COQLIB)$(d)" >> .merlin;) + echo 'B $(COQLIB)$(d)' >> .merlin;) $(HIDE)$(foreach d,$(COQ_SRC_SUBDIRS), \ - echo "S $(COQLIB)$(d)" >> .merlin;) - $(HIDE)$(foreach d,$(SRC_SUBDIRS), echo "B $(d)" >> .merlin;) - $(HIDE)$(foreach d,$(SRC_SUBDIRS), echo "S $(d)" >> .merlin;) + echo 'S $(COQLIB)$(d)' >> .merlin;) + $(HIDE)$(foreach d,$(SRC_SUBDIRS), echo 'B $(d)' >> .merlin;) + $(HIDE)$(foreach d,$(SRC_SUBDIRS), echo 'S $(d)' >> .merlin;) $(HIDE)$(MAKE) merlin-hook -f "$(SELF)" .PHONY: merlin diff --git a/tools/TimeFileMaker.py b/tools/TimeFileMaker.py new file mode 100644 index 0000000000..a207c2171b --- /dev/null +++ b/tools/TimeFileMaker.py @@ -0,0 +1,187 @@ +#!/usr/bin/env python +from __future__ import with_statement +import os, sys, re + +# This script parses the output of `make TIMED=1` into a dictionary +# mapping names of compiled files to the number of minutes and seconds +# that they took to compile. + +STRIP_REG = re.compile('^(coq/|contrib/|)(?:theories/|src/)?') +STRIP_REP = r'\1' +INFINITY = '\xe2\x88\x9e' + +def reformat_time_string(time): + seconds, milliseconds = time.split('.') + seconds = int(seconds) + minutes, seconds = int(seconds / 60), seconds % 60 + return '%dm%02d.%ss' % (minutes, seconds, milliseconds) + +def get_times(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 compile durations, as strings. Removes common prefixes + using STRIP_REG and STRIP_REP. + ''' + if file_name == '-': + lines = sys.stdin.read() + else: + with open(file_name, 'r') as f: + lines = f.read() + reg = re.compile(r'^([^\s]+) \([^\)]*?user: ([0-9\.]+)[^\)]*?\)$', re.MULTILINE) + 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\.]+)[^\)]*?\)$', re.MULTILINE) + 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): + ''' + 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. + ''' + if file_name == '-': + lines = sys.stdin.read() + else: + with open(file_name, 'r') as f: + lines = f.read() + reg = re.compile(r'^Chars ([0-9]+) - ([0-9]+) ([^ ]+) ([0-9\.]+) secs (.*)$', 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) + 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) + +def make_sorting_key(times_dict, descending=True): + def get_key(name): + minutes, seconds = times_dict[name].replace('s', '').split('m') + def fix_sign(num): + return -num if descending else num + return (fix_sign(int(minutes)), fix_sign(float(seconds)), name) + return get_key + +def get_sorted_file_list_from_times_dict(times_dict, descending=True): + ''' + 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)) + +def to_seconds(time): + ''' + Converts a string time into a number of seconds. + ''' + minutes, seconds = time.replace('s', '').split('m') + sign = -1 if time[0] == '-' else 1 + return sign * (abs(int(minutes)) * 60 + float(seconds)) + +def from_seconds(seconds, signed=False): + ''' + Converts a number of seconds into a string time. + ''' + sign = ('-' if seconds < 0 else '+') if signed else '' + seconds = abs(seconds) + minutes = int(seconds) / 60 + seconds -= minutes * 60 + full_seconds = int(seconds) + partial_seconds = int(100 * (seconds - full_seconds)) + return sign + '%dm%02d.%02ds' % (minutes, full_seconds, partial_seconds) + +def sum_times(times, signed=False): + ''' + Takes the values of an output from get_times, parses the time + strings, and returns their sum, in the same string format. + ''' + return from_seconds(sum(map(to_seconds, times)), signed=signed) + +def format_percentage(num, signed=True): + sign = ('-' if num < 0 else '+') if signed else '' + num = abs(num) + whole_part = int(num * 100) + 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, + descending=True, + left_tag="After", tag="File Name", right_tag="Before", with_percent=True, + change_tag="Change", percent_change_tag="% Change"): + # 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 + 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'))) + 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) + # update to sort by approximate difference, first + get_key = make_sorting_key(all_names_dict, descending=descending) + all_names_dict = dict((name, (abs(int(to_seconds(diff_times_dict[name]))), get_key(name))) + for name in all_names_dict.keys()) + names = sorted(all_names_dict.keys(), key=all_names_dict.get) + #names = get_sorted_file_list_from_times_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(map(to_seconds, left_times_dict.values())) + right_sum_float = sum(map(to_seconds, right_times_dict.values())) + 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)) + 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)) + 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} + # 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 + return '\n'.join([header, sep, total, sep] + + [format_string % {'left': left_times_dict.get(name, 0), + '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' + # 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) + # 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") + sep = '-' * len(header) + return '\n'.join([header, sep, total, sep] + + [format_string % (times_dict[name], + name) + for name in names]) + +def print_or_write_table(table, files): + if len(files) == 0 or '-' in files: + print(table) + for file_name in files: + if file_name != '-': + with open(file_name, 'w') as f: + f.write(table) diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index e4f1359774..327f53520c 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -118,7 +118,7 @@ let makefile_template = let template = "/tools/CoqMakefile.in" in Coq_config.coqlib ^ template -let quote s = if String.contains s ' ' then "\"" ^ s ^ "\"" else s +let quote s = if String.contains s ' ' then "'" ^ s ^ "'" else s let generate_makefile oc conf_file local_file args project = let s = read_whole_file makefile_template in @@ -193,13 +193,19 @@ let generate_conf_includes oc { ml_includes; r_includes; q_includes } = (S.concat " " (map (fun ({ path },l) -> dash2 "R" path l) r_includes)) ;; +let windrive s = + if Coq_config.arch_is_win32 && Str.(string_match (regexp "^[a-zA-Z]:") s 0) + then Str.matched_string s + else s +;; + let generate_conf_coq_config oc args bypass_API = section oc "Coq configuration."; let src_dirs = if bypass_API then Coq_config.all_src_dirs - else Coq_config.api_dirs @ Coq_config.plugins_dirs in + else Coq_config.api_dirs @ Coq_config.plugins_dirs @ ["-open API"] in Envars.print_config ~prefix_var_name:"COQMF_" oc src_dirs; - fprintf oc "COQMF_MAKEFILE=%s\n" (quote (List.hd args)); + fprintf oc "COQMF_WINDRIVE=%s\n" (windrive Coq_config.coqlib) ;; let generate_conf_files oc diff --git a/tools/coq_tex.ml b/tools/coq_tex.ml index e17011b39a..7bc547c684 100644 --- a/tools/coq_tex.ml +++ b/tools/coq_tex.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tools/coqc.ml b/tools/coqc.ml index c1f0182d9c..5da203742c 100644 --- a/tools/coqc.ml +++ b/tools/coqc.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tools/coqdep.ml b/tools/coqdep.ml index cba9c3eb07..fd4be08b12 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tools/coqdep_boot.ml b/tools/coqdep_boot.ml index 25f62d2bec..0cb18f6a86 100644 --- a/tools/coqdep_boot.ml +++ b/tools/coqdep_boot.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index bf8bcd0c44..ab5196beb7 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli index 8c1787d315..99ec2cab4b 100644 --- a/tools/coqdep_common.mli +++ b/tools/coqdep_common.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tools/coqdep_lexer.mli b/tools/coqdep_lexer.mli index bb17fdf9f4..8bef3d39e6 100644 --- a/tools/coqdep_lexer.mli +++ b/tools/coqdep_lexer.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll index 9224cdafe8..8eeb59898f 100644 --- a/tools/coqdep_lexer.mll +++ b/tools/coqdep_lexer.mll @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -46,10 +46,9 @@ } let space = [' ' '\t' '\n' '\r'] -let lowercase = ['a'-'z' '\223'-'\246' '\248'-'\255'] -let uppercase = ['A'-'Z' '\192'-'\214' '\216'-'\222'] -let identchar = - ['A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255' '\'' '0'-'9'] +let lowercase = ['a'-'z'] +let uppercase = ['A'-'Z'] +let identchar = ['A'-'Z' 'a'-'z' '_' '\'' '0'-'9'] let caml_up_ident = uppercase identchar* let caml_low_ident = lowercase identchar* diff --git a/tools/coqdoc/alpha.ml b/tools/coqdoc/alpha.ml index 6a6db95567..961eac6465 100644 --- a/tools/coqdoc/alpha.ml +++ b/tools/coqdoc/alpha.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tools/coqdoc/alpha.mli b/tools/coqdoc/alpha.mli index f6d47a55de..7494f04020 100644 --- a/tools/coqdoc/alpha.mli +++ b/tools/coqdoc/alpha.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml index ef203960b5..325df6137d 100644 --- a/tools/coqdoc/cdglobals.ml +++ b/tools/coqdoc/cdglobals.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tools/coqdoc/cpretty.mli b/tools/coqdoc/cpretty.mli index 58b19184e7..81fdd177c9 100644 --- a/tools/coqdoc/cpretty.mli +++ b/tools/coqdoc/cpretty.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll index 919f37b91b..60a245dc4d 100644 --- a/tools/coqdoc/cpretty.mll +++ b/tools/coqdoc/cpretty.mll @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml index 4d118b9788..8ba6156709 100644 --- a/tools/coqdoc/index.ml +++ b/tools/coqdoc/index.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tools/coqdoc/index.mli b/tools/coqdoc/index.mli index e44bbd593a..490168edbf 100644 --- a/tools/coqdoc/index.mli +++ b/tools/coqdoc/index.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml index fe4387381d..4c8e39bc27 100644 --- a/tools/coqdoc/main.ml +++ b/tools/coqdoc/main.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 9723905790..5c0d2a39b0 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tools/coqdoc/output.mli b/tools/coqdoc/output.mli index 235f2588c8..efc7058950 100644 --- a/tools/coqdoc/output.mli +++ b/tools/coqdoc/output.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tools/coqdoc/tokens.ml b/tools/coqdoc/tokens.ml index b6a1057aa8..12e92614e4 100644 --- a/tools/coqdoc/tokens.ml +++ b/tools/coqdoc/tokens.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tools/coqdoc/tokens.mli b/tools/coqdoc/tokens.mli index f07efedf9e..2972113895 100644 --- a/tools/coqdoc/tokens.mli +++ b/tools/coqdoc/tokens.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tools/coqmktop.ml b/tools/coqmktop.ml index 9bca135127..30e098df59 100644 --- a/tools/coqmktop.ml +++ b/tools/coqmktop.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tools/coqwc.mll b/tools/coqwc.mll index cd07d4216f..a0b6bfbbed 100644 --- a/tools/coqwc.mll +++ b/tools/coqwc.mll @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tools/coqworkmgr.ml b/tools/coqworkmgr.ml index b8e69d6c6d..e1d1c60d72 100644 --- a/tools/coqworkmgr.ml +++ b/tools/coqworkmgr.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml index 4dad16fd8c..a9da27ba23 100644 --- a/tools/fake_ide.ml +++ b/tools/fake_ide.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -293,15 +293,28 @@ let usage () = module Coqide = Spawn.Sync(struct end) let main = - Sys.set_signal Sys.sigpipe + if Sys.os_type = "Unix" then Sys.set_signal Sys.sigpipe (Sys.Signal_handle (fun _ -> prerr_endline "Broken Pipe (coqtop died ?)"; exit 1)); let def_args = ["--xml_format=Ppcmds"; "-ideslave"] in - let coqtop_name, coqtop_args, input_file = match Sys.argv with - | [| _; f |] -> "coqtop", Array.of_list def_args, f + let coqtop_name = (* from ide/ideutils.ml *) + let prog_name = "fake_ide" in + let len_prog_name = String.length prog_name in + let fake_ide_path = Sys.executable_name in + let fake_ide_path_len = String.length fake_ide_path in + let pos = fake_ide_path_len - len_prog_name in + let rex = Str.regexp_string prog_name in + try + let i = Str.search_backward rex fake_ide_path pos in + String.sub fake_ide_path 0 i ^ "coqtop" ^ + String.sub fake_ide_path (i + len_prog_name) + (fake_ide_path_len - i - len_prog_name) + with Not_found -> assert false in + let coqtop_args, input_file = match Sys.argv with + | [| _; f |] -> Array.of_list def_args, f | [| _; f; ct |] -> let ct = Str.split (Str.regexp " ") ct in - List.hd ct, Array.of_list (def_args @ List.tl ct), f + Array.of_list (def_args @ ct), f | _ -> usage () in let inc = if input_file = "-" then stdin else open_in input_file in let coq = diff --git a/tools/gallina.ml b/tools/gallina.ml index 0bf98a8f0f..7a29c6cf5e 100644 --- a/tools/gallina.ml +++ b/tools/gallina.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tools/gallina_lexer.mll b/tools/gallina_lexer.mll index 432b18e645..3e118b85fd 100644 --- a/tools/gallina_lexer.mll +++ b/tools/gallina_lexer.mll @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tools/make-both-single-timing-files.py b/tools/make-both-single-timing-files.py new file mode 100755 index 0000000000..2d33503c36 --- /dev/null +++ b/tools/make-both-single-timing-files.py @@ -0,0 +1,18 @@ +#!/usr/bin/env python +import sys +from TimeFileMaker import * + +if __name__ == '__main__': + USAGE = 'Usage: %s 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''' + if len(sys.argv) < 3 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: + left_dict = get_single_file_times(sys.argv[1]) + right_dict = get_single_file_times(sys.argv[2]) + table = make_diff_table_string(left_dict, right_dict, tag="Code") + print_or_write_table(table, sys.argv[3:]) diff --git a/tools/make-both-time-files.py b/tools/make-both-time-files.py new file mode 100755 index 0000000000..69ec5a6631 --- /dev/null +++ b/tools/make-both-time-files.py @@ -0,0 +1,22 @@ +#!/usr/bin/env python +import sys +from TimeFileMaker import * + +if __name__ == '__main__': + USAGE = 'Usage: %s 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...) +''' + if len(sys.argv) < 3 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: + left_dict = get_times(sys.argv[1]) + right_dict = get_times(sys.argv[2]) + table = make_diff_table_string(left_dict, right_dict) + print_or_write_table(table, sys.argv[3:]) diff --git a/tools/make-one-time-file.py b/tools/make-one-time-file.py new file mode 100755 index 0000000000..e66136df9d --- /dev/null +++ b/tools/make-one-time-file.py @@ -0,0 +1,21 @@ +#!/usr/bin/env python +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:]) diff --git a/tools/ocamllibdep.mll b/tools/ocamllibdep.mll index 5d11e30089..308bb582ac 100644 --- a/tools/ocamllibdep.mll +++ b/tools/ocamllibdep.mll @@ -20,10 +20,9 @@ } let space = [' ' '\t' '\n' '\r'] -let lowercase = ['a'-'z' '\223'-'\246' '\248'-'\255'] -let uppercase = ['A'-'Z' '\192'-'\214' '\216'-'\222'] -let identchar = - ['A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255' '\'' '0'-'9'] +let lowercase = ['a'-'z'] +let uppercase = ['A'-'Z'] +let identchar = ['A'-'Z' 'a'-'z' '_' '\'' '0'-'9'] let caml_up_ident = uppercase identchar* let caml_low_ident = lowercase identchar* |