1#!/bin/bash 2 3source ../.acl2holrc.bash 4 5tests_dir=${ACL2_HOL}/tests 6inputs_dir=$tests_dir/inputs 7results_dir=$tests_dir/results 8old_results_dir=$tests_dir/old-results 9logs_dir=$tests_dir/logs 10old_logs_dir=$tests_dir/old-logs 11gold_dir=$tests_dir/gold 12lisp_dir=${ACL2_HOL}/lisp 13 14my_status=0 15 16my_args=$* 17 18if [ "$my_args" = "clean+" ]; then \ 19 pushd $lisp_dir ; \ 20 make clean ; \ 21 my_args=clean ; \ 22 popd ; \ 23fi 24 25if [ "$my_args" = "clean" ]; then \ 26 rm -f diffout diffout.old 2> /dev/null ; \ 27 rm -rf $results_dir $old_results_dir $logs_dir $old_logs_dir ; \ 28 cd $inputs_dir ; make clean ; cd .. ; \ 29 cd round-trip ; ./doit clean ; cd .. ; \ 30 exit 0 ; \ 31fi 32 33echo "Making books in $lisp_dir..." ; cd $lisp_dir ; make -s ; temp_status=$? ; cd .. 34if [ $temp_status -ne 0 ]; then echo "***Failure making books in $lisp_dir" ; my_status=1 ; fi 35 36echo "Making books in $inputs_dir..." ; cd $inputs_dir ; make -s ; temp_status=$? ; cd .. 37if [ $temp_status -ne 0 ]; then echo "***Failure making books in $inputs_dir" ; my_status=1 ; fi 38 39echo "Converting .lisp files to their essences..." 40 41tests=`ls $inputs_dir/*.lisp` 42 43rm -rf $old_results_dir 44if [ -e $results_dir ]; then mv $results_dir $old_results_dir ; fi 45mkdir $results_dir 46 47rm -rf $old_logs_dir 48if [ -e $logs_dir ]; then mv $logs_dir $old_logs_dir ; fi 49mkdir $logs_dir 50 51if [ -e diffout ]; then mv diffout diffout.old ; fi 52 53for test in $tests ; do \ 54 test=${test##*/} ; \ 55 (${ACL2_HOL_LISP}/book-essence.csh $inputs_dir/$test $results_dir/$test) > $logs_dir/$test.out 2> $logs_dir/$test.err ; \ 56 testr=${test%.*} ; \ 57 (${ACL2_HOL_LISP}/a2ml.csh $results_dir/$test $results_dir/$testr.sml $inputs_dir) > $logs_dir/$test.sml.out 2> $logs_dir/$test.sml.err ; \ 58done 59 60(diff -x .svn $results_dir $gold_dir 2>&1) > diffout 61 62if [ -s diffout ] ; then \ 63 echo '***Failure*** for main tests! See diffout and round-trip/diffout for diffs, and see logs/.' ; \ 64 my_status=1 ; \ 65else \ 66 echo 'Success for main tests!' ; \ 67fi 68 69echo "Entering round-trip/ directory..." 70pushd round-trip > /dev/null 71./doit 72temp_status=$? 73# Note that round-trip/doit does its own success/failure printing 74if [ $my_status -eq 0 ]; then my_status=$temp_status ; fi 75popd > /dev/null 76 77if [ $my_status -eq 0 ] ; then \ 78 echo 'SUCCESS!' ; \ 79 exit 0 ; \ 80else \ 81 echo 'FAILURE! See failure message(s) above.' ; \ 82 exit $my_status ; \ 83fi 84