From: Benjamin Barenblat Date: Sun, 11 Aug 2019 18:33:23 +0200 Subject: Disable tests which require -coqlib to be set Forwarded: not-needed A number of tests (mostly for coq_makefile) assume that Coq is installed when the test runs. This isn't true in an sbuild environment, though, so disable those tests. --- test-suite/coq-makefile/arg/run.sh | 7 -- test-suite/coq-makefile/compat-subdirs/run.sh | 8 -- test-suite/coq-makefile/coqdoc1/run.sh | 59 -------------- test-suite/coq-makefile/coqdoc2/run.sh | 57 -------------- test-suite/coq-makefile/emptyprefix/run.sh | 17 ---- test-suite/coq-makefile/extend-subdirs/run.sh | 8 -- test-suite/coq-makefile/findlib-package/run.sh | 19 ----- test-suite/coq-makefile/latex1/run.sh | 13 --- test-suite/coq-makefile/merlin1/run.sh | 13 --- test-suite/coq-makefile/mlpack1/run.sh | 23 ------ test-suite/coq-makefile/mlpack2/run.sh | 23 ------ test-suite/coq-makefile/multiroot/run.sh | 61 -------------- test-suite/coq-makefile/only/run.sh | 10 --- test-suite/coq-makefile/plugin1/run.sh | 26 ------ test-suite/coq-makefile/plugin2/run.sh | 26 ------ test-suite/coq-makefile/plugin3/run.sh | 26 ------ test-suite/coq-makefile/quick2vo/run.sh | 12 --- test-suite/coq-makefile/timing/run.sh | 105 ------------------------- test-suite/coq-makefile/uninstall1/run.sh | 23 ------ test-suite/coq-makefile/uninstall2/run.sh | 23 ------ test-suite/coq-makefile/validate1/run.sh | 8 -- test-suite/coq-makefile/vio2vo/run.sh | 13 --- test-suite/misc/printers.sh | 2 - 23 files changed, 582 deletions(-) delete mode 100755 test-suite/coq-makefile/arg/run.sh delete mode 100755 test-suite/coq-makefile/compat-subdirs/run.sh delete mode 100755 test-suite/coq-makefile/coqdoc1/run.sh delete mode 100755 test-suite/coq-makefile/coqdoc2/run.sh delete mode 100755 test-suite/coq-makefile/emptyprefix/run.sh delete mode 100755 test-suite/coq-makefile/extend-subdirs/run.sh delete mode 100755 test-suite/coq-makefile/findlib-package/run.sh delete mode 100755 test-suite/coq-makefile/latex1/run.sh delete mode 100755 test-suite/coq-makefile/merlin1/run.sh delete mode 100755 test-suite/coq-makefile/mlpack1/run.sh delete mode 100755 test-suite/coq-makefile/mlpack2/run.sh delete mode 100755 test-suite/coq-makefile/multiroot/run.sh delete mode 100755 test-suite/coq-makefile/only/run.sh delete mode 100755 test-suite/coq-makefile/plugin1/run.sh delete mode 100755 test-suite/coq-makefile/plugin2/run.sh delete mode 100755 test-suite/coq-makefile/plugin3/run.sh delete mode 100755 test-suite/coq-makefile/quick2vo/run.sh delete mode 100755 test-suite/coq-makefile/timing/run.sh delete mode 100755 test-suite/coq-makefile/uninstall1/run.sh delete mode 100755 test-suite/coq-makefile/uninstall2/run.sh delete mode 100755 test-suite/coq-makefile/validate1/run.sh delete mode 100755 test-suite/coq-makefile/vio2vo/run.sh delete mode 100755 test-suite/misc/printers.sh --- coq.orig/test-suite/coq-makefile/arg/run.sh +++ /dev/null @@ -1,7 +0,0 @@ -#!/usr/bin/env bash - -. ../template/init.sh - -coq_makefile -f _CoqProject -o Makefile -cat Makefile.conf -make --- coq.orig/test-suite/coq-makefile/coqdoc1/run.sh +++ /dev/null @@ -1,76 +0,0 @@ -#!/usr/bin/env bash - -. ../template/init.sh - -coq_makefile -f _CoqProject -o Makefile -cat Makefile.conf -make -make html mlihtml -make install DSTROOT="$PWD/tmp" -make install-doc DSTROOT="$PWD/tmp" -#make debug - -# to learn about <(cmd) see https://www.gnu.org/software/bash/manual/html_node/Process-Substitution.html -( - while IFS= read -r -d '' d - do - pushd "$d" >/dev/null && find . && popd >/dev/null - done < <(find tmp -name user-contrib -print0) -) | sort -u > actual - -sort -u > desired < actual -sort > desired </dev/null && find . && popd >/dev/null - done < <(find tmp -name user-contrib -print0) -) | sort -u > actual - -sort -u > desired < actual -sort > desired <> src/test_aux.ml -if which cygpath 2>/dev/null; then - # separator is ; on windows - OCAMLPATH=$OCAMLPATH;$(cygpath -m "$PWD"/findlib) -else - OCAMLPATH=$OCAMLPATH:$PWD/findlib -fi -export OCAMLPATH -make -C findlib/foo clean -coq_makefile -f _CoqProject -o Makefile -cat Makefile.conf -cat Makefile.local -make -C findlib/foo -make -make byte --- coq.orig/test-suite/coq-makefile/latex1/run.sh +++ /dev/null @@ -1,13 +0,0 @@ -#!/usr/bin/env bash - -if which pdflatex; then - -. ../template/init.sh - -coq_makefile -f _CoqProject -o Makefile -cat Makefile.conf -make -exec make all.pdf - -fi -exit 0 # test skipped --- coq.orig/test-suite/coq-makefile/merlin1/run.sh +++ /dev/null @@ -1,13 +0,0 @@ -#!/usr/bin/env bash - -. ../template/init.sh - -coq_makefile -f _CoqProject -o Makefile -cat Makefile.conf -make .merlin -cat > desired < actual -exec diff -u desired actual --- coq.orig/test-suite/coq-makefile/mlpack1/run.sh +++ /dev/null @@ -1,36 +0,0 @@ -#!/usr/bin/env bash - -. ../template/init.sh - -coq_makefile -f _CoqProject -o Makefile -cat Makefile.conf -make -make html mlihtml -make install DSTROOT="$PWD/tmp" -#make debug -(cd "$(find tmp -name user-contrib)" && find .) | sort > actual -sort > desired < actual -sort > desired < actual -sort > desired < actual -sort > desired </dev/null && find . && popd >/dev/null - done < <(find tmp -name user-contrib -print0) -) | sort -u > actual -sort > desired < actual -sort > desired < actual -sort > desired < actual -sort > desired < actual -sort > desired < actual -sort > desired < actual -sort > desired < actual -sort > desired </dev/null && find . && popd >/dev/null - done < <(find tmp \( -name user-contrib -o -name coq-test-suite \) -print0) -) | sort -u > actual -sort -u > desired </dev/null && find . && popd >/dev/null - done < <(find tmp -name user-contrib -print0) -) | sort -u > actual -sort -u > desired <&1 | tee "$f" - -# if there's an issue in base_include 'go' won't be defined -# if there's an issue in include_printers it will be an undefined printer -if ! grep -q -F 'val go : unit -> unit = ' "$f" || - grep -q -E "Error|Unbound" "$f"; -then exit 1; fi --- coq.orig/test-suite/coq-makefile/timing/run.sh +++ /dev/null @@ -1,117 +0,0 @@ -#!/usr/bin/env bash - -#set -x -set -e - -# tools -TTOOLSDIR="$COQPREFIX/lib/coq-core/tools" - -export make_both_time_files="$TTOOLSDIR"/make-both-time-files.py -export make_one_time_file="$TTOOLSDIR"/make-one-time-file.py -export make_both_single_timing_files="$TTOOLSDIR"/make-both-single-timing-files.py - -# -NONATIVECOMP=$(grep "let native_compiler = NativeOff" ../../../config/coq_config.ml)||true -if [[ ! $NONATIVECOMP ]]; then exit 0 ; fi - -. ../template/path-init.sh - -# reset MAKEFLAGS so that, e.g., `make -C test-suite -B coq-makefile` doesn't give us issues - -MAKEFLAGS= - -cd precomputed-time-tests -./run.sh || exit $? - -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 TIMING_SORT_BY=diff TIME_OF_BUILD_BEFORE_FILE=../before/time-of-build-before.log -cp ../before/time-of-build-before.log ./ -make print-pretty-timed-diff TIMING_SORT_BY=diff || exit $? - -INFINITY="∞" -INFINITY_REPLACEMENT="+.%" # assume that if the before time is zero, we expected the time to increase - -TO_SED_IN_BOTH=( - -e s"/${INFINITY}/${INFINITY_REPLACEMENT}/g" # Whether or not something shows up as ∞ depends on whether a time registers as 0.s or as 0.001s, so we can't rely on this being consistent - -e s':|\s*N/A\s*$:| '"${INFINITY_REPLACEMENT}"':g' # Whether or not something shows up as N/A depends on whether a time registers as 0.s or as 0.001s, so we can't rely on this being consistent - -e s'/ *$//g' # the number of trailing spaces depends on how many digits percentages end up being; since this varies across runs, we remove trailing spaces - -e s'/[0-9]*\.[0-9]*//g' # the precise timing numbers vary, so we strip them out - -e s'/^-*$/------/g' # When none of the numbers get over 100 (or 1000, in per-file), the width of the table is different, so we normalize the number of dashes for table separators - -e s'/+/-/g' # some code lines don't really change, but this can show up as either -0m00.01s or +0m00.01s, so we need to normalize the signs; additionally, some N/A's show up where we expect to get -∞ on the per-line file, and so the ∞-replacement gets the sign wrong, so we must correct it - -e s'/[0-9]//g' # sometimes the time is under 1 minute, sometimes it's over 1 minute, so we want to remove/normalize both instances; see https://github.com/coq/coq/issues/5675#issuecomment-487378622 -) - -TO_SED_IN_PER_FILE=( - -e s'/ */ /g' # unclear whether this is actually needed for per-file timing; it's been here from the start - -e s'/\(Total.*\)-\(.*\)-/\1+\2+/g' # Overall time in the per-file timing diff should be around 0; if it comes out negative, we remove the sign - -e s'/- ko/ko/g' # for small amounts of memory, signs can flip, so we remove mem signs -) - -TO_SED_IN_PER_LINE=( - -e s'/ */ /g' # Sometimes 0 will show up as 0m00.s, sometimes it'll end up being more like 0m00.001s; we must strip out the spaces that result from left-aligning numbers of different widths based on how many digits Coq's [-time] gives - -e s'/^ *//g' # the number of leading spaces can differ, e.g., as in the difference between ' 0m13.53s' vs '0m13.582s' - ) - -for file in time-of-build-before.log time-of-build-after.log time-of-build-both.log; do - for ext in "" .desired; do - sed "${TO_SED_IN_BOTH[@]}" "${TO_SED_IN_PER_FILE[@]}" ${file}${ext} > ${file}${ext}.processed - done - echo "cat $file" - cat "$file" - echo - 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 $? -echo "cat A.v.before-timing" -cat A.v.before-timing -echo -echo "cat A.v.after-timing" -cat A.v.after-timing -echo -echo "cat A.v.timing.diff" -cat A.v.timing.diff -echo - -file=A.v.timing.diff - -for ext in "" .desired; do - sed "${TO_SED_IN_BOTH[@]}" "${TO_SED_IN_PER_LINE[@]}" < "${file}${ext}" | sort > "${file}${ext}.processed" -done - -diff -u "$file.desired.processed" "$file.processed" || exit $? - -exit 0