diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index 46159b1594..eed749e315 100644 --- a/src/shell/CMakeLists.txt +++ b/src/shell/CMakeLists.txt @@ -204,6 +204,15 @@ FOREACH(T_OUT ${LEANBENCHTESTS}) COMMAND bash "./test_single.sh" ${T_NAME}) ENDFOREACH(T_OUT) +# LEAN PLUGIN TESTS +file(GLOB LEANINTERPTESTS "${LEAN_SOURCE_DIR}/../tests/plugin/*.lean") +FOREACH(T ${LEANINTERPTESTS}) + GET_FILENAME_COMPONENT(T_NAME ${T} NAME) + add_test(NAME "leanplugintest_${T_NAME}" + WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/plugin" + COMMAND bash "./test_single.sh" ${T_NAME}) +ENDFOREACH(T) + # LEANPKG TESTS # file(GLOB LEANPKGTESTS "${LEAN_SOURCE_DIR}/../tests/lean/leanpkg/*.sh") # FOREACH(T ${LEANPKGTESTS}) diff --git a/tests/plugin/Default.lean b/tests/plugin/Default.lean new file mode 100644 index 0000000000..b4d574ce82 --- /dev/null +++ b/tests/plugin/Default.lean @@ -0,0 +1,15 @@ +import Init.Lean + +open Lean + +def oh_no : Nat := 0 + +def snakeLinter : Linter := +fun env n => + -- TODO(Sebastian): return actual message with position from syntax tree + if n.toString.contains '_' then throw "SNAKES!!" + else pure MessageLog.empty + +@[init] +def registerSnakeLinter : IO Unit := +addLinter snakeLinter diff --git a/tests/plugin/Default.lean.expected.out b/tests/plugin/Default.lean.expected.out new file mode 100644 index 0000000000..d730c18cb4 --- /dev/null +++ b/tests/plugin/Default.lean.expected.out @@ -0,0 +1 @@ +Default.lean:5:4: error: SNAKES!! diff --git a/tests/plugin/test_single.sh b/tests/plugin/test_single.sh new file mode 100755 index 0000000000..11600b8801 --- /dev/null +++ b/tests/plugin/test_single.sh @@ -0,0 +1,65 @@ +#!/usr/bin/env bash +if [ $# -ne 2 -a $# -ne 1 ]; then + echo "Usage: test_single.sh [file] [yes/no]?" + exit 1 +fi +ulimit -s 8192 +BIN_DIR=../../bin +export LEAN_PATH=../../library:. +if [ $# -ne 2 ]; then + INTERACTIVE=no +else + INTERACTIVE=$2 +fi +f=$1 +ff=$(../lean/readlinkf.sh "$f") + +if [[ "$OSTYPE" == "msys" ]]; then + # Windows running MSYS2 + # Replace /c/ with c:, and / with \\ + ff=$(echo $ff | sed 's|^/\([a-z]\)/|\1:/|' | sed 's|/|\\\\|g') +fi + +DIFF=diff +if diff --color --help >/dev/null 2>&1; then + DIFF="diff --color"; +fi + +$BIN_DIR/lean --c="$ff".c "$ff" +if [ $? -ne 0 ]; then + echo "Failed to compile $ff into C file" + exit 1 +fi + +$BIN_DIR/leanc -O3 -DNDEBUG -shared -o "$ff.so" $ff.c +if [ $? -ne 0 ]; then + echo "Failed to compile C file $ff.c" + exit 1 +fi + +$BIN_DIR/lean --plugin="$ff.so" "$ff" | sed "s|^$ff|$f|" > "$f.produced.out" +if test -f "$f.expected.out"; then + if $DIFF -u --ignore-all-space -I "executing external script" "$f.expected.out" "$f.produced.out"; then + echo "-- checked" + exit 0 + else + echo "ERROR: file $f.produced.out does not match $f.expected.out" + if [ $INTERACTIVE == "yes" ]; then + meld "$f.produced.out" "$f.expected.out" + if diff -I "executing external script" "$f.expected.out" "$f.produced.out"; then + echo "-- mismatch was fixed" + fi + fi + exit 1 + fi +else + echo "ERROR: file $f.expected.out does not exist" + if [ $INTERACTIVE == "yes" ]; then + read -p "copy $f.produced.out (y/n)? " + if [ $REPLY == "y" ]; then + cp -- "$f.produced.out" "$f.expected.out" + echo "-- copied $f.produced.out --> $f.expected.out" + fi + fi + exit 1 +fi