diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt
index 09df59afe2..6b571939aa 100644
--- a/src/shell/CMakeLists.txt
+++ b/src/shell/CMakeLists.txt
@@ -175,6 +175,17 @@ FOREACH(T ${LEANRUNTESTS})
   endif()
 ENDFOREACH(T)
 
+# LEAN new frontend TESTS
+file(GLOB LEANNEWFRONTENDTESTS "${LEAN_SOURCE_DIR}/../tests/lean/newfrontend/*.lean")
+FOREACH(T ${LEANNEWFRONTENDTESTS})
+  if(NOT T MATCHES "\\.#")
+    GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
+    add_test(NAME "leannewfrontendtest_${T_NAME}"
+             WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/newfrontend"
+             COMMAND bash "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T_NAME})
+  endif()
+ENDFOREACH(T)
+
 # LEAN FAIL TESTS
 file(GLOB LEANFAILTESTS "${LEAN_SOURCE_DIR}/../tests/lean/fail/*.lean")
 FOREACH(T ${LEANFAILTESTS})
diff --git a/tests/lean/newfrontend/t1.lean b/tests/lean/newfrontend/t1.lean
new file mode 100644
index 0000000000..50ecb9dc2e
--- /dev/null
+++ b/tests/lean/newfrontend/t1.lean
@@ -0,0 +1,3 @@
+variable {α : Type}
+def f (a : α) : α := a
+#check f 1
diff --git a/tests/lean/newfrontend/test_single.sh b/tests/lean/newfrontend/test_single.sh
new file mode 100755
index 0000000000..2ce4caf9cd
--- /dev/null
+++ b/tests/lean/newfrontend/test_single.sh
@@ -0,0 +1,18 @@
+#!/usr/bin/env bash
+if [ $# -ne 2 ]; then
+    echo "Usage: test_single.sh [lean-executable-path] [file]"
+    exit 1
+fi
+ulimit -s 8192
+LEAN=$1
+export LEAN_PATH=Init=../../../src/Init:Test=.
+f=$2
+echo "-- testing $f"
+"$LEAN" -j 0 --new-frontend "$f"
+status=$?
+if [ "$status" -eq 0 ]; then
+    echo "-- checked"
+else
+    echo "failed $f"
+    exit 1
+fi