From 2b4bd660811743d6053b63d87f7f27b692a7f144 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 28 Jul 2014 12:06:11 -0700
Subject: [PATCH] feat(build): generate tests for all code blocks in org-files,
 and examples at ./examples/standard

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 doc/lean/test_single.sh    | 45 ++++++++++++++++++++++++++++----------
 doc/lean/tutorial.org      |  6 ++---
 src/shell/CMakeLists.txt   | 31 +++++++++++++-------------
 src/shell/test_standard.sh |  5 +++++
 4 files changed, 57 insertions(+), 30 deletions(-)
 create mode 100755 src/shell/test_standard.sh

diff --git a/doc/lean/test_single.sh b/doc/lean/test_single.sh
index 8b62fa723..0bd2a0fac 100755
--- a/doc/lean/test_single.sh
+++ b/doc/lean/test_single.sh
@@ -1,19 +1,40 @@
-#!/bin/sh
-# Test is all examples in the .md files are working
+#!/bin/bash
+# Test is all examples in the .org files are working
 if [ $# -ne 2 ]; then
-    echo "Usage: test.sh [lean-executable-path] [file]"
+    echo "Usage: test_single.sh [lean-executable-path] [file]"
     exit 1
 fi
 ulimit -s unlimited
 LEAN=$1
+export LEAN_PATH=.:../../library/standard
 f=$2
+i=0
+in_code_block=0
+lastbegin=0
+linenum=0
 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
-    echo "-- worked"
-    exit 0
-else
-    echo "ERROR executing $f.lean, produced output:"
-    cat  $f.produced.out
-    exit 1
-fi
+while read -r line; do
+    linenum=$((linenum + 1))
+    if [[ $line =~ ^#\+BEGIN_SRC\ lean ]]; then
+        in_code_block=1
+        i=$((i + 1))
+        lastbegin=$linenum
+        rm -f $f.$i.lean
+    elif [[ $line =~ ^#\+END_SRC ]]; then
+        if [[ $in_code_block -eq 1 ]]; then
+            if $LEAN $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
+                exit 1
+            fi
+        fi
+        in_code_block=0
+    elif [[ $in_code_block -eq 1 ]]; then
+        echo -E "$line" >> $f.$i.lean
+    fi
+done < $f
+rm -f *.produced.out
+rm -f *.lean
+exit 0
diff --git a/doc/lean/tutorial.org b/doc/lean/tutorial.org
index 76802a829..11d0861b9 100644
--- a/doc/lean/tutorial.org
+++ b/doc/lean/tutorial.org
@@ -267,7 +267,7 @@ explicitly.
 #+BEGIN_SRC lean
   import logic
 
-  definition id.{l} {A : Type.{l}} (a : A) : Type.{l}
+  definition id.{l} {A : Type.{l}} (a : A) : A
   := a
 
   check id true
@@ -607,7 +607,7 @@ The expression =(by simp [rule-set])= is similar to =_=, but it tells Lean to sy
 using the rewrite rule set named =[rule-set]=. In the following example, we create a simple rewrite rule set
 and use it to prove a theorem that would be quite tedious to prove by hand.
 
-#+BEGIN_SRC lean
+#+BEGIN_SRC
   -- import module that defines several tactics/strategies including "simp"
   import tactic
   -- create a rewrite rule set with name 'simple'
@@ -622,7 +622,7 @@ In Lean, we can combine manual and automated proofs in a natural way. We can man
 skeleton and use the =by= construct to invoke automated proof engines like the simplifier for filling the
 tedious steps. Here is a very simple example.
 
-#+BEGIN_SRC lean
+#+BEGIN_SRC
    theorem th2 (a b : Prop) : a ∧ b ↔ b ∧ a
    := iff_intro
         (fun H : a ∧ b, (by simp simple))
diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt
index eafd4b77b..cfdbc5a1b 100644
--- a/src/shell/CMakeLists.txt
+++ b/src/shell/CMakeLists.txt
@@ -23,13 +23,14 @@ add_test(lean_unknown_option ${LEAN_SOURCE_DIR}/cmake/check_failure.sh "${CMAKE_
 add_test(lean_unknown_file1 ${LEAN_SOURCE_DIR}/cmake/check_failure.sh "${CMAKE_CURRENT_BINARY_DIR}/lean" "boofoo.lean")
 add_test(lean_unknown_file2 ${LEAN_SOURCE_DIR}/cmake/check_failure.sh "${CMAKE_CURRENT_BINARY_DIR}/lean" "boofoo.lua")
 
-# # LEAN EXAMPLES
-# file(GLOB LEANEXAMPLES "${LEAN_SOURCE_DIR}/../examples/lean/*.lean")
-# FOREACH(T ${LEANEXAMPLES})
-#   GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
-#   add_test(NAME "leanex_${T_NAME}"
-#     COMMAND ${CMAKE_CURRENT_BINARY_DIR}/lean ${T})
-# ENDFOREACH(T)
+# LEAN EXAMPLES
+file(GLOB LEANEXAMPLES "${LEAN_SOURCE_DIR}/../examples/standard/*.lean")
+FOREACH(T ${LEANEXAMPLES})
+  GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
+  add_test(NAME "leanex_${T_NAME}"
+    WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../examples/standard"
+    COMMAND ${LEAN_SOURCE_DIR}/shell/test_standard.sh ${CMAKE_CURRENT_BINARY_DIR}/lean ${T})
+ENDFOREACH(T)
 
 # LEAN TESTS
 file(GLOB LEANTESTS "${LEAN_SOURCE_DIR}/../tests/lean/*.lean")
@@ -96,14 +97,14 @@ FOREACH(T ${LEANLUASLOWTESTS})
   set_tests_properties("leanluaslowtest_${T_NAME}" PROPERTIES LABELS "expensive")
 ENDFOREACH(T)
 
-# # LEAN DOCS
-# file(GLOB LEANDOCS "${LEAN_SOURCE_DIR}/../doc/lean/*.md")
-# FOREACH(T ${LEANDOCS})
-#   GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
-#   add_test(NAME "leandoc_${T_NAME}"
-#            WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../doc/lean"
-#            COMMAND "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean -t" ${T})
-# ENDFOREACH(T)
+# LEAN DOCS
+file(GLOB LEANDOCS "${LEAN_SOURCE_DIR}/../doc/lean/*.org")
+FOREACH(T ${LEANDOCS})
+  GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
+  add_test(NAME "leandoc_${T_NAME}"
+           WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../doc/lean"
+           COMMAND "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T})
+ENDFOREACH(T)
 
 # LEAN LUA DOCS
 file(GLOB LEANLUADOCS "${LEAN_SOURCE_DIR}/../doc/lua/*.md")
diff --git a/src/shell/test_standard.sh b/src/shell/test_standard.sh
new file mode 100755
index 000000000..45b670846
--- /dev/null
+++ b/src/shell/test_standard.sh
@@ -0,0 +1,5 @@
+#!/bin/bash
+LEAN=$1
+FILE=$2
+export LEAN_PATH=.:../../library/standard
+$LEAN $2