test(tests/lean): add new test script that checks if Lean can parse the output produced by its pretty printer

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/shell/CMakeLists.txt

@@ -39,6 +39,16 @@ FOREACH(T ${LEANTESTS})
            COMMAND "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T})
 ENDFOREACH(T)
 
+# LEAN PP TESTS
+# For making sure that Lean can parse the output produced by its pretty printer
+file(GLOB LEANPPTESTS "${LEAN_SOURCE_DIR}/../tests/lean/*.lean")
+FOREACH(T ${LEANPPTESTS})
+  GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
+  add_test(NAME "leanpptest_${T_NAME}"
+           WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean"
+           COMMAND "./test_single_pp.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T})
+ENDFOREACH(T)
+
 # LEAN INTERACTIVE TESTS
 file(GLOB LEANINTERACTIVETESTS "${LEAN_SOURCE_DIR}/../tests/lean/interactive/*.lean")
 FOREACH(T ${LEANINTERACTIVETESTS})

tests/lean/showenv.l

@@ -0,0 +1,3 @@
+SetOption pp::colors  false
+Echo "===BEGIN ENVIRONMENT==="
+Show Environment

tests/lean/test_single_pp.sh

@@ -0,0 +1,26 @@
+#!/bin/bash
+# Script for testing if Lean can parse the output produced by its
+# pretty printer
+if [ $# -ne 2 ]; then
+    echo "Usage: test_single_pp.sh [lean-executable-path] [file]"
+    exit 1
+fi
+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
+      echo "-- checked"
+   else
+      echo "-- failed to parse output produced by Lean"
+      exit 1
+   fi
+else
+   echo "-- unexpected output produced by Lean"
+   exit 1
+fi