1#!/bin/bash 2 3source ../../.acl2holrc.bash 4 5round_trip_dir=${ACL2_HOL}/tests/round-trip 6results_dir=$round_trip_dir/results 7old_results_dir=$round_trip_dir/old-results 8logs_dir=$round_trip_dir/logs 9old_logs_dir=$round_trip_dir/old-logs 10gold_dir=$round_trip_dir/gold 11lisp_dir=${ACL2_HOL}/lisp 12 13if [ "$*" = "clean" ]; then \ 14 rm -rf $results_dir $old_results_dir $logs_dir $old_logs_dir diffout diffout.old ; \ 15 exit 0 ; \ 16fi 17 18echo "Making books in $lisp_dir..." 19pushd $lisp_dir > /dev/null 20make 21popd > /dev/null 22 23echo "Converting .lisp files to their essences..." 24 25rm -rf $old_results_dir 26if [ -e $results_dir ]; then mv $results_dir $old_results_dir ; fi 27mkdir $results_dir 28 29rm -rf $old_logs_dir 30if [ -e $logs_dir ]; then mv $logs_dir $old_logs_dir ; fi 31mkdir $logs_dir 32 33if [ -e diffout ]; then mv diffout diffout.old ; fi 34 35(${ACL2_HOL_LISP}/axioms-essence.csh $results_dir/axioms.lisp) > $logs_dir/axioms.out 2> $logs_dir/axioms.err ; \ 36 37(${ACL2_HOL_LISP}/a2ml.csh $gold_dir/axioms.lisp $results_dir/axioms.sml) > $logs_dir/axioms.sml.out 2> $logs_dir/axioms.sml.err ; \ 38 39(diff -x .svn $results_dir $gold_dir 2>&1) > diffout 40 41if [ -s diffout ] ; then \ 42 echo '***Failure*** for round-trip testing! See diffout for diffs, and see logs/.' ; \ 43 exit 1 ; \ 44else \ 45 echo 'Success for round-trip testing!' ; \ 46 exit 0 ; \ 47fi 48