git.iko.soy/Idris-dev
on master help sign in
Merge pull request #2106 from melted/great_expectations
bedca84David Christiansen
test/basic010/run+31−25
compare with master
unifiedsplit
@@ -1,28 +1,5 @@
1#!/usr/bin/env bash
1#!/usr/bin/env bash
2
2
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
3
27declare -a extraargs
4declare -a extraargs
28for arg in "$@"
5for arg in "$@"
@@ -30,6 +7,35 @@ do
30 extraargs=("${extraargs[@]}" "'$arg'")
7 extraargs=("${extraargs[@]}" "'$arg'")
31done
8done
32
9
10+if (which timeout&>/dev/null); then
11+ timeout 10 idris $@ Main.idr --nocolour --check --warnreach -o basic010
12+ timeout 5 ./basic010
13+else
14+ # From http://unix.stackexchange.com/questions/43340/how-to-introduce-timeout-for-shell-scripting
15+ # Here copied from reg039.
16+ #
17+ # Executes command with a timeout
18+ # Params:
19+ # $1 timeout in seconds
20+ # $2 command
21+ # Returns 1 if timed out 0 otherwise
22+ timeout() {
23+
24+ time=$1
25+
26+ # start the command in a subshell to avoid problem with pipes
27+ # (spawn accepts one command)
28+ command="/bin/sh -c \"$2\""
29+
30+ expect -c "set echo \"-noecho\"; set timeout $time; spawn -noecho $command; expect timeout { exit 1 } eof { exit 0 }"
31+
32+ if [ $? = 1 ] ; then
33+ echo "Timeout after ${time} seconds"
34+ fi
35+
36+ }
37+
33−timeout 10 "idris ${extraargs[*]} Main.idr --nocolour --check --warnreach -o basic010"
38+ timeout 10 "idris ${extraargs[*]} Main.idr --nocolour --check --warnreach -o basic010"
34−timeout 5 "./basic010"
39+ timeout 5 "./basic010"
40+fi
35rm -f *.ibc basic010
41rm -f *.ibc basic010
test/reg039/run+27−24
@@ -1,32 +1,35 @@
1#!/usr/bin/env bash
1#!/usr/bin/env bash
2
2
3−# From http://unix.stackexchange.com/questions/43340/how-to-introduce-timeout-for-shell-scripting
4−# Executes command with a timeout
5−# Params:
6−# $1 timeout in seconds
7−# $2 command
8−# Returns 1 if timed out 0 otherwise
9−timeout() {
10−
11− time=$1
12−
13− # start the command in a subshell to avoid problem with pipes
14− # (spawn accepts one command)
15− command="/bin/sh -c \"$2\""
16−
17− expect -c "set echo \"-noecho\"; set timeout $time; spawn -noecho $command; expect timeout { exit 1 } eof { exit 0 }"
18−
19− if [ $? = 1 ] ; then
20− echo "Timeout after ${time} seconds"
21− fi
22−
23−}
24
3
25declare -a extraargs
4declare -a extraargs
26for arg in "$@"
5for arg in "$@"
27do
6do
28 extraargs=("${extraargs[@]}" "'$arg'")
7 extraargs=("${extraargs[@]}" "'$arg'")
29done
8done
30−
9+if (which timeout&>/dev/null); then
10+ timeout 60 idris $@ --nocolour reg039.idr --exec go
11+else
12+ # From http://unix.stackexchange.com/questions/43340/how-to-introduce-timeout-for-shell-scripting
13+ # Executes command with a timeout
14+ # Params:
15+ # $1 timeout in seconds
16+ # $2 command
17+ # Returns 1 if timed out 0 otherwise
18+ timeout() {
19+
20+ time=$1
21+
22+ # start the command in a subshell to avoid problem with pipes
23+ # (spawn accepts one command)
24+ command="/bin/sh -c \"$2\""
25+
26+ expect -c "set echo \"-noecho\"; set timeout $time; spawn -noecho $command; expect timeout { exit 1 } eof { exit 0 }"
27+
28+ if [ $? = 1 ] ; then
29+ echo "Timeout after ${time} seconds"
30+ fi
31+
32+ }
31−timeout 60 "idris ${extraargs[*]} --nocolour reg039.idr --exec go"
33+ timeout 60 "idris ${extraargs[*]} --nocolour reg039.idr --exec go"
34+ fi
32−rm -f reg039 *.ibc
35+ rm -f reg039 *.ibc