diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2017-08-07 18:35:30 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-08-07 18:35:30 -0700 |
| commit | e73457b4f243ea1a68d14486918e53d5d88f065d (patch) | |
| tree | ad7cc1744fc00cd04534523410539d461aa4fb33 | |
| parent | 6eee137dc64e3f2c467d70edf2bb18abd6b3b071 (diff) | |
Optionally split regression tests into test groups (#207)
To prevent timing out on Travis, this commit adds the option to split
the regression tests into groups and run each group in a separate job.
The group of a test is determined by computing a checksum of its name.
| -rw-r--r-- | .travis.yml | 4 | ||||
| -rwxr-xr-x | test/regress/run_regression | 18 |
2 files changed, 20 insertions, 2 deletions
diff --git a/.travis.yml b/.travis.yml index 6ef64f0e2..47fc617c2 100644 --- a/.travis.yml +++ b/.travis.yml @@ -15,9 +15,11 @@ env: # The next declaration is the encrypted COVERITY_SCAN_TOKEN, created # via the "travis encrypt" command using the project repo's public key - secure: "fRfdzYwV10VeW5tVSvy5qpR8ZlkXepR7XWzCulzlHs9SRI2YY20BpzWRjyMBiGu2t7IeJKT7qdjq/CJOQEM8WS76ON7QJ1iymKaRDewDs3OhyPJ71fsFKEGgLky9blk7I9qZh23hnRVECj1oJAVry9IK04bc2zyIEjUYpjRkUAQ=" + - TEST_GROUPS=2 matrix: - TRAVIS_CVC4=yes TRAVIS_CVC4_CHECK_PORTFOLIO=yes TRAVIS_CVC4_CONFIG='production --enable-language-bindings=java,c --enable-proof --with-portfolio' - - TRAVIS_CVC4=yes TRAVIS_CVC4_CHECK_PORTFOLIO=yes TRAVIS_CVC4_CONFIG='debug --enable-language-bindings=java,c --enable-proof --with-portfolio' + - TRAVIS_CVC4=yes TRAVIS_CVC4_CHECK_PORTFOLIO=yes TRAVIS_CVC4_CONFIG='debug --enable-language-bindings=java,c --enable-proof --with-portfolio' TEST_GROUP=0 + - TRAVIS_CVC4=yes TRAVIS_CVC4_CHECK_PORTFOLIO=yes TRAVIS_CVC4_CONFIG='debug --enable-language-bindings=java,c --enable-proof --with-portfolio' TEST_GROUP=1 - TRAVIS_CVC4=yes TRAVIS_CVC4_CONFIG='--disable-proof' - TRAVIS_CVC4=yes TRAVIS_CVC4_DISTCHECK=yes TRAVIS_CVC4_CONFIG='--enable-proof' - TRAVIS_LFSC=yes diff --git a/test/regress/run_regression b/test/regress/run_regression index 5bc46d4f9..f6dc00b3f 100755 --- a/test/regress/run_regression +++ b/test/regress/run_regression @@ -5,10 +5,16 @@ # # usage: # -# run_regression cvc4-binary [ --proof | --dump ] [ benchmark.cvc | benchmark.smt | benchmark.smt2 ] +# run_regression [ --proof | --dump ] [ wrapper ] cvc4-binary [ benchmark.cvc | benchmark.smt | benchmark.smt2 | benchmark.p ] # # Runs benchmark and checks for correct exit status and output. # +# The TEST_GROUP and TEST_GROUPS environment variables can be used to split the +# benchmarks into groups and only run one of the groups. The benchmarks are +# associated with a group based on a hash of their name. TEST_GROUPS controls +# how many groups are created while TEST_GROUP specifies the group to run. +# Currently, the primary use case for this is to split the benchmarks across +# multiple Travis jobs. # ulimit -t 1 # For detecting long running regressions ulimit -s 65000 # Needed for some (esp. portfolio and model-building) @@ -49,6 +55,16 @@ cvc4=$1 benchmark_orig=$2 benchmark="$benchmark_orig" +if [ -n "$TEST_GROUP" ]; then + # Use the checksum of the benchmark name to determine the group of the + # benchmark + benchmark_group=$(( $(echo "$benchmark" | cksum | cut -d " " -f1) % $TEST_GROUPS )) + if (( $benchmark_group != $TEST_GROUP )); then + # Skip the benchmark if it is not in the expected test group + exit 77 + fi +fi + function error { echo "$prog: error: $*" exit 1 |