From 8243ed63399ff15079cbec99a2e534c10a1ca660 Mon Sep 17 00:00:00 2001
From: Soonho Kong <soonhok@cs.cmu.edu>
Date: Sat, 28 Mar 2015 23:29:52 -0400
Subject: [PATCH] fix(test*.sh): allow spaces in filename

fix #515
---
 doc/lean/test.sh                      |  4 ++--
 doc/lean/test_single.sh               | 14 +++++++-------
 doc/lua/test.sh                       |  4 ++--
 doc/lua/test_single.sh                |  6 +++---
 script/lcov.sh                        |  8 ++++----
 src/shell/CMakeLists.txt              |  2 +-
 src/shell/mk_lean_sh.sh               |  6 +++---
 tests/lean/extra/ac_bug.sh            |  6 +++---
 tests/lean/extra/test_eqn_macro.sh    |  4 ++--
 tests/lean/extra/test_single.sh       |  2 +-
 tests/lean/hott/test_single.sh        |  2 +-
 tests/lean/interactive/test_single.sh | 14 +++++++-------
 tests/lean/run/test_single.sh         |  2 +-
 tests/lean/slow/test_single.sh        |  2 +-
 tests/lean/test.sh                    | 16 ++++++++--------
 tests/lean/test_single.sh             | 18 +++++++++---------
 tests/lean/test_single_pp.sh          | 12 ++++++------
 tests/lean/trust0/test_single.sh      |  7 ++++---
 tests/lua/test.sh                     |  2 +-
 tests/lua/test_single.sh              |  4 ++--
 20 files changed, 68 insertions(+), 67 deletions(-)

diff --git a/doc/lean/test.sh b/doc/lean/test.sh
index a7a27dc6a..051b89492 100755
--- a/doc/lean/test.sh
+++ b/doc/lean/test.sh
@@ -9,8 +9,8 @@ LEAN=$1
 NUM_ERRORS=0
 for f in `ls *.md`; do
     echo "-- testing $f"
-    awk 'BEGIN{ in_block = 0 } !/```/{ if (in_block == 1) print $0; else print "" } /```/ && !/```lean/{ in_block = 0; print "" } /```lean/{ in_block = 1; print "" }' $f > $f.lean
-    if $LEAN $f.lean > $f.produced.out; then
+    awk 'BEGIN{ in_block = 0 } !/```/{ if (in_block == 1) print $0; else print "" } /```/ && !/```lean/{ in_block = 0; print "" } /```lean/{ in_block = 1; print "" }' "$f" > "$f.lean"
+    if "$LEAN" "$f.lean" > "$f.produced.out"; then
         echo "-- worked"
     else
         echo "ERROR executing $f.lean, produced output is at $f.produced.out"
diff --git a/doc/lean/test_single.sh b/doc/lean/test_single.sh
index 2acbc4900..1ce2baa3c 100755
--- a/doc/lean/test_single.sh
+++ b/doc/lean/test_single.sh
@@ -19,22 +19,22 @@ while read -r line; do
         in_code_block=1
         i=$((i + 1))
         lastbegin=$linenum
-        rm -f $f.$i.lean
+        rm -f -- "$f.$i.lean"
     elif [[ $line =~ ^#\+END_SRC ]]; then
         if [[ $in_code_block -eq 1 ]]; then
-            if $LEAN -t 100000 $f.$i.lean > $f.$i.produced.out; then
+            if "$LEAN" -t 100000 "$f.$i.lean" > "$f.$i.produced.out"; then
                 echo "code fragment #$i worked"
             else
                 echo "ERROR executing $f.$i.lean, for in_code_block block starting at $lastbegin, produced output:"
-                cat  $f.$i.produced.out
+                cat  "$f.$i.produced.out"
                 exit 1
             fi
         fi
         in_code_block=0
     elif [[ $in_code_block -eq 1 ]]; then
-        echo -E "$line" >> $f.$i.lean
+        echo -E "$line" >> "$f.$i.lean"
     fi
-done < $f
-rm -f $f.*.produced.out
-rm -f $f.*.lean
+done < "$f"
+rm -f "$f.*.produced.out"
+rm -f "$f.*.lean"
 exit 0
diff --git a/doc/lua/test.sh b/doc/lua/test.sh
index e9e5d4316..22c3189f4 100755
--- a/doc/lua/test.sh
+++ b/doc/lua/test.sh
@@ -9,8 +9,8 @@ LEAN=$1
 NUM_ERRORS=0
 for f in `ls *.md`; do
     echo "-- testing $f"
-    awk 'BEGIN{ in_block = 0 } !/```/{ if (in_block == 1) print $0; else print "" } /```/ && !/```lua/{ in_block = 0; print "" } /```lua/{ in_block = 1; print "" }' $f > $f.lua
-    if $LEAN $f.lua > $f.produced.out; then
+    awk 'BEGIN{ in_block = 0 } !/```/{ if (in_block == 1) print $0; else print "" } /```/ && !/```lua/{ in_block = 0; print "" } /```lua/{ in_block = 1; print "" }' "$f" > "$f.lua"
+    if "$LEAN" "$f.lua" > "$f.produced.out"; then
         echo "-- worked"
     else
         echo "ERROR executing $f.lua, produced output is at $f.produced.out"
diff --git a/doc/lua/test_single.sh b/doc/lua/test_single.sh
index 5faa8bcfd..c5d65b10c 100755
--- a/doc/lua/test_single.sh
+++ b/doc/lua/test_single.sh
@@ -8,12 +8,12 @@ ulimit -s unlimited
 LEAN=$1
 f=$2
 echo "-- testing $f"
-awk 'BEGIN{ in_block = 0 } !/```/{ if (in_block == 1) print $0; else print "" } /```/ && !/```lua/{ in_block = 0; print "" } /```lua/{ in_block = 1; print "" }' $f > $f.lua
-if $LEAN $f.lua > $f.produced.out; then
+awk 'BEGIN{ in_block = 0 } !/```/{ if (in_block == 1) print $0; else print "" } /```/ && !/```lua/{ in_block = 0; print "" } /```lua/{ in_block = 1; print "" }' "$f" > "$f.lua"
+if "$LEAN" "$f.lua" > "$f.produced.out"; then
     echo "-- worked"
     exit 0
 else
     echo "ERROR executing $f.lua, produced output:"
-    cat  $f.produced.out
+    cat  "$f.produced.out"
     exit 1
 fi
diff --git a/script/lcov.sh b/script/lcov.sh
index 16a0f6444..c0707c9d8 100755
--- a/script/lcov.sh
+++ b/script/lcov.sh
@@ -7,10 +7,10 @@ GENHTML=~/bin/genhtml
 rm -rf build
 mkdir -p build/testcov
 cd build/testcov
-cmake -DCMAKE_BUILD_TYPE=TESTCOV -DCMAKE_CXX_COMPILER=$CXX ../../src
+cmake -DCMAKE_BUILD_TYPE=TESTCOV -DCMAKE_CXX_COMPILER="$CXX" ../../src
 make
 ctest
-$LCOV -c -b ../../src -d . -o cov.info --no-external --gcov-tool $GCOV_TOOL
-$LCOV --remove cov.info "tests/*" -o cov.info
-$GENHTML cov.info --output-directory lcov
+"$LCOV" -c -b ../../src -d . -o cov.info --no-external --gcov-tool "$GCOV_TOOL"
+"$LCOV" --remove cov.info "tests/*" -o cov.info
+"$GENHTML" cov.info --output-directory lcov
 cd ../../
diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt
index 5bab86e03..56aa9f116 100644
--- a/src/shell/CMakeLists.txt
+++ b/src/shell/CMakeLists.txt
@@ -77,7 +77,7 @@ FOREACH(T ${LEANT0TESTS})
   GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
   add_test(NAME "leant0test_${T_NAME}"
            WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/trust0"
-           COMMAND bash "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean -t 0" ${T_NAME})
+           COMMAND bash "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T_NAME} "-t 0")
 ENDFOREACH(T)
 
 # LEAN RUN HoTT TESTS
diff --git a/src/shell/mk_lean_sh.sh b/src/shell/mk_lean_sh.sh
index eb04a89f2..0551b4e9b 100755
--- a/src/shell/mk_lean_sh.sh
+++ b/src/shell/mk_lean_sh.sh
@@ -6,8 +6,8 @@ if [ -x "$DEST/lean.sh" ]; then
     # Nothing to be done, file already exists
     exit 0
 else
-    cat > $DEST/lean.sh <<EOF
-if ! $DEST/lean \$* ; then echo "FAILED: \$*"; exit 1; fi
+    cat > "$DEST/lean.sh" <<EOF
+if ! "$DEST/lean" \$* ; then echo "FAILED: \$*"; exit 1; fi
 EOF
-    chmod +x $DEST/lean.sh
+    chmod +x "$DEST/lean.sh"
 fi
diff --git a/tests/lean/extra/ac_bug.sh b/tests/lean/extra/ac_bug.sh
index aecc6c5d2..f44dcac47 100755
--- a/tests/lean/extra/ac_bug.sh
+++ b/tests/lean/extra/ac_bug.sh
@@ -9,11 +9,11 @@ LEAN=$1
 export LEAN_PATH=../../../library:.
 for f in `ls ac_bug*.input`; do
     echo "testing $f..."
-    $LEAN --server-trace $f > $f.produced.out
-    if grep "nat.mul.assoc" $f.produced.out; then
+    "$LEAN" --server-trace "$f" > "$f.produced.out"
+    if grep "nat.mul.assoc" "$f.produced.out"; then
         echo "FAILED"
         exit 1
     fi
-    rm -f $f.produced.out
+    rm -f -- "$f.produced.out"
 done
 echo "done"
diff --git a/tests/lean/extra/test_eqn_macro.sh b/tests/lean/extra/test_eqn_macro.sh
index 913559444..80ac7efe3 100755
--- a/tests/lean/extra/test_eqn_macro.sh
+++ b/tests/lean/extra/test_eqn_macro.sh
@@ -6,5 +6,5 @@ if [ $# -ne 1 ]; then
 fi
 LEAN=$1
 export LEAN_PATH=../../../library:.
-$LEAN -o eqn_macro1.olean eqn_macro1.lean
-$LEAN eqn_macro2.lean
+"$LEAN" -o eqn_macro1.olean eqn_macro1.lean
+"$LEAN" eqn_macro2.lean
diff --git a/tests/lean/extra/test_single.sh b/tests/lean/extra/test_single.sh
index 1339f11d6..0cce45ba6 100755
--- a/tests/lean/extra/test_single.sh
+++ b/tests/lean/extra/test_single.sh
@@ -8,7 +8,7 @@ LEAN=$1
 export LEAN_PATH=../../../library:.
 f=$2
 echo "-- testing $f"
-if $LEAN $f; then
+if "$LEAN" "$f"; then
    echo "-- checked"
 else
    echo "failed $f"
diff --git a/tests/lean/hott/test_single.sh b/tests/lean/hott/test_single.sh
index 3184dc115..308d3ee22 100755
--- a/tests/lean/hott/test_single.sh
+++ b/tests/lean/hott/test_single.sh
@@ -8,7 +8,7 @@ LEAN=$1
 export HLEAN_PATH=../../../hott:.
 f=$2
 echo "-- testing $f"
-if $LEAN $f; then
+if "$LEAN" "$f"; then
    echo "-- checked"
 else
    echo "failed $f"
diff --git a/tests/lean/interactive/test_single.sh b/tests/lean/interactive/test_single.sh
index f89bfb290..5f5d3cb72 100755
--- a/tests/lean/interactive/test_single.sh
+++ b/tests/lean/interactive/test_single.sh
@@ -13,20 +13,20 @@ else
 fi
 f=$2
 echo "-- testing $f"
-$LEAN -D pp.unicode=true --server < $f > $f.produced.out
-if test -f $f.expected.out; then
-    if diff --ignore-all-space $f.produced.out $f.expected.out; then
+"$LEAN" -D pp.unicode=true --server < "$f" > "$f.produced.out"
+if test -f "$f.expected.out"; then
+    if diff --ignore-all-space "$f.produced.out" "$f.expected.out"; then
         echo "-- checked"
         exit 0
     else
         echo "ERROR: file $f.produced.out does not match $f.expected.out"
         if [ $INTERACTIVE == "yes" ]; then
-            meld $f.produced.out $f.expected.out
-            if diff --ignore-all-space $f.produced.out $f.expected.out; then
+            meld "$f.produced.out" "$f.expected.out"
+            if diff --ignore-all-space "$f.produced.out" "$f.expected.out"; then
                 echo "-- mismath was fixed"
             fi
         else
-            diff --ignore-all-space $f.produced.out $f.expected.out
+            diff --ignore-all-space "$f.produced.out" "$f.expected.out"
         fi
         exit 1
     fi
@@ -35,7 +35,7 @@ else
     if [ $INTERACTIVE == "yes" ]; then
         read -p "copy $f.produced.out (y/n)? "
         if [ $REPLY == "y" ]; then
-            cp $f.produced.out $f.expected.out
+            cp -- "$f.produced.out" "$f.expected.out"
             echo "-- copied $f.produced.out --> $f.expected.out"
         fi
     fi
diff --git a/tests/lean/run/test_single.sh b/tests/lean/run/test_single.sh
index 1339f11d6..0cce45ba6 100755
--- a/tests/lean/run/test_single.sh
+++ b/tests/lean/run/test_single.sh
@@ -8,7 +8,7 @@ LEAN=$1
 export LEAN_PATH=../../../library:.
 f=$2
 echo "-- testing $f"
-if $LEAN $f; then
+if "$LEAN" "$f"; then
    echo "-- checked"
 else
    echo "failed $f"
diff --git a/tests/lean/slow/test_single.sh b/tests/lean/slow/test_single.sh
index 1339f11d6..0cce45ba6 100755
--- a/tests/lean/slow/test_single.sh
+++ b/tests/lean/slow/test_single.sh
@@ -8,7 +8,7 @@ LEAN=$1
 export LEAN_PATH=../../../library:.
 f=$2
 echo "-- testing $f"
-if $LEAN $f; then
+if "$LEAN" "$f"; then
    echo "-- checked"
 else
    echo "failed $f"
diff --git a/tests/lean/test.sh b/tests/lean/test.sh
index 2a0607802..11787a083 100755
--- a/tests/lean/test.sh
+++ b/tests/lean/test.sh
@@ -15,18 +15,18 @@ fi
 NUM_ERRORS=0
 for f in *.lean; do
     echo "-- testing $f"
-    $LEAN -t config.lean $f &> $f.produced.out.1
-    sed "/warning: imported file uses 'sorry'/d" $f.produced.out.1 > $f.produced.out
-    rm -f $f.produced.out.1
-    if test -f $f.expected.out; then
-        if diff -I "executing external script" $f.produced.out $f.expected.out; then
+    "$LEAN" -t config.lean "$f" &> "$f.produced.out.1"
+    sed "/warning: imported file uses 'sorry'/d" "$f.produced.out.1" > "$f.produced.out"
+    rm -f -- "$f.produced.out.1"
+    if test -f "$f.expected.out"; then
+        if diff -I "executing external script" "$f.produced.out" "$f.expected.out"; then
             echo "-- checked"
         else
             echo "ERROR: file $f.produced.out does not match $f.expected.out"
             NUM_ERRORS=$(($NUM_ERRORS+1))
             if [ $INTERACTIVE == "yes" ]; then
-                meld $f.produced.out $f.expected.out
-                if diff -I "executing external script" $f.produced.out $f.expected.out; then
+                meld "$f.produced.out" "$f.expected.out"
+                if diff -I "executing external script" "$f.produced.out" "$f.expected.out"; then
                     echo "-- mismath was fixed"
                 fi
             fi
@@ -37,7 +37,7 @@ for f in *.lean; do
         if [ $INTERACTIVE == "yes" ]; then
             read -p "copy $f.produced.out (y/n)? "
             if [ $REPLY == "y" ]; then
-                cp $f.produced.out $f.expected.out
+                cp -- "$f.produced.out" "$f.expected.out"
                 echo "-- copied $f.produced.out --> $f.expected.out"
             fi
         fi
diff --git a/tests/lean/test_single.sh b/tests/lean/test_single.sh
index aebfdd271..91e7c0322 100755
--- a/tests/lean/test_single.sh
+++ b/tests/lean/test_single.sh
@@ -21,22 +21,22 @@ else
 fi
 
 echo "-- testing $f"
-$LEAN $CONFIG $f &> $f.produced.out.1
-sed "/warning: imported file uses 'sorry'/d" $f.produced.out.1 > $f.produced.out
-rm -f $f.produced.out.1
-if test -f $f.expected.out; then
-    if diff --ignore-all-space -I "executing external script" $f.produced.out $f.expected.out; then
+"$LEAN" $CONFIG "$f" &> "$f.produced.out.1"
+sed "/warning: imported file uses 'sorry'/d" "$f.produced.out.1" > "$f.produced.out"
+rm -f "$f.produced.out.1"
+if test -f "$f.expected.out"; then
+    if diff --ignore-all-space -I "executing external script" "$f.produced.out" "$f.expected.out"; then
         echo "-- checked"
         exit 0
     else
         echo "ERROR: file $f.produced.out does not match $f.expected.out"
         if [ $INTERACTIVE == "yes" ]; then
-            meld $f.produced.out $f.expected.out
-            if diff -I "executing external script" $f.produced.out $f.expected.out; then
+            meld "$f.produced.out" "$f.expected.out"
+            if diff -I "executing external script" "$f.produced.out" "$f.expected.out"; then
                 echo "-- mismath was fixed"
             fi
         else
-            diff --ignore-all-space -I "executing external script" $f.produced.out $f.expected.out
+            diff --ignore-all-space -I "executing external script" "$f.produced.out" "$f.expected.out"
         fi
         exit 1
     fi
@@ -45,7 +45,7 @@ else
     if [ $INTERACTIVE == "yes" ]; then
         read -p "copy $f.produced.out (y/n)? "
         if [ $REPLY == "y" ]; then
-            cp $f.produced.out $f.expected.out
+            cp -- "$f.produced.out" "$f.expected.out"
             echo "-- copied $f.produced.out --> $f.expected.out"
         fi
     fi
diff --git a/tests/lean/test_single_pp.sh b/tests/lean/test_single_pp.sh
index bf24352a1..37ffd31f3 100755
--- a/tests/lean/test_single_pp.sh
+++ b/tests/lean/test_single_pp.sh
@@ -9,12 +9,12 @@ ulimit -s 8192
 LEAN=$1
 f=$2
 echo "-- testing $f"
-$LEAN $f showenv.l &> $f.pp.out
-if grep "===BEGIN ENVIRONMENT===" $f.pp.out; then
-   awk 'BEGIN { SHOW = 0 } { if (SHOW == 1) print $0 } /===BEGIN ENVIRONMENT===/ { SHOW = 1 }' $f.pp.out > $f.pp
-   rm -f $f.pp.out
-   if $LEAN $f.pp; then
-      rm -f $f.pp
+"$LEAN" "$f" showenv.l &> "$f.pp.out"
+if grep "===BEGIN ENVIRONMENT===" "$f.pp.out"; then
+   awk 'BEGIN { SHOW = 0 } { if (SHOW == 1) print $0 } /===BEGIN ENVIRONMENT===/ { SHOW = 1 }' "$f.pp.out" > "$f.pp"
+   rm -f -- "$f.pp.out"
+   if "$LEAN" "$f.pp"; then
+      rm -f -- "$f.pp"
       echo "-- checked"
    else
       echo "-- failed to parse output produced by Lean"
diff --git a/tests/lean/trust0/test_single.sh b/tests/lean/trust0/test_single.sh
index 1339f11d6..41b6c6fa9 100755
--- a/tests/lean/trust0/test_single.sh
+++ b/tests/lean/trust0/test_single.sh
@@ -1,14 +1,15 @@
 #!/usr/bin/env bash
-if [ $# -ne 2 ]; then
-    echo "Usage: test_single.sh [lean-executable-path] [file]"
+if [ $# -lt 2 ]; then
+    echo "Usage: test_single.sh [lean-executable-path] [file] [options]"
     exit 1
 fi
 ulimit -s 8192
 LEAN=$1
 export LEAN_PATH=../../../library:.
 f=$2
+shift 2
 echo "-- testing $f"
-if $LEAN $f; then
+if "$LEAN" "$f" $@; then
    echo "-- checked"
 else
    echo "failed $f"
diff --git a/tests/lua/test.sh b/tests/lua/test.sh
index 9bdcf1e5b..d8df10a6e 100755
--- a/tests/lua/test.sh
+++ b/tests/lua/test.sh
@@ -9,7 +9,7 @@ LEAN=$1
 NUM_ERRORS=0
 for f in *.lua; do
     echo "-- testing $f"
-    if $LEAN extra.lua $f > $f.produced.out; then
+    if "$LEAN" "extra.lua" "$f" > "$f.produced.out"; then
         echo "-- worked"
     else
         echo "ERROR executing $f, produced output is at $f.produced.out"
diff --git a/tests/lua/test_single.sh b/tests/lua/test_single.sh
index b268ce7c1..c604486ba 100755
--- a/tests/lua/test_single.sh
+++ b/tests/lua/test_single.sh
@@ -7,11 +7,11 @@ ulimit -s unlimited
 LEAN=$1
 f=$2
 echo "-- testing $f"
-if $LEAN extra.lua $f > $f.produced.out; then
+if "$LEAN" extra.lua "$f" > "$f.produced.out"; then
     echo "-- worked"
     exit 0
 else
     echo "ERROR executing $f, produced output:"
-    cat $f.produced.out
+    cat "$f.produced.out"
     exit 1
 fi