diff options
32 files changed, 607 insertions, 24 deletions
diff --git a/.gitignore b/.gitignore index 5340f081d..71de7bb8d 100644 --- a/.gitignore +++ b/.gitignore @@ -9,6 +9,7 @@ *.spot *.o *.a +*.pyc *.log *.aux *.dvi @@ -35,6 +36,10 @@ *.tacind *.v.tex *.v.ps +*.v.timing +*.v.timing.diff +*.v.before-timing +*.v.after-timing *.v.html *.stamp *.native @@ -55,6 +60,10 @@ plugins/micromega/csdpcert plugins/micromega/.micromega.ml.generated kernel/byterun/dllcoqrun.so coqdoc.sty +time-of-build.log +time-of-build-pretty.log +time-of-build-before.log +time-of-build-after.log .csdp.cache test-suite/.lia.cache test-suite/.nra.cache @@ -63,8 +72,9 @@ test-suite/misc/universes/all_stdlib.v test-suite/misc/universes/universes.txt test-suite/coq-makefile/*/actual test-suite/coq-makefile/*/desired -test-suite/coq-makefile/*/Makefile -test-suite/coq-makefile/*/Makefile.conf +test-suite/coq-makefile/**/*.processed +test-suite/coq-makefile/**/Makefile +test-suite/coq-makefile/**/Makefile.conf test-suite/coq-makefile/*/src test-suite/coq-makefile/*/theories test-suite/coq-makefile/*/theories2 diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index e1feabd06..95928d7bd 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -21,6 +21,8 @@ variables: COMPILER_BLEEDING_EDGE: "4.04.1" CAMLP5_VER_BLEEDING_EDGE: "6.17" + TEST_PACKAGES: "time python" + COQIDE_PACKAGES: "libgtk2.0-dev libgtksourceview2.0-dev" #COQIDE_PACKAGES_32BIT: "libgtk2.0-dev:i386 libgtksourceview2.0-dev:i386" COQIDE_OPAM: "lablgtk-extras" @@ -193,6 +195,8 @@ test-suite: <<: *test-suite-template dependencies: - build + variables: + EXTRA_PACKAGES: "$TEST_PACKAGES" test-suite:32bit: <<: *test-suite-template @@ -200,7 +204,7 @@ test-suite:32bit: - build:32bit variables: COMPILER: "$COMPILER_32BIT" - EXTRA_PACKAGES: "gcc-multilib" + EXTRA_PACKAGES: "gcc-multilib $TEST_PACKAGES" test-suite:bleeding-edge: <<: *test-suite-template @@ -209,6 +213,7 @@ test-suite:bleeding-edge: variables: COMPILER: "$COMPILER_BLEEDING_EDGE" CAMLP5_VER: "$CAMLP5_VER_BLEEDING_EDGE" + EXTRA_PACKAGES: "$TEST_PACKAGES" documentation: <<: *documentation-template @@ -17,7 +17,7 @@ # read # http://miller.emu.id.au/pmiller/books/rmch/ # before complaining. -# +# # When you are working in a subdir, you can compile without moving to the # upper directory using "make -C ..", and the output is still understood # by Emacs' next-error. @@ -168,7 +168,7 @@ Makefile $(wildcard Makefile.*) config/Makefile : ; # Cleaning ########################################################################### -.PHONY: clean cleankeepvo objclean cruftclean indepclean docclean archclean optclean clean-ide ml4clean depclean cleanconfig distclean voclean devdocclean +.PHONY: clean cleankeepvo objclean cruftclean indepclean docclean archclean optclean clean-ide ml4clean depclean cleanconfig distclean voclean timingclean devdocclean clean: objclean cruftclean depclean docclean devdocclean @@ -239,16 +239,19 @@ cacheclean: cleanconfig: rm -f config/Makefile config/coq_config.ml myocamlbuild_config.ml dev/ocamldebug-coq dev/camlp4.dbg config/Info-*.plist -distclean: clean cleanconfig cacheclean +distclean: clean cleanconfig cacheclean timingclean voclean: find theories plugins test-suite \( -name '*.vo' -o -name '*.glob' -o -name "*.cmxs" -o -name "*.native" -o -name "*.cmx" -o -name "*.cmi" -o -name "*.o" \) -delete find theories plugins test-suite -name .coq-native -empty -delete +timingclean: + find theories plugins test-suite \( -name '*.v.timing' -o -name '*.v.before-timing' -o -name "*.v.after-timing" -o -name "*.v.timing.diff" -o -name "time-of-build.log" -o -name "time-of-build-before.log" -o -name "time-of-build-after.log" -o -name "time-of-build-pretty.log" -o -name "time-of-build-both.log" \) -delete + devdocclean: find . -name '*.dep.ps' -o -name '*.dot' | xargs rm -f - rm -f $(OCAMLDOCDIR)/*.log $(OCAMLDOCDIR)/*.aux $(OCAMLDOCDIR)/*.toc - rm -f $(OCAMLDOCDIR)/ocamldoc.sty $(OCAMLDOCDIR)/coq.tex + rm -f $(OCAMLDOCDIR)/*.log $(OCAMLDOCDIR)/*.aux $(OCAMLDOCDIR)/*.toc + rm -f $(OCAMLDOCDIR)/ocamldoc.sty $(OCAMLDOCDIR)/coq.tex rm -f $(OCAMLDOCDIR)/html/*.html ########################################################################### @@ -299,4 +302,3 @@ printenv: @env | wc -L @echo -n "Total (win32 limit is 32k) : " @env | wc -m - diff --git a/Makefile.build b/Makefile.build index 3f870ed17..2179bafe3 100644 --- a/Makefile.build +++ b/Makefile.build @@ -34,6 +34,12 @@ TIMED ?= # it could be set to "'/usr/bin/time -p'". TIMECMD ?= +# When non-empty, -time is passed to coqc and the output is recorded +# in a timing file for each .v file. If set to "before" or "after", +# the file name for foo.v is foo.v.$(TIMING)-timing; otherwise, it is +# foo.v.timing +TIMING ?= + # Non-empty skips the update of all dependency .d files: NO_RECALC_DEPS ?= @@ -43,6 +49,16 @@ VALIDATE ?= # Is "-xml" when building XML library: COQ_XML ?= +# 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 +BEFORE ?= +AFTER ?= + ########################################################################### # Default starting rule ########################################################################### @@ -53,6 +69,9 @@ world: coq coqide documentation revision coq: coqlib coqbinaries tools +world.timing.diff: coq.timing.diff +coq.timing.diff: coqlib.timing.diff + # Note: 'world' does not build the bytecode binaries anymore. # For that, you can use the 'byte' rule. Native and byte compilations # shouldn't be done in a same make -j... run, otherwise both ocamlc and @@ -60,7 +79,7 @@ coq: coqlib coqbinaries tools byte: coqbyte coqide-byte pluginsbyte printers -.PHONY: world coq byte +.PHONY: world coq byte world.timing.diff coq.timing.diff ########################################################################### # Includes @@ -78,6 +97,53 @@ include Makefile.install include Makefile.dev ## provides the 'printers' and 'revision' rules ########################################################################### +# Timing targets +########################################################################### +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 $(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 make-pretty-timed + $(HIDE)$(MAKE) --no-print-directory print-pretty-timed +.PHONY: pretty-timed make-pretty-timed make-pretty-timed-before make-pretty-timed-after print-pretty-timed print-pretty-timed-diff + +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 + +########################################################################### # This include below will lauch the build of all .d. # The - at front is for disabling warnings about currently missing ones. @@ -616,18 +682,28 @@ OCAMLDEP = $(OCAMLFIND) ocamldep -slash -ml-synonym .ml4 -ml-synonym .mlpack # since they are all mentioned in at least one Declare ML Module in some .v coqlib: theories plugins +coqlib.timing.diff: theories.timing.diff plugins.timing.diff theories: $(THEORIESVO) plugins: $(PLUGINSVO) -.PHONY: coqlib theories plugins +theories.timing.diff: $(THEORIESVO:.vo=.v.timing.diff) +plugins.timing.diff: $(PLUGINSVO:.vo=.v.timing.diff) + +.PHONY: coqlib theories plugins coqlib.timing.diff theories.timing.diff plugins.timing.diff # The .vo files in Init are built with the -noinit option +ifneq (,$(TIMING)) +TIMING_EXTRA = > $<.$(TIMING_EXT) +else +TIMING_EXTRA = +endif + theories/Init/%.vo theories/Init/%.glob: theories/Init/%.v $(VO_TOOLS_DEP) $(SHOW)'COQC $(COQ_XML) -noinit $<' $(HIDE)rm -f theories/Init/$*.glob - $(HIDE)$(BOOTCOQC) $< $(COQ_XML) -noinit -R theories Coq + $(HIDE)$(BOOTCOQC) $< $(COQ_XML) -noinit -R theories Coq $(TIMING_ARG) $(TIMING_EXTRA) # MExtraction.v generates the ml core file of the micromega tactic. # We check that this generated code is still in sync with the version @@ -654,13 +730,18 @@ $(MICROMEGAV:.v=.vo) $(MICROMEGAV:.v=.glob) : $(MICROMEGAV) theories/Init/Prelud %.vo %.glob: %.v theories/Init/Prelude.vo $(VO_TOOLS_DEP) $(SHOW)'COQC $<' $(HIDE)rm -f $*.glob - $(HIDE)$(BOOTCOQC) $< + $(HIDE)$(BOOTCOQC) $< $(TIMING_ARG) $(TIMING_EXTRA) ifdef VALIDATE $(SHOW)'COQCHK $(call vo_to_mod,$@)' $(HIDE)$(CHICKEN) -boot -silent -norec $(call vo_to_mod,$@) \ || ( RV=$$?; rm -f "$@"; exit $${RV} ) endif +%.v.timing.diff: %.v.before-timing %.v.after-timing + $(SHOW)PYTHON TIMING-DIFF $< + $(HIDE)$(MAKE) --no-print-directory print-pretty-single-time-diff BEFORE=$*.v.before-timing AFTER=$*.v.after-timing TIME_OF_PRETTY_BUILD_FILE="$@" + + # Dependencies of .v files %.v.d: $(D_DEPEND_BEFORE_SRC) %.v $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) diff --git a/Makefile.common b/Makefile.common index 100698321..85ecb1a08 100644 --- a/Makefile.common +++ b/Makefile.common @@ -12,7 +12,7 @@ # Executables ########################################################################### -COQMKTOP:=bin/coqmktop$(EXE) +COQMKTOP:=bin/coqmktop$(EXE) COQTOPBYTE:=bin/coqtop.byte$(EXE) COQTOPEXE:=bin/coqtop$(EXE) @@ -25,9 +25,15 @@ COQWC:=bin/coqwc$(EXE) COQDOC:=bin/coqdoc$(EXE) COQC:=bin/coqc$(EXE) COQWORKMGR:=bin/coqworkmgr$(EXE) +COQMAKE_ONE_TIME_FILE:=tools/make-one-time-file.py +COQTIME_FILE_MAKER:=tools/TimeFileMaker.py +COQMAKE_BOTH_TIME_FILES:=tools/make-both-time-files.py +COQMAKE_BOTH_SINGLE_TIMING_FILES:=tools/make-both-single-timing-files.py TOOLS:=$(COQDEP) $(COQMAKEFILE) $(GALLINA) $(COQTEX) $(COQWC) $(COQDOC) $(COQC)\ $(COQWORKMGR) +TOOLS_HELPERS:=tools/CoqMakefile.in $(COQMAKE_ONE_TIME_FILE) $(COQTIME_FILE_MAKER)\ + $(COQMAKE_BOTH_TIME_FILES) $(COQMAKE_BOTH_SINGLE_TIMING_FILES) COQDEPBOOT:=bin/coqdep_boot$(EXE) OCAMLLIBDEP:=bin/ocamllibdep$(EXE) @@ -64,7 +70,7 @@ DYNLIB:=.cma endif INSTALLBIN:=install -INSTALLLIB:=install -m 644 +INSTALLLIB:=install -m 644 INSTALLSH:=./install.sh MKDIR:=install -d @@ -191,7 +197,7 @@ LIBFILES:=$(ALLVO) $(call vo_to_cm,$(ALLVO)) \ $(call vo_to_obj,$(ALLVO)) \ $(VFILES) $(GLOBFILES) -# For emacs: -# Local Variables: -# mode: makefile +# For emacs: +# Local Variables: +# mode: makefile # End: diff --git a/Makefile.install b/Makefile.install index 4a3227620..02ae724df 100644 --- a/Makefile.install +++ b/Makefile.install @@ -107,7 +107,7 @@ install-devfiles: $(MKDIR) $(FULLCOQLIB) $(INSTALLSH) $(FULLCOQLIB) $(GRAMMARCMA) $(INSTALLSH) $(FULLCOQLIB) $(INSTALLCMI) - $(INSTALLSH) $(FULLCOQLIB) tools/CoqMakefile.in + $(INSTALLSH) $(FULLCOQLIB) $(TOOLS_HELPERS) ifeq ($(BEST),opt) $(INSTALLSH) $(FULLCOQLIB) $(LINKCMX) $(CORECMA:.cma=.a) $(STATICPLUGINS:.cma=.a) endif diff --git a/install.sh b/install.sh index c5835b014..f8589a3c7 100755 --- a/install.sh +++ b/install.sh @@ -8,7 +8,7 @@ for f; do dn=`dirname $f` install -d "$dest/$dn" case $bn in - *.cmxs) install -m 755 $f "$dest/$dn/$bn" + *.cmxs|*.py) install -m 755 $f "$dest/$dn/$bn" ;; *) install -m 644 $f "$dest/$dn/$bn" ;; diff --git a/test-suite/coq-makefile/timing/after/Fast.v b/test-suite/coq-makefile/timing/after/Fast.v new file mode 100644 index 000000000..54d3cfc3e --- /dev/null +++ b/test-suite/coq-makefile/timing/after/Fast.v @@ -0,0 +1,4 @@ +Require Coq.ZArith.BinInt. +Definition foo0 := Eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl. +Definition foo1 := Eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl. +Definition foo2 := Eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl. diff --git a/test-suite/coq-makefile/timing/after/Slow.v b/test-suite/coq-makefile/timing/after/Slow.v new file mode 100644 index 000000000..8b1378917 --- /dev/null +++ b/test-suite/coq-makefile/timing/after/Slow.v @@ -0,0 +1 @@ + diff --git a/test-suite/coq-makefile/timing/after/_CoqProject b/test-suite/coq-makefile/timing/after/_CoqProject new file mode 100644 index 000000000..36c3a18c2 --- /dev/null +++ b/test-suite/coq-makefile/timing/after/_CoqProject @@ -0,0 +1,2 @@ +Slow.v +Fast.v diff --git a/test-suite/coq-makefile/timing/after/time-of-build-after.log.desired b/test-suite/coq-makefile/timing/after/time-of-build-after.log.desired new file mode 100644 index 000000000..729de2f36 --- /dev/null +++ b/test-suite/coq-makefile/timing/after/time-of-build-after.log.desired @@ -0,0 +1,16 @@ +Makefile:69: warning: undefined variable '*' +Makefile:204: warning: undefined variable 'DSTROOT' +COQDEP Fast.v +COQDEP Slow.v +Makefile:69: warning: undefined variable '*' +Makefile:204: warning: undefined variable 'DSTROOT' +Makefile:69: warning: undefined variable '*' +Makefile:204: warning: undefined variable 'DSTROOT' +Makefile:69: warning: undefined variable '*' +Makefile:204: warning: undefined variable 'DSTROOT' +COQC Slow.v +Slow (real: 0.04, user: 0.02, sys: 0.01, mem: 45512 ko) +COQC Fast.v +Fast (real: 0.41, user: 0.37, sys: 0.04, mem: 395200 ko) +Makefile:69: warning: undefined variable '*' +Makefile:204: warning: undefined variable 'DSTROOT' diff --git a/test-suite/coq-makefile/timing/after/time-of-build-before.log.desired b/test-suite/coq-makefile/timing/after/time-of-build-before.log.desired new file mode 100644 index 000000000..b25bc3683 --- /dev/null +++ b/test-suite/coq-makefile/timing/after/time-of-build-before.log.desired @@ -0,0 +1,16 @@ +Makefile:69: warning: undefined variable '*' +Makefile:204: warning: undefined variable 'DSTROOT' +COQDEP Fast.v +COQDEP Slow.v +Makefile:69: warning: undefined variable '*' +Makefile:204: warning: undefined variable 'DSTROOT' +Makefile:69: warning: undefined variable '*' +Makefile:204: warning: undefined variable 'DSTROOT' +Makefile:69: warning: undefined variable '*' +Makefile:204: warning: undefined variable 'DSTROOT' +COQC Slow.v +Slow (real: 0.40, user: 0.35, sys: 0.04, mem: 394968 ko) +COQC Fast.v +Fast (real: 0.04, user: 0.03, sys: 0.00, mem: 46564 ko) +Makefile:69: warning: undefined variable '*' +Makefile:204: warning: undefined variable 'DSTROOT' diff --git a/test-suite/coq-makefile/timing/after/time-of-build-both.log.desired b/test-suite/coq-makefile/timing/after/time-of-build-both.log.desired new file mode 100644 index 000000000..56815d241 --- /dev/null +++ b/test-suite/coq-makefile/timing/after/time-of-build-both.log.desired @@ -0,0 +1,6 @@ +After | File Name | Before || Change | % Change +-------------------------------------------------------- +0m00.38s | Total | 0m00.39s || -0m00.01s | -2.56% +-------------------------------------------------------- +0m00.35s | Slow | 0m00.02s || +0m00.32s | +1649.99% +0m00.03s | Fast | 0m00.37s || -0m00.34s | -91.89%
\ No newline at end of file diff --git a/test-suite/coq-makefile/timing/aggregate/Fast.v b/test-suite/coq-makefile/timing/aggregate/Fast.v new file mode 100644 index 000000000..8b1378917 --- /dev/null +++ b/test-suite/coq-makefile/timing/aggregate/Fast.v @@ -0,0 +1 @@ + diff --git a/test-suite/coq-makefile/timing/aggregate/Slow.v b/test-suite/coq-makefile/timing/aggregate/Slow.v new file mode 100644 index 000000000..54d3cfc3e --- /dev/null +++ b/test-suite/coq-makefile/timing/aggregate/Slow.v @@ -0,0 +1,4 @@ +Require Coq.ZArith.BinInt. +Definition foo0 := Eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl. +Definition foo1 := Eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl. +Definition foo2 := Eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl. diff --git a/test-suite/coq-makefile/timing/aggregate/_CoqProject b/test-suite/coq-makefile/timing/aggregate/_CoqProject new file mode 100644 index 000000000..36c3a18c2 --- /dev/null +++ b/test-suite/coq-makefile/timing/aggregate/_CoqProject @@ -0,0 +1,2 @@ +Slow.v +Fast.v diff --git a/test-suite/coq-makefile/timing/before/Fast.v b/test-suite/coq-makefile/timing/before/Fast.v new file mode 100644 index 000000000..8b1378917 --- /dev/null +++ b/test-suite/coq-makefile/timing/before/Fast.v @@ -0,0 +1 @@ + diff --git a/test-suite/coq-makefile/timing/before/Slow.v b/test-suite/coq-makefile/timing/before/Slow.v new file mode 100644 index 000000000..54d3cfc3e --- /dev/null +++ b/test-suite/coq-makefile/timing/before/Slow.v @@ -0,0 +1,4 @@ +Require Coq.ZArith.BinInt. +Definition foo0 := Eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl. +Definition foo1 := Eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl. +Definition foo2 := Eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl. diff --git a/test-suite/coq-makefile/timing/before/_CoqProject b/test-suite/coq-makefile/timing/before/_CoqProject new file mode 100644 index 000000000..36c3a18c2 --- /dev/null +++ b/test-suite/coq-makefile/timing/before/_CoqProject @@ -0,0 +1,2 @@ +Slow.v +Fast.v diff --git a/test-suite/coq-makefile/timing/error/A.v b/test-suite/coq-makefile/timing/error/A.v new file mode 100644 index 000000000..932363a12 --- /dev/null +++ b/test-suite/coq-makefile/timing/error/A.v @@ -0,0 +1 @@ +Check I : I. diff --git a/test-suite/coq-makefile/timing/error/_CoqProject b/test-suite/coq-makefile/timing/error/_CoqProject new file mode 100644 index 000000000..790e05713 --- /dev/null +++ b/test-suite/coq-makefile/timing/error/_CoqProject @@ -0,0 +1 @@ +A.v diff --git a/test-suite/coq-makefile/timing/per-file-after/A.v b/test-suite/coq-makefile/timing/per-file-after/A.v new file mode 100644 index 000000000..851e2b973 --- /dev/null +++ b/test-suite/coq-makefile/timing/per-file-after/A.v @@ -0,0 +1,4 @@ +Require Coq.ZArith.BinInt. +Declare Reduction comp := native_compute. +Definition foo0 := Eval comp in (Coq.ZArith.BinInt.Z.div_eucl, Coq.ZArith.BinInt.Z.div_eucl). +Definition foo1 := Eval comp in (foo0, foo0). diff --git a/test-suite/coq-makefile/timing/per-file-after/A.v.timing.diff.desired b/test-suite/coq-makefile/timing/per-file-after/A.v.timing.diff.desired new file mode 100644 index 000000000..18f0f34b2 --- /dev/null +++ b/test-suite/coq-makefile/timing/per-file-after/A.v.timing.diff.desired @@ -0,0 +1,9 @@ +After | Code | Before || Change | % Change +--------------------------------------------------------------------------------------------------- +0m00.50s | Total | 0m04.17s || -0m03.66s | -87.96% +--------------------------------------------------------------------------------------------------- +0m00.145s | Chars 069 - 162 [Definition~foo0~:=~Eval~comp~i...] | 0m00.192s || -0m00.04s | -24.47% +0m00.126s | Chars 000 - 026 [Require~Coq.ZArith.BinInt.] | 0m00.143s || -0m00.01s | -11.88% + N/A | Chars 027 - 068 [Declare~Reduction~comp~:=~nati...] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 027 - 068 [Declare~Reduction~comp~:=~vm_c...] | N/A || +0m00.00s | N/A +0m00.231s | Chars 163 - 208 [Definition~foo1~:=~Eval~comp~i...] | 0m03.836s || -0m03.60s | -93.97%
\ No newline at end of file diff --git a/test-suite/coq-makefile/timing/per-file-after/_CoqProject b/test-suite/coq-makefile/timing/per-file-after/_CoqProject new file mode 100644 index 000000000..790e05713 --- /dev/null +++ b/test-suite/coq-makefile/timing/per-file-after/_CoqProject @@ -0,0 +1 @@ +A.v diff --git a/test-suite/coq-makefile/timing/per-file-before/A.v b/test-suite/coq-makefile/timing/per-file-before/A.v new file mode 100644 index 000000000..115c1f95b --- /dev/null +++ b/test-suite/coq-makefile/timing/per-file-before/A.v @@ -0,0 +1,4 @@ +Require Coq.ZArith.BinInt. +Declare Reduction comp := vm_compute. +Definition foo0 := Eval comp in (Coq.ZArith.BinInt.Z.div_eucl, Coq.ZArith.BinInt.Z.div_eucl). +Definition foo1 := Eval comp in (foo0, foo0). diff --git a/test-suite/coq-makefile/timing/per-file-before/_CoqProject b/test-suite/coq-makefile/timing/per-file-before/_CoqProject new file mode 100644 index 000000000..790e05713 --- /dev/null +++ b/test-suite/coq-makefile/timing/per-file-before/_CoqProject @@ -0,0 +1 @@ +A.v diff --git a/test-suite/coq-makefile/timing/run.sh b/test-suite/coq-makefile/timing/run.sh new file mode 100755 index 000000000..9786af10a --- /dev/null +++ b/test-suite/coq-makefile/timing/run.sh @@ -0,0 +1,68 @@ +#!/usr/bin/env bash + +#set -x +set -e + +. ../template/init.sh + +cd error +coq_makefile -f _CoqProject -o Makefile +make cleanall +if make pretty-timed TGTS="all" -j1; then + echo "Error: make pretty-timed should have failed" + exit 1 +fi + +cd ../aggregate +coq_makefile -f _CoqProject -o Makefile +make cleanall +make pretty-timed TGTS="all" -j1 || exit $? + +cd ../before +coq_makefile -f _CoqProject -o Makefile +make cleanall +make make-pretty-timed-before TGTS="all" -j1 || exit $? + +cd ../after +coq_makefile -f _CoqProject -o Makefile +make cleanall +make make-pretty-timed-after TGTS="all" -j1 || exit $? +rm -f time-of-build-before.log +make print-pretty-timed-diff TIME_OF_BUILD_BEFORE_FILE=../before/time-of-build-before.log +cp ../before/time-of-build-before.log ./ +make print-pretty-timed-diff || exit $? + +for ext in "" .desired; do + for file in time-of-build-before.log time-of-build-after.log time-of-build-both.log; do + cat ${file}${ext} | grep -v 'warning: undefined variable' | sed s'/[0-9]//g' | sed s'/ *$//g' | sed s'/^-*$/------/g' | sed s'/ */ /g' | sed s'/\(Total.*\)-\(.*\)-/\1+\2+/g' > ${file}${ext}.processed + done +done +for file in time-of-build-before.log time-of-build-after.log time-of-build-both.log; do + diff -u $file.desired.processed $file.processed || exit $? +done + +cd ../per-file-before +coq_makefile -f _CoqProject -o Makefile +make cleanall +make all TIMING=before -j2 || exit $? + +cd ../per-file-after +coq_makefile -f _CoqProject -o Makefile +make cleanall +make all TIMING=after -j2 || exit $? + +find ../per-file-before/ -name "*.before-timing" -exec 'cp' '{}' './' ';' +make all.timing.diff -j2 || exit $? +cat A.v.timing.diff +echo + +for ext in "" .desired; do + for file in A.v.timing.diff; do + cat ${file}${ext} | sed s'/[0-9]*\.[0-9]*//g' | sed s'/0//g' | sed s'/ */ /g' | sed s'/+/-/g' | sort > ${file}${ext}.processed + done +done +for file in A.v.timing.diff; do + diff -u $file.desired.processed $file.processed || exit $? +done + +exit 0 diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index e4f527d44..7d281977a 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 @@ -86,6 +87,11 @@ COQDEP ?= "$(COQBIN)coqdep" GALLINA ?= "$(COQBIN)gallina" COQDOC ?= "$(COQBIN)coqdoc" COQMKTOP ?= "$(COQBIN)coqmktop" +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 @@ -102,7 +108,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 @@ -171,6 +185,21 @@ 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) @@ -270,6 +299,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 @@ -286,6 +350,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 @@ -459,13 +526,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:: @@ -534,9 +607,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 @@ -546,6 +625,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 $< @@ -572,7 +655,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),) diff --git a/tools/TimeFileMaker.py b/tools/TimeFileMaker.py new file mode 100644 index 000000000..a207c2171 --- /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/make-both-single-timing-files.py b/tools/make-both-single-timing-files.py new file mode 100755 index 000000000..2d33503c3 --- /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 000000000..69ec5a663 --- /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 000000000..e66136df9 --- /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:]) |