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

@@ -1,19 +1,40 @@
-#!/bin/sh
+#!/bin/bash
-# Test is all examples in the .md files are working
+# 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
+while read -r line; do
-if $LEAN $f.lean > $f.produced.out; then
+    linenum=$((linenum + 1))
-    echo "-- worked"
+    if [[ $line =~ ^#\+BEGIN_SRC\ lean ]]; then
-    exit 0
+        in_code_block=1
-else
+        i=$((i + 1))
-    echo "ERROR executing $f.lean, produced output:"
+        lastbegin=$linenum
-    cat  $f.produced.out
+        rm -f $f.$i.lean
-    exit 1
+    elif [[ $line =~ ^#\+END_SRC ]]; then
-fi
+        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

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))

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
+# LEAN EXAMPLES
-# file(GLOB LEANEXAMPLES "${LEAN_SOURCE_DIR}/../examples/lean/*.lean")
+file(GLOB LEANEXAMPLES "${LEAN_SOURCE_DIR}/../examples/standard/*.lean")
-# FOREACH(T ${LEANEXAMPLES})
+FOREACH(T ${LEANEXAMPLES})
-#   GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
+  GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
-#   add_test(NAME "leanex_${T_NAME}"
+  add_test(NAME "leanex_${T_NAME}"
-#     COMMAND ${CMAKE_CURRENT_BINARY_DIR}/lean ${T})
+    WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../examples/standard"
-# ENDFOREACH(T)
+    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
+# LEAN DOCS
-# file(GLOB LEANDOCS "${LEAN_SOURCE_DIR}/../doc/lean/*.md")
+file(GLOB LEANDOCS "${LEAN_SOURCE_DIR}/../doc/lean/*.org")
-# FOREACH(T ${LEANDOCS})
+FOREACH(T ${LEANDOCS})
-#   GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
+  GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
-#   add_test(NAME "leandoc_${T_NAME}"
+  add_test(NAME "leandoc_${T_NAME}"
-#            WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../doc/lean"
+           WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../doc/lean"
-#            COMMAND "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean -t" ${T})
+           COMMAND "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T})
-# ENDFOREACH(T)
+ENDFOREACH(T)
 
 # LEAN LUA DOCS
 file(GLOB LEANLUADOCS "${LEAN_SOURCE_DIR}/../doc/lua/*.md")

src/shell/test_standard.sh

@@ -0,0 +1,5 @@
+#!/bin/bash
+LEAN=$1
+FILE=$2
+export LEAN_PATH=.:../../library/standard
+$LEAN $2