1#!/bin/sh 2 3# A shell script to build the various examples distributed with HOL. 4# These represent a valuable regression test. At the moment, those tests 5# that don't use Holmake can fail without this script being able to notice. 6# The developer has to watch the output and check that everything looks 7# reasonable. 8 9holmake=`pwd`/../bin/Holmake 10 11toplevel () { 12 ../bin/hol < autopilot.sml 13 ../bin/hol < euclid.sml 14 ../bin/hol < fol.sml 15 ../bin/hol < root2.sml 16 ../bin/hol < Thery.sml 17} 18 19simple_example () { 20 pushd $1 21 $holmake cleanAll 22 if $holmake --qof 23 then 24 echo Done Example $1 25 popd 26 else 27 echo "***** Failed in $1" 28 popd 29 exit 1 30 fi 31} 32 33MLsyntax () { simple_example MLsyntax; } 34ind_def () { simple_example ind_def; } 35lambda () { simple_example lambda; } 36arm6 () { simple_example arm6; } 37PSL () { simple_example PSL/1.1; } 38ring () { ../bin/hol < ring.sml; } 39 40bmark () { 41 cd bmark 42 ./run_bmark ../../bin/hol.bare 43 cd .. 44} 45 46parity () { 47 cd parity 48 ../../bin/hol < PARITY.sml 49 cd .. 50} 51 52elliptic () { 53 cd elliptic 54 ../../bin/hol < elliptic.sml 55 cd .. 56} 57 58miller () { 59 cd miller 60 ./m clean 61 ./m 62 cd .. 63} 64 65Crypto () { 66 cd Crypto 67 for i in AES IDEA MARS RC6 TEA TWOFISH 68 do 69 cd $i 70 $holmake cleanAll 71 $holmake 72 cd .. 73 done 74 cd .. 75} 76 77fast () { 78 for i in toplevel MLsyntax ind_def lambda bmark parity elliptic 79 do 80 buildit $i 81 done 82} 83 84buildit () { 85 logfile=/tmp/example-build-log-$1 86 echo "Building $1 - output in $logfile" 87 eval $1 | tee /tmp/example-build-log-$1 88} 89 90check_cwd () { 91 if [ -f Thery.sml -a -f README -a -f fol.sml -a -d miller ] 92 then 93 : 94 else 95 return 1 96 fi 97} 98 99 100if check_cwd 101then 102 : 103else 104 echo "This doesn't look like the examples directory; please cd there and" 105 echo "try again." 106 exit 1 107fi 108 109if [ $# -eq 0 ] 110then 111 echo Building all examples 112 for i in toplevel MLsyntax RSA ind_def lambda bmark parity elliptic \ 113 miller arm6 Crypto PSL 114 do 115 buildit $i 116 done 117else 118 while [ $# -gt 0 ] 119 do 120 arg=`basename $1 .sml` # use of basename strips trailing slashes from 121 # inputs of the form dirname/ and .sml 122 # from ring.sml and others we may wish to use 123 buildit $arg 124 shift 125 done 126fi 127 128 129 130# Local variables: 131# mode: shell-script 132# end: 133