Stream: Coq devs & plugin devs

Topic: test suite timeouts in CI

view this post on Zulip Gaëtan Gilbert (Sep 25 2023 at 14:26):

test-suite:base usually takes around 30min (eg https://gitlab.com/coq/coq/-/jobs/4981022166)
but sometimes it hits the 1h timeout (eg https://gitlab.inria.fr/coq/coq/-/jobs/3448538)
how can we investigate this variance?
cc @Thierry Martinez

view this post on Zulip Jason Gross (Sep 27 2023 at 20:17):

Can we make use of TIMED=1 and get a target that prints out the timing table for the test-suite a la make-pretty-timed and print-pretty-timed of coq_makefile

view this post on Zulip Gaëtan Gilbert (Sep 27 2023 at 20:46):

interesting idea
the test suite isn't a coq_makefile project so it would need a fresh implementation though

view this post on Zulip Jason Gross (Sep 27 2023 at 21:12):

If TIMED=1 works, the other targets would be pretty minimal. The variables to define are:

COQMAKE_ONE_TIME_FILE ?= "$(COQCORELIB)/tools/make-one-time-file.py"
# Option for changing sorting of timing output file
TIMING_SORT_BY ?= auto
# Option for changing the fuzz parameter on the output file
TIMING_FUZZ ?= 0
# Option for changing whether to use real or user time for timing tables
TIMING_REAL?=
# Option for including the memory column(s)
TIMING_INCLUDE_MEM?=
# Option for sorting by the memory column
TIMING_SORT_BY_MEM?=

TIME_OF_BUILD_FILE               ?= time-of-build.log
TIME_OF_PRETTY_BUILD_FILE        ?= time-of-build-pretty.log

TGTS ?=

ifeq (0,$(TIMING_REAL))
TIMING_REAL_ARG :=
TIMING_USER_ARG := --user
else
ifeq (1,$(TIMING_REAL))
TIMING_REAL_ARG := --real
TIMING_USER_ARG :=
else
TIMING_REAL_ARG :=
TIMING_USER_ARG :=
endif
endif

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

and the targets are

make-pretty-timed::
    $(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) $(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)
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 print-pretty-timed

and then we'd just invoke it as make -C test-suite pretty-timed TGTS="<whatever>"

Last updated: Dec 05 2023 at 09:01 UTC