From 5e941d5ece705b4416f1d7fe6fd6650f89840518 Mon Sep 17 00:00:00 2001 From: Thomas Hader Date: Mon, 12 Feb 2024 16:24:03 -0800 Subject: [PATCH 01/15] Split test in two scripts --- tests/regress/check.sh | 181 +++++++----------------------------- tests/regress/run_test.sh | 188 ++++++++++++++++++++++++++++++++++++++ 2 files changed, 222 insertions(+), 147 deletions(-) create mode 100644 tests/regress/run_test.sh diff --git a/tests/regress/check.sh b/tests/regress/check.sh index e2870e180..a2e838cc8 100755 --- a/tests/regress/check.sh +++ b/tests/regress/check.sh @@ -38,20 +38,20 @@ usage() { echo "Usage: $0 [test1] [test2] ..." exit } - -smt2_options= - -while getopts "s:" o; do - case "$o" in - s) - smt2_options=${OPTARG} - ;; - *) - usage - ;; - esac -done -shift $((OPTIND-1)) + +#smt2_options= + +#while getopts "s:" o; do +# case "$o" in +# s) +# smt2_options=${OPTARG} +# ;; +# *) +# usage +# ;; +# esac +#done +#shift $((OPTIND-1)) if test $# "<" 2 ; then usage @@ -62,13 +62,11 @@ bin_dir=$2 shift 2 all_tests="$@" -# Make sure fatal errors go to stderr -export LIBC_FATAL_STDERR_=1 - # # System-dependent configuration +# TODO why? # -os_name=`uname 2>/dev/null` || os_name=unknown +os_name=$(uname 2>/dev/null) || os_name=unknown case "$os_name" in *Darwin* ) @@ -81,50 +79,20 @@ case "$os_name" in esac -# -# We try bash's builtin time command -# -TIMEFORMAT="%U" - - -# -# Output colors -# -red= -green= -black= -if test -t 1 ; then - red=`tput setaf 1` - green=`tput setaf 2` - black=`tput sgr0` -fi - # # The temp file for output # -outfile=`$mktemp_cmd` || { echo "Can't create temp file" ; exit 1 ; } -timefile=`$mktemp_cmd` || { echo "Can't create temp file" ; exit 1 ; } - -fail=0 -pass=0 - -failed_tests=() +logdir=$($mktemp_cmd -d) || { echo "Can't create temp folder" ; exit 1 ; } if [[ -z "$REGRESS_FILTER" ]]; then REGRESS_FILTER="." fi -if [[ -z "$TIME_LIMIT" ]]; -then - TIME_LIMIT=60 -fi - - # # Check if MCSAT is supported # -./$bin_dir/yices_smt2 --mcsat >& /dev/null < /dev/null +./"$bin_dir"/yices_smt2 --mcsat >& /dev/null < /dev/null if [ $? -ne 0 ] then MCSAT_FILTER="-v mcsat" @@ -132,114 +100,33 @@ else MCSAT_FILTER="." fi -if test -z "$all_tests"; then +if [ -z "$all_tests" ] ; then all_tests=$( - find "$regress_dir" -name '*.smt' -or -name '*.smt2' -or -name '*.ys' | + find "$regress_dir" -name '*.smt' -or -name '*.smt2' -or -name '*.ys' | grep $REGRESS_FILTER | grep $MCSAT_FILTER | sort ) fi for file in $all_tests; do - - echo -n $file - - # Get the binary based on the filename - filename=`basename "$file"` - - options= - - case $filename in - *.smt2) - binary=yices_smt2 - options=$smt2_options - ;; - *.smt) - binary=yices_smtcomp - ;; - *.ys) - binary=yices - ;; - *) - echo FAIL: unknown extension for $filename - fail=`expr $fail + 1` - continue - esac - - # Get the options - if [ -e "$file.options" ] - then - options="$options `cat $file.options`" - echo " [ $options ]" - test_string="$file [ $options ]" - else - test_string="$file" - echo - fi - - # Get the expected result - if [ -e "$file.gold" ] - then - gold=$file.gold - else - echo -n $red - echo FAIL: missing file: $file.gold - echo -n $black - fail=`expr $fail + 1` - failed_tests+=("$test_string") - continue - fi - - # Run the binary - ( - ulimit -S -t $TIME_LIMIT &> /dev/null - ulimit -H -t $((1+$TIME_LIMIT)) &> /dev/null - (time ./$bin_dir/$binary $options ./$file >& $outfile ) >& $timefile - ) - status=$? - thetime=`cat $timefile` - - # Do the diff - DIFF=`diff -w $outfile $gold` - - if [ $? -eq 0 ] && [ $status -eq 0 ] - then - echo -n $green - echo PASS [${thetime} s] - echo -n $black - pass=`expr $pass + 1` - else - echo -n $red - echo FAIL - echo -n $black - fail=`expr $fail + 1` - failed_tests+=("$test_string"$'\n'"$DIFF") - fi - + bash "${BASH_SOURCE%/*}"/run_test.sh "$file" "$bin_dir" "$logdir" done -rm $outfile -rm $timefile +pass=$(find "$logdir" -type f -name "*.pass" | wc -l) +fail=$(find "$logdir" -type f -name "*.error" | wc -l) -if [ $fail -eq 0 ] -then - echo -n $green - echo Pass: $pass - echo Fail: $fail - echo -n $black -else - echo -n $red - echo Pass: $pass - echo Fail: $fail - echo -n $black -fi +echo "Pass: $pass" +echo "Fail: $fail" -if [ $fail -eq 0 ] -then - exit 0 +if [ "$fail" -eq 0 ] ; then + code=0 else - for i in "${!failed_tests[@]}"; do echo "$((i+1)). ${failed_tests[$i]}"; done - exit 1 + for f in "$logdir"/*.error ; do + cat "$f" + echo + done + code=1 fi -echo -n $black +rm -rf "$logdir" +exit $code diff --git a/tests/regress/run_test.sh b/tests/regress/run_test.sh new file mode 100644 index 000000000..2be012654 --- /dev/null +++ b/tests/regress/run_test.sh @@ -0,0 +1,188 @@ +#!/bin/bash + +# +# This file is part of the Yices SMT Solver. +# Copyright (C) 2017 SRI International. +# +# Yices is free software: you can redistribute it and/or modify +# it under the terms of the GNU General Public License as published by +# the Free Software Foundation, either version 3 of the License, or +# (at your option) any later version. +# +# Yices is distributed in the hope that it will be useful, +# but WITHOUT ANY WARRANTY; without even the implied warranty of +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +# GNU General Public License for more details. +# +# You should have received a copy of the GNU General Public License +# along with Yices. If not, see . +# + +# +# Run one single regression tests +# +# Usage: run_test.sh [] +# +# test-file is the test file the SMT1, SMT2, or Yices input language +# bin-dir contains the Yices binaries for each of these languages +# tmp-dir (optional) and specifies the location to put the results +# +# For each test file, the expected results are stored in file.gold +# and command-line options are stored in file.options. +# +# This scripts calls the appropriate binary on each test file, passing it +# the command-line options if any, then check whether the output matches +# what's expected. +# + +usage() { + echo "Usage: $0 [out-dir]" + exit 4 +} + +if [ $# -lt 2 ] ; then + usage +fi + +test_file=$1 +bin_dir=$2 + +if [ $# -ge 3 ] ; then + out_dir=$3 +fi + +export LIBC_FATAL_STDERR_=1 + +# +# System-dependent configuration +# +os_name=$(uname 2>/dev/null) || os_name=unknown + +case "$os_name" in + *Darwin* ) + mktemp_cmd="/usr/bin/mktemp -t out" + ;; + + * ) + mktemp_cmd=mktemp + ;; + +esac + +# +# We try bash's builtin time command +# +TIMEFORMAT="%U" + + +# +# Output colors +# +red= +green= +black= +if test -t 1 ; then + red=$(tput setaf 1) + green=$(tput setaf 2) + black=$(tput sgr0) +fi + +# +# The temp file for output +# +outfile=$($mktemp_cmd) || { echo "Can't create temp file" ; exit 3 ; } +timefile=$($mktemp_cmd) || { echo "Can't create temp file" ; exit 3 ; } + +if [[ -z "$TIME_LIMIT" ]]; +then + TIME_LIMIT=60 +fi + +echo -n "$test_file" + +# Get the binary based on the filename +filename=$(basename "$test_file") + +options= + +case $filename in + *.smt2) + binary=yices_smt2 + #options=$smt2_options + ;; + *.smt) + binary=yices_smtcomp + ;; + *.ys) + binary=yices + ;; + *) + echo FAIL: unknown extension for "$filename" + exit 2 +esac + +# Get the options +if [ -e "$test_file.options" ] +then + options="$options $(cat $test_file.options)" + echo " [ $options ]" + test_string="$test_file [ $options ]" +else + test_string="$test_file" + echo +fi + +# Get the expected result +if [ -e "$test_file.gold" ] +then + gold=$test_file.gold +else + echo -n $red + echo FAIL: missing file: $test_file.gold + echo -n $black + exit 2 +fi + +# Run the binary +( + ulimit -S -t $TIME_LIMIT &> /dev/null + ulimit -H -t $((1+$TIME_LIMIT)) &> /dev/null + (time ./$bin_dir/$binary $options ./$test_file >& $outfile ) >& $timefile +) +status=$? +runtime=$(cat $timefile) + +# Do the diff +DIFF=$(diff -w "$outfile" "$gold") + +rm "$timefile" +rm "$outfile" + +# find log url +if [ -d "$out_dir" ] ; then + # add pid in case there are multiple tests with the same name + log_file="$out_dir/$filename.$BASHPID" +fi + +if [ $? -eq 0 ] && [ $status -eq 0 ] +then + echo -n $green + echo PASS [${runtime} s] + echo -n $black + if [ -n "$log_file" ] ; then + log_file="$log_file.pass" + echo "$test_string" > "$log_file" + fi + exit 0 +else + echo -n $red + echo FAIL + echo -n $black + + if [ -n "$log_file" ] ; then + log_file="$log_file.error" + echo "$test_string" > "$log_file" + echo "$DIFF" >> "$log_file" + fi + exit 1 +fi From c36f47c7c54a42bc70bd60cf6aae14f73b2257cc Mon Sep 17 00:00:00 2001 From: Thomas Hader Date: Mon, 12 Feb 2024 18:34:01 -0800 Subject: [PATCH 02/15] Parallel regression done --- Makefile.build | 4 +-- tests/regress/check.sh | 57 +++++++++++++++++++++++++---------- tests/regress/run_test.sh | 63 ++++++++++++++++++++++----------------- 3 files changed, 78 insertions(+), 46 deletions(-) diff --git a/Makefile.build b/Makefile.build index f1b700e9c..c6a33f859 100644 --- a/Makefile.build +++ b/Makefile.build @@ -309,14 +309,14 @@ regress: build_subdirs version @ echo "=== Building binaries ===" @ $(MAKE) -C $(srcdir) BUILD=../$(build_dir) bin @ echo "=== Running regressions ===" - @ $(regressdir)/check.sh $(regressdir) $(build_dir)/bin + @ $(regressdir)/check.sh -j $(regressdir) $(build_dir)/bin static-regress: static_build_subdirs version @ echo "=== Building binaries ===" @ $(MAKE) -C $(srcdir) BUILD=../$(build_dir) static-bin @ echo "=== Running regressions ===" - @ $(regressdir)/check.sh $(regressdir) $(build_dir)/static_bin + @ $(regressdir)/check.sh -j $(regressdir) $(build_dir)/static_bin .PHONY: all obj static-obj lib static-lib bin static-bin test static-test \ diff --git a/tests/regress/check.sh b/tests/regress/check.sh index a2e838cc8..528efe071 100755 --- a/tests/regress/check.sh +++ b/tests/regress/check.sh @@ -39,19 +39,23 @@ usage() { exit } -#smt2_options= - -#while getopts "s:" o; do -# case "$o" in -# s) -# smt2_options=${OPTARG} -# ;; -# *) -# usage -# ;; -# esac -#done -#shift $((OPTIND-1)) +smt2_options= +use_parallel= + +while getopts "js:" o; do + case "$o" in + s) + smt2_options=${OPTARG} + ;; + j) + use_parallel=yes + ;; + *) + usage + ;; + esac +done +shift $((OPTIND-1)) if test $# "<" 2 ; then usage @@ -108,9 +112,30 @@ if [ -z "$all_tests" ] ; then ) fi -for file in $all_tests; do - bash "${BASH_SOURCE%/*}"/run_test.sh "$file" "$bin_dir" "$logdir" -done +run_parallel= +if [ -n "$use_parallel" ] ; then + if command -v parallel &> /dev/null ; then + if parallel --version 2>&1 | grep GNU > /dev/null 2>&1 ; then + echo "GNU parallel is not supported. Use moreutils parallel instead." + else + run_parallel=yes + fi + else + echo "Install moreutils to run tests in parallel" + fi +fi + +if [ -t 1 ] ; then + color_flag="-c" +fi + +if [ -n "$run_parallel" ]; then + parallel -i bash "${BASH_SOURCE%/*}/run_test.sh" $color_flag -s "$smt2_options" {} "$bin_dir" "$logdir" -- $all_tests +else + for file in $all_tests; do + bash "${BASH_SOURCE%/*}"/run_test.sh $color_flag -s "$smt2_options" "$file" "$bin_dir" "$logdir" + done +fi pass=$(find "$logdir" -type f -name "*.pass" | wc -l) fail=$(find "$logdir" -type f -name "*.error" | wc -l) diff --git a/tests/regress/run_test.sh b/tests/regress/run_test.sh index 2be012654..c28148c2f 100644 --- a/tests/regress/run_test.sh +++ b/tests/regress/run_test.sh @@ -40,6 +40,24 @@ usage() { exit 4 } +smt2_options= +color= + +while getopts "cs:" o; do + case "$o" in + s) + smt2_options=${OPTARG} + ;; + c) + color="on" + ;; + *) + usage + ;; + esac +done +shift $((OPTIND-1)) + if [ $# -lt 2 ] ; then usage fi @@ -81,7 +99,7 @@ TIMEFORMAT="%U" red= green= black= -if test -t 1 ; then +if [ -t 1 ] || [ -n "$color" ]; then red=$(tput setaf 1) green=$(tput setaf 2) black=$(tput sgr0) @@ -98,8 +116,6 @@ then TIME_LIMIT=60 fi -echo -n "$test_file" - # Get the binary based on the filename filename=$(basename "$test_file") @@ -108,7 +124,7 @@ options= case $filename in *.smt2) binary=yices_smt2 - #options=$smt2_options + options=$smt2_options ;; *.smt) binary=yices_smtcomp @@ -117,7 +133,7 @@ case $filename in binary=yices ;; *) - echo FAIL: unknown extension for "$filename" + echo "FAIL: unknown extension for $filename" exit 2 esac @@ -125,11 +141,9 @@ esac if [ -e "$test_file.options" ] then options="$options $(cat $test_file.options)" - echo " [ $options ]" test_string="$test_file [ $options ]" else test_string="$test_file" - echo fi # Get the expected result @@ -137,12 +151,15 @@ if [ -e "$test_file.gold" ] then gold=$test_file.gold else - echo -n $red - echo FAIL: missing file: $test_file.gold - echo -n $black + echo "$red FAIL: missing file: $test_file.gold $black" exit 2 fi +if [ -d "$out_dir" ] ; then + # add pid in case there are multiple tests with the same name + log_file="$out_dir/$filename.$BASHPID" +fi + # Run the binary ( ulimit -S -t $TIME_LIMIT &> /dev/null @@ -155,34 +172,24 @@ runtime=$(cat $timefile) # Do the diff DIFF=$(diff -w "$outfile" "$gold") -rm "$timefile" -rm "$outfile" - -# find log url -if [ -d "$out_dir" ] ; then - # add pid in case there are multiple tests with the same name - log_file="$out_dir/$filename.$BASHPID" -fi - if [ $? -eq 0 ] && [ $status -eq 0 ] then - echo -n $green - echo PASS [${runtime} s] - echo -n $black + echo -e "$green PASS [${runtime} s] $black $test_string" if [ -n "$log_file" ] ; then log_file="$log_file.pass" echo "$test_string" > "$log_file" fi - exit 0 + code=0 else - echo -n $red - echo FAIL - echo -n $black - + echo -e "$red FAIL $black $test_string" if [ -n "$log_file" ] ; then log_file="$log_file.error" echo "$test_string" > "$log_file" echo "$DIFF" >> "$log_file" fi - exit 1 + code=1 fi + +rm "$timefile" +rm "$outfile" +exit $code From e4010e7d9385f837ee8cd09fad06b216c4fbc439 Mon Sep 17 00:00:00 2001 From: Thomas Hader Date: Fri, 16 Feb 2024 02:41:43 +0100 Subject: [PATCH 03/15] Code formatting --- tests/regress/check.sh | 51 +++++++++++++++++++-------------------- tests/regress/run_test.sh | 38 ++++++++++++++--------------- 2 files changed, 44 insertions(+), 45 deletions(-) diff --git a/tests/regress/check.sh b/tests/regress/check.sh index 528efe071..c5417beaf 100755 --- a/tests/regress/check.sh +++ b/tests/regress/check.sh @@ -45,14 +45,14 @@ use_parallel= while getopts "js:" o; do case "$o" in s) - smt2_options=${OPTARG} - ;; - j) - use_parallel=yes - ;; - *) - usage - ;; + smt2_options=${OPTARG} + ;; + j) + use_parallel=yes + ;; + *) + usage + ;; esac done shift $((OPTIND-1)) @@ -68,7 +68,6 @@ all_tests="$@" # # System-dependent configuration -# TODO why? # os_name=$(uname 2>/dev/null) || os_name=unknown @@ -90,7 +89,7 @@ logdir=$($mktemp_cmd -d) || { echo "Can't create temp folder" ; exit 1 ; } if [[ -z "$REGRESS_FILTER" ]]; then - REGRESS_FILTER="." + REGRESS_FILTER="." fi # @@ -106,23 +105,23 @@ fi if [ -z "$all_tests" ] ; then all_tests=$( - find "$regress_dir" -name '*.smt' -or -name '*.smt2' -or -name '*.ys' | - grep $REGRESS_FILTER | grep $MCSAT_FILTER | - sort + find "$regress_dir" -name '*.smt' -or -name '*.smt2' -or -name '*.ys' | + grep $REGRESS_FILTER | grep $MCSAT_FILTER | + sort ) fi run_parallel= if [ -n "$use_parallel" ] ; then - if command -v parallel &> /dev/null ; then - if parallel --version 2>&1 | grep GNU > /dev/null 2>&1 ; then - echo "GNU parallel is not supported. Use moreutils parallel instead." + if command -v parallel &> /dev/null ; then + if parallel --version 2>&1 | grep GNU > /dev/null 2>&1 ; then + echo "GNU parallel is not supported. Use moreutils parallel instead." + else + run_parallel=yes + fi else - run_parallel=yes + echo "Install moreutils to run tests in parallel" fi - else - echo "Install moreutils to run tests in parallel" - fi fi if [ -t 1 ] ; then @@ -130,11 +129,11 @@ if [ -t 1 ] ; then fi if [ -n "$run_parallel" ]; then - parallel -i bash "${BASH_SOURCE%/*}/run_test.sh" $color_flag -s "$smt2_options" {} "$bin_dir" "$logdir" -- $all_tests + parallel -i bash "${BASH_SOURCE%/*}/run_test.sh" $color_flag -s "$smt2_options" {} "$bin_dir" "$logdir" -- $all_tests else - for file in $all_tests; do - bash "${BASH_SOURCE%/*}"/run_test.sh $color_flag -s "$smt2_options" "$file" "$bin_dir" "$logdir" - done + for file in $all_tests; do + bash "${BASH_SOURCE%/*}"/run_test.sh $color_flag -s "$smt2_options" "$file" "$bin_dir" "$logdir" + done fi pass=$(find "$logdir" -type f -name "*.pass" | wc -l) @@ -147,8 +146,8 @@ if [ "$fail" -eq 0 ] ; then code=0 else for f in "$logdir"/*.error ; do - cat "$f" - echo + cat "$f" + echo done code=1 fi diff --git a/tests/regress/run_test.sh b/tests/regress/run_test.sh index c28148c2f..ff715dc3b 100644 --- a/tests/regress/run_test.sh +++ b/tests/regress/run_test.sh @@ -46,14 +46,14 @@ color= while getopts "cs:" o; do case "$o" in s) - smt2_options=${OPTARG} - ;; - c) - color="on" - ;; - *) - usage - ;; + smt2_options=${OPTARG} + ;; + c) + color="on" + ;; + *) + usage + ;; esac done shift $((OPTIND-1)) @@ -100,9 +100,9 @@ red= green= black= if [ -t 1 ] || [ -n "$color" ]; then - red=$(tput setaf 1) - green=$(tput setaf 2) - black=$(tput sgr0) + red=$(tput setaf 1) + green=$(tput setaf 2) + black=$(tput sgr0) fi # @@ -113,7 +113,7 @@ timefile=$($mktemp_cmd) || { echo "Can't create temp file" ; exit 3 ; } if [[ -z "$TIME_LIMIT" ]]; then - TIME_LIMIT=60 + TIME_LIMIT=60 fi # Get the binary based on the filename @@ -156,8 +156,8 @@ else fi if [ -d "$out_dir" ] ; then - # add pid in case there are multiple tests with the same name - log_file="$out_dir/$filename.$BASHPID" + # add pid in case there are multiple tests with the same name + log_file="$out_dir/$filename.$BASHPID" fi # Run the binary @@ -176,16 +176,16 @@ if [ $? -eq 0 ] && [ $status -eq 0 ] then echo -e "$green PASS [${runtime} s] $black $test_string" if [ -n "$log_file" ] ; then - log_file="$log_file.pass" - echo "$test_string" > "$log_file" + log_file="$log_file.pass" + echo "$test_string" > "$log_file" fi code=0 else echo -e "$red FAIL $black $test_string" if [ -n "$log_file" ] ; then - log_file="$log_file.error" - echo "$test_string" > "$log_file" - echo "$DIFF" >> "$log_file" + log_file="$log_file.error" + echo "$test_string" > "$log_file" + echo "$DIFF" >> "$log_file" fi code=1 fi From 337025abf4f0244e7254f899d24496411a445619 Mon Sep 17 00:00:00 2001 From: Thomas Hader Date: Tue, 19 Dec 2023 16:07:16 +0100 Subject: [PATCH 04/15] Build system update to use static libpoly for all builds when configured --- configure.ac | 7 +++++-- src/Makefile | 19 ++++++++++++++----- tests/api/Makefile | 15 ++++++++++++--- tests/unit/Makefile | 15 ++++++++++++--- 4 files changed, 43 insertions(+), 13 deletions(-) diff --git a/configure.ac b/configure.ac index 15b4a97b6..1def5ddff 100644 --- a/configure.ac +++ b/configure.ac @@ -578,7 +578,7 @@ if test -z "$1"; then if test -f $ldir/libgmp.a; then AC_MSG_RESULT(found) testlib=$ldir/libgmp.a - CSL_CHECK_GMP($testlib,$testincludedir) + CSL_CHECK_GMP($testlib,$testincludedir) if test $run_ok = yes; then STATIC_GMP=$testlib STATIC_GMP_INCLUDE_DIR=$testincludedir @@ -829,16 +829,19 @@ fi # # Default GMP # +if test "x$STATIC_LIBGMP" = x ; then AC_CHECK_LIB(gmp, __gmpz_cmp, [], [AC_MSG_ERROR([*** GMP library not found. Try to set LDFLAGS ***])]) - +fi # # Default libpoly # if test $use_mcsat = yes ; then +if test "x$STATIC_LIBPOLY" = x ; then AC_CHECK_LIB([poly],[lp_polynomial_new], [], [AC_MSG_ERROR([*** libpoly library not found. Try to set LDFLAGS ***])]) fi +fi # # Default CUDD diff --git a/src/Makefile b/src/Makefile index 267a96287..3d595c1de 100644 --- a/src/Makefile +++ b/src/Makefile @@ -875,14 +875,23 @@ endif # More CPPFLAGS for compiling static objects # ifneq ($(STATIC_GMP_INCLUDE_DIR),) - STATIC_CPP_GMP := -I$(STATIC_GMP_INCLUDE_DIR) + STATIC_GMP_INCLUDE := -I$(STATIC_GMP_INCLUDE_DIR) endif ifneq ($(STATIC_LIBPOLY_INCLUDE_DIR),) - STATIC_CPP_LIBPOLY := -I$(STATIC_LIBPOLY_INCLUDE_DIR) + STATIC_LIBPOLY_INCLUDE := -I$(STATIC_LIBPOLY_INCLUDE_DIR) endif -STATIC_CPPFLAGS := $(STATIC_CPP_GMP) $(STATIC_CPP_LIBPOLY) $(CPPFLAGS) +ifneq ($(STATIC_LIBPOLY),) + LIBS := $(subst -lpoly,,$(LIBS)) $(STATIC_LIBPOLY) +endif + +ifneq ($(STATIC_GMP),) + LIBS := $(subst -lgmp,,$(LIBS)) $(STATIC_GMP) +endif + +STATIC_CPPFLAGS := $(STATIC_GMP_INCLUDE) $(STATIC_LIBPOLY_INCLUDE) $(CPPFLAGS) +CPPFLAGS := $(STATIC_GMP_INCLUDE) $(STATIC_LIBPOLY_INCLUDE) $(CPPFLAGS) # # For building dll linked statically with libgmp.a @@ -891,11 +900,11 @@ STATIC_CPPFLAGS := $(STATIC_CPP_GMP) $(STATIC_CPP_LIBPOLY) $(CPPFLAGS) # we also add the NOYICES_DLL flag. # ifeq ($(POSIXOS),cygwin) - STATIC_DLL_CPPFLAGS := $(STATIC_CPP_GMP) $(STATIC_CPP_LIBPOLY) $(CPPFLAGS) + STATIC_DLL_CPPFLAGS := $(STATIC_GMP_INCLUDE) $(STATIC_LIBPOLY_INCLUDE) $(CPPFLAGS) STATIC_CPPFLAGS += -DNOYICES_DLL else ifeq ($(POSIXOS),mingw) - STATIC_DLL_CPPFLAGS := $(STATIC_CPP_GMP) $(STATIC_CPP_LIBPOLY) $(CPPFLAGS) + STATIC_DLL_CPPFLAGS := $(STATIC_GMP_INCLUDE) $(STATIC_LIBPOLY_INCLUDE) $(CPPFLAGS) STATIC_CPPFLAGS += -DNOYICES_DLL endif endif diff --git a/tests/api/Makefile b/tests/api/Makefile index b181e889e..4c749b857 100644 --- a/tests/api/Makefile +++ b/tests/api/Makefile @@ -272,14 +272,23 @@ CPPFLAGS := -I../../src -I../../src/include $(CPPFLAGS) # More CPPFLAGS for compiling static objects # ifneq ($(STATIC_GMP_INCLUDE_DIR),) - STATIC_CPP_GMP := -I$(STATIC_GMP_INCLUDE_DIR) + STATIC_GMP_INCLUDE := -I$(STATIC_GMP_INCLUDE_DIR) endif ifneq ($(STATIC_LIBPOLY_INCLUDE_DIR),) - STATIC_CPP_LIBPOLY := -I$(STATIC_LIBPOLY_INCLUDE_DIR) + STATIC_LIBPOLY_INCLUDE := -I$(STATIC_LIBPOLY_INCLUDE_DIR) endif -STATIC_CPPFLAGS := $(STATIC_CPP_GMP) $(STATIC_CPP_LIBPOLY) $(CPPFLAGS) +ifneq ($(STATIC_LIBPOLY),) + LIBS := $(subst -lpoly,,$(LIBS)) $(STATIC_LIBPOLY) +endif + +ifneq ($(STATIC_GMP),) + LIBS := $(subst -lgmp,,$(LIBS)) $(STATIC_GMP) +endif + +STATIC_CPPFLAGS := $(STATIC_GMP_INCLUDE) $(STATIC_LIBPOLY_INCLUDE) $(CPPFLAGS) +CPPFLAGS := $(STATIC_GMP_INCLUDE) $(STATIC_LIBPOLY_INCLUDE) $(CPPFLAGS) # # These are not needed for the tests -DNOYICES_DLL is already diff --git a/tests/unit/Makefile b/tests/unit/Makefile index 6848641ec..d5e9550fe 100644 --- a/tests/unit/Makefile +++ b/tests/unit/Makefile @@ -274,14 +274,23 @@ CPPFLAGS := -I../../src -I../../src/include $(CPPFLAGS) # More CPPFLAGS for compiling static objects # ifneq ($(STATIC_GMP_INCLUDE_DIR),) - STATIC_CPP_GMP := -I$(STATIC_GMP_INCLUDE_DIR) + STATIC_GMP_INCLUDE := -I$(STATIC_GMP_INCLUDE_DIR) endif ifneq ($(STATIC_LIBPOLY_INCLUDE_DIR),) - STATIC_CPP_LIBPOLY := -I$(STATIC_LIBPOLY_INCLUDE_DIR) + STATIC_LIBPOLY_INCLUDE := -I$(STATIC_LIBPOLY_INCLUDE_DIR) endif -STATIC_CPPFLAGS := $(STATIC_CPP_GMP) $(STATIC_CPP_LIBPOLY) $(CPPFLAGS) +ifneq ($(STATIC_LIBPOLY),) + LIBS := $(subst -lpoly,,$(LIBS)) $(STATIC_LIBPOLY) +endif + +ifneq ($(STATIC_GMP),) + LIBS := $(subst -lgmp,,$(LIBS)) $(STATIC_GMP) +endif + +STATIC_CPPFLAGS := $(STATIC_GMP_INCLUDE) $(STATIC_LIBPOLY_INCLUDE) $(CPPFLAGS) +CPPFLAGS := $(STATIC_GMP_INCLUDE) $(STATIC_LIBPOLY_INCLUDE) $(CPPFLAGS) # # These are not needed for the tests -DNOYICES_DLL is already From 6be7eb30278f88590ab42dfa746c049622681a86 Mon Sep 17 00:00:00 2001 From: Thomas Hader Date: Fri, 16 Feb 2024 20:23:34 +0100 Subject: [PATCH 05/15] Added GNU parallel support --- tests/regress/check.sh | 24 +++++++++++++++--------- 1 file changed, 15 insertions(+), 9 deletions(-) diff --git a/tests/regress/check.sh b/tests/regress/check.sh index c5417beaf..3e1d2b986 100755 --- a/tests/regress/check.sh +++ b/tests/regress/check.sh @@ -115,9 +115,9 @@ run_parallel= if [ -n "$use_parallel" ] ; then if command -v parallel &> /dev/null ; then if parallel --version 2>&1 | grep GNU > /dev/null 2>&1 ; then - echo "GNU parallel is not supported. Use moreutils parallel instead." + run_parallel=gnu else - run_parallel=yes + run_parallel=more fi else echo "Install moreutils to run tests in parallel" @@ -128,13 +128,19 @@ if [ -t 1 ] ; then color_flag="-c" fi -if [ -n "$run_parallel" ]; then - parallel -i bash "${BASH_SOURCE%/*}/run_test.sh" $color_flag -s "$smt2_options" {} "$bin_dir" "$logdir" -- $all_tests -else - for file in $all_tests; do - bash "${BASH_SOURCE%/*}"/run_test.sh $color_flag -s "$smt2_options" "$file" "$bin_dir" "$logdir" - done -fi +case "$run_parallel" in + more) + parallel -i bash "${BASH_SOURCE%/*}/run_test.sh" $color_flag -s "$smt2_options" {} "$bin_dir" "$logdir" -- $all_tests + ;; + gnu) + parallel bash "${BASH_SOURCE%/*}/run_test.sh" $color_flag {} "$bin_dir" "$logdir" ::: $all_tests + ;; + *) + for file in $all_tests; do + bash "${BASH_SOURCE%/*}"/run_test.sh $color_flag -s "$smt2_options" "$file" "$bin_dir" "$logdir" + done + ;; +esac pass=$(find "$logdir" -type f -name "*.pass" | wc -l) fail=$(find "$logdir" -type f -name "*.error" | wc -l) From ead1b1e5d134323bd7395370276fa832aa2a9ac3 Mon Sep 17 00:00:00 2001 From: Thomas Hader Date: Fri, 16 Feb 2024 12:01:59 -0800 Subject: [PATCH 06/15] Fixed GNU parallel escaping --- tests/regress/check.sh | 10 +++++----- tests/regress/run_test.sh | 2 +- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/tests/regress/check.sh b/tests/regress/check.sh index 3e1d2b986..d8343e361 100755 --- a/tests/regress/check.sh +++ b/tests/regress/check.sh @@ -111,13 +111,13 @@ if [ -z "$all_tests" ] ; then ) fi -run_parallel= +run_parallel="no" if [ -n "$use_parallel" ] ; then if command -v parallel &> /dev/null ; then if parallel --version 2>&1 | grep GNU > /dev/null 2>&1 ; then - run_parallel=gnu + run_parallel="gnu" else - run_parallel=more + run_parallel="more" fi else echo "Install moreutils to run tests in parallel" @@ -130,10 +130,10 @@ fi case "$run_parallel" in more) - parallel -i bash "${BASH_SOURCE%/*}/run_test.sh" $color_flag -s "$smt2_options" {} "$bin_dir" "$logdir" -- $all_tests + parallel -i bash "${BASH_SOURCE%/*}/run_test.sh" $color_flag -s "$smt2_options" {} "$bin_dir" "$logdir" -- "$all_tests" ;; gnu) - parallel bash "${BASH_SOURCE%/*}/run_test.sh" $color_flag {} "$bin_dir" "$logdir" ::: $all_tests + parallel -q bash "${BASH_SOURCE%/*}/run_test.sh" $color_flag -s "$smt2_options" {} "$bin_dir" "$logdir" ::: "$all_tests" ;; *) for file in $all_tests; do diff --git a/tests/regress/run_test.sh b/tests/regress/run_test.sh index ff715dc3b..886cd6073 100644 --- a/tests/regress/run_test.sh +++ b/tests/regress/run_test.sh @@ -167,7 +167,7 @@ fi (time ./$bin_dir/$binary $options ./$test_file >& $outfile ) >& $timefile ) status=$? -runtime=$(cat $timefile) +runtime=$(cat "$timefile") # Do the diff DIFF=$(diff -w "$outfile" "$gold") From ed541e03fb7643a84466d5c18e86829dd144312a Mon Sep 17 00:00:00 2001 From: Thomas Hader Date: Fri, 16 Feb 2024 12:10:38 -0800 Subject: [PATCH 07/15] Fixed some missing quotes in bash scripts --- tests/regress/check.sh | 8 +++++--- tests/regress/run_test.sh | 4 ++-- 2 files changed, 7 insertions(+), 5 deletions(-) diff --git a/tests/regress/check.sh b/tests/regress/check.sh index d8343e361..11f1f9c35 100755 --- a/tests/regress/check.sh +++ b/tests/regress/check.sh @@ -120,7 +120,9 @@ if [ -n "$use_parallel" ] ; then run_parallel="more" fi else - echo "Install moreutils to run tests in parallel" + echo "****************************************************************" + echo "HINT: Install moreutils or GNU parallel to run tests in parallel" + echo "****************************************************************" fi fi @@ -130,10 +132,10 @@ fi case "$run_parallel" in more) - parallel -i bash "${BASH_SOURCE%/*}/run_test.sh" $color_flag -s "$smt2_options" {} "$bin_dir" "$logdir" -- "$all_tests" + parallel -i bash "${BASH_SOURCE%/*}/run_test.sh" $color_flag -s "$smt2_options" {} "$bin_dir" "$logdir" -- $all_tests ;; gnu) - parallel -q bash "${BASH_SOURCE%/*}/run_test.sh" $color_flag -s "$smt2_options" {} "$bin_dir" "$logdir" ::: "$all_tests" + parallel -q bash "${BASH_SOURCE%/*}/run_test.sh" $color_flag -s "$smt2_options" {} "$bin_dir" "$logdir" ::: $all_tests ;; *) for file in $all_tests; do diff --git a/tests/regress/run_test.sh b/tests/regress/run_test.sh index 886cd6073..e4e84047d 100644 --- a/tests/regress/run_test.sh +++ b/tests/regress/run_test.sh @@ -140,7 +140,7 @@ esac # Get the options if [ -e "$test_file.options" ] then - options="$options $(cat $test_file.options)" + options="$options $(cat "$test_file.options")" test_string="$test_file [ $options ]" else test_string="$test_file" @@ -164,7 +164,7 @@ fi ( ulimit -S -t $TIME_LIMIT &> /dev/null ulimit -H -t $((1+$TIME_LIMIT)) &> /dev/null - (time ./$bin_dir/$binary $options ./$test_file >& $outfile ) >& $timefile + (time "./$bin_dir/$binary" $options "./$test_file" >& "$outfile" ) >& "$timefile" ) status=$? runtime=$(cat "$timefile") From 455a0cd99ef2fae8edff10a35e870246f4c94019 Mon Sep 17 00:00:00 2001 From: Thomas Hader Date: Fri, 16 Feb 2024 13:55:51 -0800 Subject: [PATCH 08/15] use full path in output log instead of PID --- tests/regress/run_test.sh | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/tests/regress/run_test.sh b/tests/regress/run_test.sh index e4e84047d..a0376269e 100644 --- a/tests/regress/run_test.sh +++ b/tests/regress/run_test.sh @@ -156,8 +156,7 @@ else fi if [ -d "$out_dir" ] ; then - # add pid in case there are multiple tests with the same name - log_file="$out_dir/$filename.$BASHPID" + log_file="$out_dir/$(echo "$test_file" | tr '/' '_')" fi # Run the binary From 70949b0ae8e7b46bee8e11315e14f551b04672c4 Mon Sep 17 00:00:00 2001 From: Thomas Hader Date: Fri, 16 Feb 2024 14:57:20 -0800 Subject: [PATCH 09/15] fixed whitespace --- configure.ac | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/configure.ac b/configure.ac index 1def5ddff..ddebcb2a8 100644 --- a/configure.ac +++ b/configure.ac @@ -578,7 +578,7 @@ if test -z "$1"; then if test -f $ldir/libgmp.a; then AC_MSG_RESULT(found) testlib=$ldir/libgmp.a - CSL_CHECK_GMP($testlib,$testincludedir) + CSL_CHECK_GMP($testlib,$testincludedir) if test $run_ok = yes; then STATIC_GMP=$testlib STATIC_GMP_INCLUDE_DIR=$testincludedir From 1d46fcaa567fdc39bdfd709defe816c3cceea894 Mon Sep 17 00:00:00 2001 From: Thomas Hader Date: Fri, 16 Feb 2024 15:14:06 -0800 Subject: [PATCH 10/15] Fixed result printing with hidden error files --- tests/regress/check.sh | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/tests/regress/check.sh b/tests/regress/check.sh index 11f1f9c35..866dc7e59 100755 --- a/tests/regress/check.sh +++ b/tests/regress/check.sh @@ -153,9 +153,10 @@ echo "Fail: $fail" if [ "$fail" -eq 0 ] ; then code=0 else - for f in "$logdir"/*.error ; do - cat "$f" - echo + find "$logdir" -type f -name "*.error" -printf '%P\0' | + while read -rd $'\0' path; do + cat "$path" + echo done code=1 fi From d219ec6f9f59db789e3beb37bfe14a7be49a3b0f Mon Sep 17 00:00:00 2001 From: Thomas Hader Date: Fri, 16 Feb 2024 15:48:50 -0800 Subject: [PATCH 11/15] Fix path escape --- tests/regress/check.sh | 5 ++--- tests/regress/run_test.sh | 3 ++- 2 files changed, 4 insertions(+), 4 deletions(-) mode change 100644 => 100755 tests/regress/run_test.sh diff --git a/tests/regress/check.sh b/tests/regress/check.sh index 866dc7e59..575ea1536 100755 --- a/tests/regress/check.sh +++ b/tests/regress/check.sh @@ -153,9 +153,8 @@ echo "Fail: $fail" if [ "$fail" -eq 0 ] ; then code=0 else - find "$logdir" -type f -name "*.error" -printf '%P\0' | - while read -rd $'\0' path; do - cat "$path" + for f in "$logdir"/*.error ; do + cat "$f" echo done code=1 diff --git a/tests/regress/run_test.sh b/tests/regress/run_test.sh old mode 100644 new mode 100755 index a0376269e..2ef34be9d --- a/tests/regress/run_test.sh +++ b/tests/regress/run_test.sh @@ -156,7 +156,8 @@ else fi if [ -d "$out_dir" ] ; then - log_file="$out_dir/$(echo "$test_file" | tr '/' '_')" + # replace _ with __ and / with _ + log_file="$out_dir/_$(echo "${test_file//_/__}" | tr '/' '_')}" fi # Run the binary From a80dbe81b256e8b1bc74ebe34bd22fea3099923d Mon Sep 17 00:00:00 2001 From: Thomas Hader Date: Mon, 19 Feb 2024 15:28:59 -0800 Subject: [PATCH 12/15] Revert "Build system update to use static libpoly for all builds when configured" This reverts commit 337025abf4f0244e7254f899d24496411a445619. --- configure.ac | 5 +---- src/Makefile | 19 +++++-------------- tests/api/Makefile | 15 +++------------ tests/unit/Makefile | 15 +++------------ 4 files changed, 12 insertions(+), 42 deletions(-) diff --git a/configure.ac b/configure.ac index ddebcb2a8..b9448ef30 100644 --- a/configure.ac +++ b/configure.ac @@ -829,19 +829,16 @@ fi # # Default GMP # -if test "x$STATIC_LIBGMP" = x ; then AC_CHECK_LIB(gmp, __gmpz_cmp, [], [AC_MSG_ERROR([*** GMP library not found. Try to set LDFLAGS ***])]) -fi + # # Default libpoly # if test $use_mcsat = yes ; then -if test "x$STATIC_LIBPOLY" = x ; then AC_CHECK_LIB([poly],[lp_polynomial_new], [], [AC_MSG_ERROR([*** libpoly library not found. Try to set LDFLAGS ***])]) fi -fi # # Default CUDD diff --git a/src/Makefile b/src/Makefile index 3d595c1de..267a96287 100644 --- a/src/Makefile +++ b/src/Makefile @@ -875,23 +875,14 @@ endif # More CPPFLAGS for compiling static objects # ifneq ($(STATIC_GMP_INCLUDE_DIR),) - STATIC_GMP_INCLUDE := -I$(STATIC_GMP_INCLUDE_DIR) + STATIC_CPP_GMP := -I$(STATIC_GMP_INCLUDE_DIR) endif ifneq ($(STATIC_LIBPOLY_INCLUDE_DIR),) - STATIC_LIBPOLY_INCLUDE := -I$(STATIC_LIBPOLY_INCLUDE_DIR) + STATIC_CPP_LIBPOLY := -I$(STATIC_LIBPOLY_INCLUDE_DIR) endif -ifneq ($(STATIC_LIBPOLY),) - LIBS := $(subst -lpoly,,$(LIBS)) $(STATIC_LIBPOLY) -endif - -ifneq ($(STATIC_GMP),) - LIBS := $(subst -lgmp,,$(LIBS)) $(STATIC_GMP) -endif - -STATIC_CPPFLAGS := $(STATIC_GMP_INCLUDE) $(STATIC_LIBPOLY_INCLUDE) $(CPPFLAGS) -CPPFLAGS := $(STATIC_GMP_INCLUDE) $(STATIC_LIBPOLY_INCLUDE) $(CPPFLAGS) +STATIC_CPPFLAGS := $(STATIC_CPP_GMP) $(STATIC_CPP_LIBPOLY) $(CPPFLAGS) # # For building dll linked statically with libgmp.a @@ -900,11 +891,11 @@ CPPFLAGS := $(STATIC_GMP_INCLUDE) $(STATIC_LIBPOLY_INCLUDE) $(CPPFLAGS) # we also add the NOYICES_DLL flag. # ifeq ($(POSIXOS),cygwin) - STATIC_DLL_CPPFLAGS := $(STATIC_GMP_INCLUDE) $(STATIC_LIBPOLY_INCLUDE) $(CPPFLAGS) + STATIC_DLL_CPPFLAGS := $(STATIC_CPP_GMP) $(STATIC_CPP_LIBPOLY) $(CPPFLAGS) STATIC_CPPFLAGS += -DNOYICES_DLL else ifeq ($(POSIXOS),mingw) - STATIC_DLL_CPPFLAGS := $(STATIC_GMP_INCLUDE) $(STATIC_LIBPOLY_INCLUDE) $(CPPFLAGS) + STATIC_DLL_CPPFLAGS := $(STATIC_CPP_GMP) $(STATIC_CPP_LIBPOLY) $(CPPFLAGS) STATIC_CPPFLAGS += -DNOYICES_DLL endif endif diff --git a/tests/api/Makefile b/tests/api/Makefile index 4c749b857..b181e889e 100644 --- a/tests/api/Makefile +++ b/tests/api/Makefile @@ -272,23 +272,14 @@ CPPFLAGS := -I../../src -I../../src/include $(CPPFLAGS) # More CPPFLAGS for compiling static objects # ifneq ($(STATIC_GMP_INCLUDE_DIR),) - STATIC_GMP_INCLUDE := -I$(STATIC_GMP_INCLUDE_DIR) + STATIC_CPP_GMP := -I$(STATIC_GMP_INCLUDE_DIR) endif ifneq ($(STATIC_LIBPOLY_INCLUDE_DIR),) - STATIC_LIBPOLY_INCLUDE := -I$(STATIC_LIBPOLY_INCLUDE_DIR) + STATIC_CPP_LIBPOLY := -I$(STATIC_LIBPOLY_INCLUDE_DIR) endif -ifneq ($(STATIC_LIBPOLY),) - LIBS := $(subst -lpoly,,$(LIBS)) $(STATIC_LIBPOLY) -endif - -ifneq ($(STATIC_GMP),) - LIBS := $(subst -lgmp,,$(LIBS)) $(STATIC_GMP) -endif - -STATIC_CPPFLAGS := $(STATIC_GMP_INCLUDE) $(STATIC_LIBPOLY_INCLUDE) $(CPPFLAGS) -CPPFLAGS := $(STATIC_GMP_INCLUDE) $(STATIC_LIBPOLY_INCLUDE) $(CPPFLAGS) +STATIC_CPPFLAGS := $(STATIC_CPP_GMP) $(STATIC_CPP_LIBPOLY) $(CPPFLAGS) # # These are not needed for the tests -DNOYICES_DLL is already diff --git a/tests/unit/Makefile b/tests/unit/Makefile index d5e9550fe..6848641ec 100644 --- a/tests/unit/Makefile +++ b/tests/unit/Makefile @@ -274,23 +274,14 @@ CPPFLAGS := -I../../src -I../../src/include $(CPPFLAGS) # More CPPFLAGS for compiling static objects # ifneq ($(STATIC_GMP_INCLUDE_DIR),) - STATIC_GMP_INCLUDE := -I$(STATIC_GMP_INCLUDE_DIR) + STATIC_CPP_GMP := -I$(STATIC_GMP_INCLUDE_DIR) endif ifneq ($(STATIC_LIBPOLY_INCLUDE_DIR),) - STATIC_LIBPOLY_INCLUDE := -I$(STATIC_LIBPOLY_INCLUDE_DIR) + STATIC_CPP_LIBPOLY := -I$(STATIC_LIBPOLY_INCLUDE_DIR) endif -ifneq ($(STATIC_LIBPOLY),) - LIBS := $(subst -lpoly,,$(LIBS)) $(STATIC_LIBPOLY) -endif - -ifneq ($(STATIC_GMP),) - LIBS := $(subst -lgmp,,$(LIBS)) $(STATIC_GMP) -endif - -STATIC_CPPFLAGS := $(STATIC_GMP_INCLUDE) $(STATIC_LIBPOLY_INCLUDE) $(CPPFLAGS) -CPPFLAGS := $(STATIC_GMP_INCLUDE) $(STATIC_LIBPOLY_INCLUDE) $(CPPFLAGS) +STATIC_CPPFLAGS := $(STATIC_CPP_GMP) $(STATIC_CPP_LIBPOLY) $(CPPFLAGS) # # These are not needed for the tests -DNOYICES_DLL is already From 7b1d0ee61ec7cd2324986e84d40b42d8514d7cb4 Mon Sep 17 00:00:00 2001 From: Thomas Hader Date: Tue, 20 Feb 2024 17:07:29 -0800 Subject: [PATCH 13/15] Include support for GNU make jobserver --- Makefile.build | 2 +- tests/regress/check.sh | 62 ++++++++++++++++++++++++++++-------------- 2 files changed, 43 insertions(+), 21 deletions(-) diff --git a/Makefile.build b/Makefile.build index c6a33f859..99a8fe43c 100644 --- a/Makefile.build +++ b/Makefile.build @@ -309,7 +309,7 @@ regress: build_subdirs version @ echo "=== Building binaries ===" @ $(MAKE) -C $(srcdir) BUILD=../$(build_dir) bin @ echo "=== Running regressions ===" - @ $(regressdir)/check.sh -j $(regressdir) $(build_dir)/bin + +@ $(regressdir)/check.sh $(regressdir) $(build_dir)/bin static-regress: static_build_subdirs version diff --git a/tests/regress/check.sh b/tests/regress/check.sh index 575ea1536..0216ccd92 100755 --- a/tests/regress/check.sh +++ b/tests/regress/check.sh @@ -40,7 +40,7 @@ usage() { } smt2_options= -use_parallel= +j_option= while getopts "js:" o; do case "$o" in @@ -48,7 +48,7 @@ while getopts "js:" o; do smt2_options=${OPTARG} ;; j) - use_parallel=yes + j_option=yes ;; *) usage @@ -82,6 +82,15 @@ case "$os_name" in esac +parallel_tool= +if command -v parallel &> /dev/null ; then + if parallel --version 2>&1 | grep GNU > /dev/null 2>&1 ; then + parallel_tool="gnu" + else + parallel_tool="more" + fi +fi + # # The temp file for output # @@ -111,31 +120,38 @@ if [ -z "$all_tests" ] ; then ) fi -run_parallel="no" -if [ -n "$use_parallel" ] ; then - if command -v parallel &> /dev/null ; then - if parallel --version 2>&1 | grep GNU > /dev/null 2>&1 ; then - run_parallel="gnu" - else - run_parallel="more" - fi - else - echo "****************************************************************" - echo "HINT: Install moreutils or GNU parallel to run tests in parallel" - echo "****************************************************************" - fi -fi - if [ -t 1 ] ; then color_flag="-c" fi -case "$run_parallel" in +# job_count 1: serial execution, 0: unrestricted parallel, n>1: n processes +job_count=1 + +#check if we are in a make run with -j N +if [ -n "$parallel_tool" ]; then + if [[ -n "$j_option" ]]; then + job_count=0 + elif [[ "$MAKEFLAGS" == *"jobserver-fds="* ]] || [[ "$MAKEFLAGS" == *"jobserver-auth="* ]]; then + # greedy get as many tokens as possible + fdR=$(echo "$MAKEFLAGS" | sed -E "s|.*--jobserver-(fds\|auth)=([0-9]+),([0-9]+).*|\2|") + fdW=$(echo "$MAKEFLAGS" | sed -E "s|.*--jobserver-(fds\|auth)=([0-9]+),([0-9]+).*|\3|") + while IFS= read -r -d '' -t 1 -n 1 <&"$fdR"; do + job_count=$((job_count+1)) + done + elif [[ "$MAKEFLAGS" =~ (^|[ ])-?j($|[ ]) ]]; then + job_count=0 + fi +fi + +j_param="-j$job_count" +if [[ $job_count == 0 ]]; then j_param=""; fi + +case "$parallel_tool" in more) - parallel -i bash "${BASH_SOURCE%/*}/run_test.sh" $color_flag -s "$smt2_options" {} "$bin_dir" "$logdir" -- $all_tests + parallel -i $j_param bash "${BASH_SOURCE%/*}/run_test.sh" $color_flag -s "$smt2_options" {} "$bin_dir" "$logdir" -- $all_tests ;; gnu) - parallel -q bash "${BASH_SOURCE%/*}/run_test.sh" $color_flag -s "$smt2_options" {} "$bin_dir" "$logdir" ::: $all_tests + parallel -q $j_param bash "${BASH_SOURCE%/*}/run_test.sh" $color_flag -s "$smt2_options" {} "$bin_dir" "$logdir" ::: $all_tests ;; *) for file in $all_tests; do @@ -144,6 +160,12 @@ case "$run_parallel" in ;; esac +# give back tokens +while [[ $job_count -gt 1 ]]; do + echo -n '+' >&"$fdW" + job_count=$((job_count-1)) +done + pass=$(find "$logdir" -type f -name "*.pass" | wc -l) fail=$(find "$logdir" -type f -name "*.error" | wc -l) From bba1dd359d8f9c0a85e548a577342a6ea6595393 Mon Sep 17 00:00:00 2001 From: Thomas Hader Date: Tue, 20 Feb 2024 17:54:36 -0800 Subject: [PATCH 14/15] Fixed for newer make versions --- tests/regress/check.sh | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/tests/regress/check.sh b/tests/regress/check.sh index 0216ccd92..62d7d3ed0 100755 --- a/tests/regress/check.sh +++ b/tests/regress/check.sh @@ -131,13 +131,18 @@ job_count=1 if [ -n "$parallel_tool" ]; then if [[ -n "$j_option" ]]; then job_count=0 - elif [[ "$MAKEFLAGS" == *"jobserver-fds="* ]] || [[ "$MAKEFLAGS" == *"jobserver-auth="* ]]; then + elif [[ "$MAKEFLAGS" =~ --jobserver-(fds\|auth)=([0-9]+),([0-9]+) ]]; then # greedy get as many tokens as possible fdR=$(echo "$MAKEFLAGS" | sed -E "s|.*--jobserver-(fds\|auth)=([0-9]+),([0-9]+).*|\2|") fdW=$(echo "$MAKEFLAGS" | sed -E "s|.*--jobserver-(fds\|auth)=([0-9]+),([0-9]+).*|\3|") while IFS= read -r -d '' -t 1 -n 1 <&"$fdR"; do job_count=$((job_count+1)) done + elif [[ "$MAKEFLAGS" =~ --jobserver-auth=fifo:([^ ]+) ]]; then + fifo=$(echo "$MAKEFLAGS" | sed -E "s|.*--jobserver-auth=fifo:([^ ]+).*|\1|") + while IFS= read -r -d '' -t 1 -n 1 <"$fifo"; do + job_count=$((job_count+1)) + done elif [[ "$MAKEFLAGS" =~ (^|[ ])-?j($|[ ]) ]]; then job_count=0 fi @@ -162,8 +167,9 @@ esac # give back tokens while [[ $job_count -gt 1 ]]; do - echo -n '+' >&"$fdW" - job_count=$((job_count-1)) + [[ -n $fdW ]] && echo -n '+' >&"$fdW" + [[ -n $fifo ]] && echo -n '+' >"$fifo" + job_count=$((job_count-1)) done pass=$(find "$logdir" -type f -name "*.pass" | wc -l) From 62cc24f7fdc14f1715af3eed51afd1451c723123 Mon Sep 17 00:00:00 2001 From: Thomas Hader Date: Tue, 20 Feb 2024 18:29:12 -0800 Subject: [PATCH 15/15] Added cleanupto check.sh --- tests/regress/check.sh | 52 +++++++++++++++++++++++++++--------------- 1 file changed, 33 insertions(+), 19 deletions(-) diff --git a/tests/regress/check.sh b/tests/regress/check.sh index 62d7d3ed0..0849f6ea7 100755 --- a/tests/regress/check.sh +++ b/tests/regress/check.sh @@ -39,6 +39,10 @@ usage() { exit } +cleanup() { + [[ -n "$logdir" ]] && rm -rf "$logdir" +} + smt2_options= j_option= @@ -94,6 +98,7 @@ fi # # The temp file for output # +trap cleanup EXIT logdir=$($mktemp_cmd -d) || { echo "Can't create temp folder" ; exit 1 ; } if [[ -z "$REGRESS_FILTER" ]]; @@ -128,24 +133,34 @@ fi job_count=1 #check if we are in a make run with -j N -if [ -n "$parallel_tool" ]; then - if [[ -n "$j_option" ]]; then - job_count=0 - elif [[ "$MAKEFLAGS" =~ --jobserver-(fds\|auth)=([0-9]+),([0-9]+) ]]; then - # greedy get as many tokens as possible - fdR=$(echo "$MAKEFLAGS" | sed -E "s|.*--jobserver-(fds\|auth)=([0-9]+),([0-9]+).*|\2|") - fdW=$(echo "$MAKEFLAGS" | sed -E "s|.*--jobserver-(fds\|auth)=([0-9]+),([0-9]+).*|\3|") - while IFS= read -r -d '' -t 1 -n 1 <&"$fdR"; do - job_count=$((job_count+1)) - done - elif [[ "$MAKEFLAGS" =~ --jobserver-auth=fifo:([^ ]+) ]]; then - fifo=$(echo "$MAKEFLAGS" | sed -E "s|.*--jobserver-auth=fifo:([^ ]+).*|\1|") - while IFS= read -r -d '' -t 1 -n 1 <"$fifo"; do - job_count=$((job_count+1)) - done - elif [[ "$MAKEFLAGS" =~ (^|[ ])-?j($|[ ]) ]]; then - job_count=0 - fi +if [[ -n "$j_option" ]]; then + job_count=0 +elif [[ "$MAKEFLAGS" =~ --jobserver-(fds|auth)=([0-9]+),([0-9]+) ]]; then + # greedy get as many tokens as possible + fdR=$(echo "$MAKEFLAGS" | sed -E "s|.*--jobserver-(fds\|auth)=([0-9]+),([0-9]+).*|\2|") + fdW=$(echo "$MAKEFLAGS" | sed -E "s|.*--jobserver-(fds\|auth)=([0-9]+),([0-9]+).*|\3|") + while IFS= read -r -d '' -t 1 -n 1 <&"$fdR"; do + job_count=$((job_count+1)) + done +elif [[ "$MAKEFLAGS" =~ --jobserver-auth=fifo:([^ ]+) ]]; then + fifo=$(echo "$MAKEFLAGS" | sed -E "s|.*--jobserver-auth=fifo:([^ ]+).*|\1|") + while IFS= read -r -d '' -t 1 -n 1 <"$fifo"; do + job_count=$((job_count+1)) + done +elif [[ "$MAKEFLAGS" =~ (^|[ ])-?j($|[ ]) ]]; then + job_count=0 +fi + +if [[ $job_count != 1 ]] && [[ -z "$parallel_tool" ]]; then + echo "**********************************************************" + echo "Install moreutils or GNU parallel to run tests in parallel" + echo "**********************************************************" +else + case $job_count in + 0) echo "Running in parallel";; + 1) echo "Running sequentially";; + *) echo "Running with $job_count parallel jobs";; + esac fi j_param="-j$job_count" @@ -188,5 +203,4 @@ else code=1 fi -rm -rf "$logdir" exit $code