@@ -1,5 +1,35 @@
11#!/usr/bin/env bash
22
3−idris $@ Main.idr --nocolour --check --warnreach -o basic010
4−./basic010
3+# From http://unix.stackexchange.com/questions/43340/how-to-introduce-timeout-for-shell-scripting
4+# Here copied from reg039.
5+#
6+# Executes command with a timeout
7+# Params:
8+# $1 timeout in seconds
9+# $2 command
10+# Returns 1 if timed out 0 otherwise
11+timeout() {
12+
13+ time=$1
14+
15+ # start the command in a subshell to avoid problem with pipes
16+ # (spawn accepts one command)
17+ command="/bin/sh -c \"$2\""
18+
19+ expect -c "set echo \"-noecho\"; set timeout $time; spawn -noecho $command; expect timeout { exit 1 } eof { exit 0 }"
20+
21+ if [ $? = 1 ] ; then
22+ echo "Timeout after ${time} seconds"
23+ fi
24+
25+}
26+
27+declare -a extraargs
28+for arg in "$@"
29+do
30+ extraargs=("${extraargs[@]}" "'$arg'")
31+done
32+
33+timeout 10 "idris ${extraargs[*]} Main.idr --nocolour --check --warnreach -o basic010"
34+timeout 5 "./basic010"
535rm -f *.ibc basic010