mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-11-10 15:16:54 +03:00
Don't require expect for tests with timeouts
Turns out there's a timeout command in core utils that is convenient. Fixes basic010 and reg039 on Windows.
This commit is contained in:
parent
2e919c86d0
commit
c47608d968
@ -1,28 +1,5 @@
|
||||
#!/usr/bin/env bash
|
||||
|
||||
# From http://unix.stackexchange.com/questions/43340/how-to-introduce-timeout-for-shell-scripting
|
||||
# Here copied from reg039.
|
||||
#
|
||||
# Executes command with a timeout
|
||||
# Params:
|
||||
# $1 timeout in seconds
|
||||
# $2 command
|
||||
# Returns 1 if timed out 0 otherwise
|
||||
timeout() {
|
||||
|
||||
time=$1
|
||||
|
||||
# start the command in a subshell to avoid problem with pipes
|
||||
# (spawn accepts one command)
|
||||
command="/bin/sh -c \"$2\""
|
||||
|
||||
expect -c "set echo \"-noecho\"; set timeout $time; spawn -noecho $command; expect timeout { exit 1 } eof { exit 0 }"
|
||||
|
||||
if [ $? = 1 ] ; then
|
||||
echo "Timeout after ${time} seconds"
|
||||
fi
|
||||
|
||||
}
|
||||
|
||||
declare -a extraargs
|
||||
for arg in "$@"
|
||||
@ -30,6 +7,35 @@ do
|
||||
extraargs=("${extraargs[@]}" "'$arg'")
|
||||
done
|
||||
|
||||
timeout 10 "idris ${extraargs[*]} Main.idr --nocolour --check --warnreach -o basic010"
|
||||
timeout 5 "./basic010"
|
||||
if (which timeout&>/dev/null); then
|
||||
timeout 10 idris $@ Main.idr --nocolour --check --warnreach -o basic010
|
||||
timeout 5 ./basic010
|
||||
else
|
||||
# From http://unix.stackexchange.com/questions/43340/how-to-introduce-timeout-for-shell-scripting
|
||||
# Here copied from reg039.
|
||||
#
|
||||
# Executes command with a timeout
|
||||
# Params:
|
||||
# $1 timeout in seconds
|
||||
# $2 command
|
||||
# Returns 1 if timed out 0 otherwise
|
||||
timeout() {
|
||||
|
||||
time=$1
|
||||
|
||||
# start the command in a subshell to avoid problem with pipes
|
||||
# (spawn accepts one command)
|
||||
command="/bin/sh -c \"$2\""
|
||||
|
||||
expect -c "set echo \"-noecho\"; set timeout $time; spawn -noecho $command; expect timeout { exit 1 } eof { exit 0 }"
|
||||
|
||||
if [ $? = 1 ] ; then
|
||||
echo "Timeout after ${time} seconds"
|
||||
fi
|
||||
|
||||
}
|
||||
|
||||
timeout 10 "idris ${extraargs[*]} Main.idr --nocolour --check --warnreach -o basic010"
|
||||
timeout 5 "./basic010"
|
||||
fi
|
||||
rm -f *.ibc basic010
|
||||
|
@ -1,32 +1,35 @@
|
||||
#!/usr/bin/env bash
|
||||
|
||||
# From http://unix.stackexchange.com/questions/43340/how-to-introduce-timeout-for-shell-scripting
|
||||
# Executes command with a timeout
|
||||
# Params:
|
||||
# $1 timeout in seconds
|
||||
# $2 command
|
||||
# Returns 1 if timed out 0 otherwise
|
||||
timeout() {
|
||||
|
||||
time=$1
|
||||
|
||||
# start the command in a subshell to avoid problem with pipes
|
||||
# (spawn accepts one command)
|
||||
command="/bin/sh -c \"$2\""
|
||||
|
||||
expect -c "set echo \"-noecho\"; set timeout $time; spawn -noecho $command; expect timeout { exit 1 } eof { exit 0 }"
|
||||
|
||||
if [ $? = 1 ] ; then
|
||||
echo "Timeout after ${time} seconds"
|
||||
fi
|
||||
|
||||
}
|
||||
|
||||
declare -a extraargs
|
||||
for arg in "$@"
|
||||
do
|
||||
extraargs=("${extraargs[@]}" "'$arg'")
|
||||
done
|
||||
if (which timeout&>/dev/null); then
|
||||
timeout 60 idris $@ --nocolour reg039.idr --exec go
|
||||
else
|
||||
# From http://unix.stackexchange.com/questions/43340/how-to-introduce-timeout-for-shell-scripting
|
||||
# Executes command with a timeout
|
||||
# Params:
|
||||
# $1 timeout in seconds
|
||||
# $2 command
|
||||
# Returns 1 if timed out 0 otherwise
|
||||
timeout() {
|
||||
|
||||
timeout 60 "idris ${extraargs[*]} --nocolour reg039.idr --exec go"
|
||||
rm -f reg039 *.ibc
|
||||
time=$1
|
||||
|
||||
# start the command in a subshell to avoid problem with pipes
|
||||
# (spawn accepts one command)
|
||||
command="/bin/sh -c \"$2\""
|
||||
|
||||
expect -c "set echo \"-noecho\"; set timeout $time; spawn -noecho $command; expect timeout { exit 1 } eof { exit 0 }"
|
||||
|
||||
if [ $? = 1 ] ; then
|
||||
echo "Timeout after ${time} seconds"
|
||||
fi
|
||||
|
||||
}
|
||||
timeout 60 "idris ${extraargs[*]} --nocolour reg039.idr --exec go"
|
||||
fi
|
||||
rm -f reg039 *.ibc
|
||||
|
Loading…
Reference in New Issue
Block a user