Commit 1aba0115 authored by Heiko Becker's avatar Heiko Becker
Browse files

Add conversion script to easily format experiment data

parent 6acb343b
#!/usr/bin/env python3
import sys
def parseTime (timeStr):
timeL = timeStr.split(":")
time_sec_micro = timeL [len(timeL)-1].split(".")
timeL.pop(len(timeL)-1)
#We have already taken away the seoncds and microseconds value --> start with minutes
multiplier = 60
res = 0
for val in reversed(timeL):
res = res + (int (val) * multiplier)
multiplier = multiplier * 60
#Add seconds
res += int(time_sec_micro[0])
#Round to next second
if (int (time_sec_micro[1]) > 0):
res += 1
return res
def convert (fname):
fileo = open (fname, "r")
out = open (fname+"converted.txt", "w")
for line in fileo:
spl_line = line.split (" ")
timeInSeconds = parseTime (spl_line[len(spl_line)-1])
#remove already parsed time from list
spl_line.pop(len(spl_line)-1)
curr_line = ""
for val in spl_line:
curr_line += str(val)
curr_line += ", " + str(timeInSeconds) + "\n"
out.write (curr_line)
fileo.close()
out.close()
def main():
#get file name from argument list
fname = sys.argv[1]
convert(fname)
if __name__ == "__main__" :
main()
...@@ -7,7 +7,7 @@ ...@@ -7,7 +7,7 @@
# # # #
#################################################################################### ####################################################################################
#Configure a 20 minute stimeout for the HOL-Light scripts #Configure a 40 minute stimeout for the HOL-Light scripts
TIMEOUT=40m TIMEOUT=40m
arr=() arr=()
...@@ -21,10 +21,10 @@ do ...@@ -21,10 +21,10 @@ do
echo "Coq certificate" echo "Coq certificate"
/usr/bin/time -o $1 -a -f "%C %E" ./daisy $file --certificate=coq >/dev/null /usr/bin/time -o $1 -a -f "%C %E" ./daisy $file --certificate=coq >/dev/null
echo "HOL Certificate" echo "HOL Certificate"
/usr/bin/time -o $1 -a -f "%C %E" ./daisy $file --certificate=hol >/dev/null /usr/bin/time -o $1 -a -f "%C %E" ./daisy $file --certificate=hol4 >/dev/null
echo "" echo ""
done done
#
echo "" echo ""
echo "[Certificate Test]" echo "[Certificate Test]"
echo "" echo ""
...@@ -42,20 +42,18 @@ do ...@@ -42,20 +42,18 @@ do
/usr/bin/time -o $1 -a -f "%C %E" coqc -R ./ Daisy $file /usr/bin/time -o $1 -a -f "%C %E" coqc -R ./ Daisy $file
done done
cd ../hol cd ../hol4/output
#cd hol
arrHOL=() arrHOL=()
while IFS= read -r -d $'\0'; do while IFS= read -r -d $'\0'; do
arrHOL+=("$REPLY") arrHOL+=("$REPLY")
done < <(find ./output/ -name "*.hl" -print0) done < <(find ./ -name "*Script.sml" -print0)
for file in "${arrHOL[@]}" for file in "${arrHOL[@]}"
do do
echo $file echo $file
echo "" echo ""
echo $file >> $1 timeout $TIMEOUT /usr/bin/time -o $1 -a -f "%C %E" $HOLDIR/bin/Holmake ${file/Script.sml/Theory.sig}
timeout $TIMEOUT /usr/bin/time -o $1 -a -f "%C %E" ocaml<$file &>.$file
RETVAL=$? RETVAL=$?
if [ $RETVAL -eq 124 ] if [ $RETVAL -eq 124 ]
then echo "TIMEOUT "$file then echo "TIMEOUT "$file
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment