-
Notifications
You must be signed in to change notification settings - Fork 0
/
run_experiments.sh
executable file
·71 lines (62 loc) · 1.5 KB
/
run_experiments.sh
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
#!/bin/bash
# Terminal colors
BLUE='\033[1;34m'
PURPLE='\033[1;35m'
RED='\033[1;31m'
GREEN='\033[1;32m'
NC='\033[0m'
EXP_PATH="./experiments/"
CERT_PATH="./$EXP_PATH/ho_poly_certificates"
# Delete old certificates
rm -rf ./$EXP_PATH/$CERT_PATH
rm -rf .nia.cache
# Create new certificate folder
mkdir -p $CERT_PATH
# Execute onijn on experiment data and generate the corresponding Coq certificates.
FILES="./$EXP_PATH/ho_poly/*"
for f in $FILES
do
g=${f::${#f}-6}
dune exec -- onijn $f -o $g.v
mv $g.v "$CERT_PATH"
done
FILES="./$CERT_PATH/*.v"
fail=0
timeout=0
success=0
total=0
for f in $FILES
do
ext=${f: -2}
if [ $ext == ".v" ]
then
total=$((total+1))
echo "Compiling proof script: $f"
timeout 300s time coqc $f
err=$?
if [ $err == "0" ]
then
success=$((success+1))
printf "${GREEN}success${NC}\n"
else
if [ $err == "1" ]
then
fail=$((fail+1))
printf "${RED}fail${NC}\n"
else
if [ $err == "124" ]
then
timeout=$((timeout+1))
printf "${PURPLE}timeout${NC}\n"
fi
fi
fi
fi
done
echo "Results"
echo "------------------------------------------------------------------------"
printf "${GREEN}Success:${NC} $success\n"
printf "${RED}Fail:${NC} $fail\n"
printf "${PURPLE}Timeout:${NC} $timeout\n"
printf "${BLUE}Total:${NC} $total\n"
echo "------------------------------------------------------------------------"