From 52a52fbed73761db2d22e6d63c83915e94a00985 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 24 Mar 2022 15:20:18 -0700
Subject: [PATCH] chore: add `doc/examples` to the test suite

---
 doc/examples/test_single.sh |  4 ++++
 src/shell/CMakeLists.txt    | 11 +++++++++++
 2 files changed, 15 insertions(+)
 create mode 100755 doc/examples/test_single.sh

diff --git a/doc/examples/test_single.sh b/doc/examples/test_single.sh
new file mode 100755
index 0000000000..8ca4f4d2f7
--- /dev/null
+++ b/doc/examples/test_single.sh
@@ -0,0 +1,4 @@
+#!/usr/bin/env bash
+source ../../tests/common.sh
+
+exec_check lean -j 0 "$f"
diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt
index 78493d2513..b9b815ff77 100644
--- a/src/shell/CMakeLists.txt
+++ b/src/shell/CMakeLists.txt
@@ -71,6 +71,17 @@ FOREACH(T ${LEANRUNTESTS})
   endif()
 ENDFOREACH(T)
 
+# LEAN RUN doc/examples
+file(GLOB LEANDOCEXS "${LEAN_SOURCE_DIR}/../doc/examples/*.lean")
+FOREACH(T ${LEANDOCEXS})
+  if(NOT T MATCHES "\\.#")
+    GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
+    add_test(NAME "leandocex_${T_NAME}"
+             WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../doc/examples"
+             COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}")
+  endif()
+ENDFOREACH(T)
+
 # LEAN COMPILER TESTS
 file(GLOB LEANCOMPTESTS "${LEAN_SOURCE_DIR}/../tests/compiler/*.lean")
 FOREACH(T ${LEANCOMPTESTS})