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