chore(shell/CMakeLists): leanpkg integration tests

src/shell/CMakeLists.txt

@@ -215,6 +215,16 @@ FOREACH(T ${SMT2RUNTESTS})
            COMMAND bash "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T_NAME})
 ENDFOREACH(T)
 
+# LEANPKG TESTS
+file(GLOB LEANPKGTESTS "${LEAN_SOURCE_DIR}/../tests/lean/leanpkg/*.sh")
+FOREACH(T ${LEANPKGTESTS})
+  GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
+  if(NOT T_NAME MATCHES "test_single.sh")
+  add_test(NAME "leanpkgtest_${T_NAME}"
+           WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/leanpkg/"
+           COMMAND bash "./test_single.sh" "${LEAN_SOURCE_DIR}/../bin/lean" ${T_NAME})
+  endif()
+ENDFOREACH(T)
 
 # LEAN TESTS using --trust=0
 file(GLOB LEANT0TESTS "${LEAN_SOURCE_DIR}/../tests/lean/trust0/*.lean")

tests/lean/leanpkg/test_single.sh

@@ -0,0 +1,58 @@
+#!/usr/bin/env bash
+if [ $# -ne 3 -a $# -ne 2 ]; then
+    echo "Usage: test_single.sh [lean-executable-path] [file] [yes/no]?"
+    exit 1
+fi
+ulimit -s 8192
+export PATH=$(dirname $(../readlinkf.sh "$1")):$PATH
+export LEAN_PATH=../../library:.
+if [ $# -ne 3 ]; then
+    INTERACTIVE=no
+else
+    INTERACTIVE=$3
+fi
+f=$2
+ff=$(../readlinkf.sh "$f")
+
+if [[ "$OSTYPE" == "msys" ]]; then
+    # Windows running MSYS2
+    # Replace /c/ with c:, and / with \\
+    ff=$(echo $ff  | sed 's|^/\([a-z]\)/|\1:/|' | sed 's|/|\\\\|g')
+fi
+
+DIFF=diff
+if diff --color --help >/dev/null 2>&1; then
+  DIFF="diff --color";
+fi
+
+echo "-- testing $f"
+bash "$ff" >& "$f.tmp"
+echo $? >> "$f.tmp"
+
+sed -E "s|^[^ ]*[/\\\\]||" "$f.tmp" | sed "/WARNING: Lean version mismatch/d" > "$f.produced.out"
+rm "$f.tmp"
+if test -f "$f.expected.out"; then
+    if $DIFF -u --ignore-all-space -I "executing external script" "$f.expected.out" "$f.produced.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.expected.out" "$f.produced.out"; then
+                echo "-- mismatch was fixed"
+            fi
+        fi
+        exit 1
+    fi
+else
+    echo "ERROR: file $f.expected.out does not exist"
+    if [ $INTERACTIVE == "yes" ]; then
+        read -p "copy $f.produced.out (y/n)? "
+        if [ $REPLY == "y" ]; then
+            cp -- "$f.produced.out" "$f.expected.out"
+            echo "-- copied $f.produced.out --> $f.expected.out"
+        fi
+    fi
+    exit 1
+fi