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