1#! /bin/bash
2
3# * Copyright 2018, Data61
4# *
5# * This software may be distributed and modified according to the terms of
6# * the BSD 2-Clause license. Note that NO WARRANTY is provided.
7# * See "LICENSE_BSD2.txt" for details.
8# *
9# * @TAG(Data61_BSD)
10
11function report_err {
12  echo .. failed!
13  echo Short error output:
14  echo
15  tail -n 20 $1
16  echo
17  echo "  (more error output in $1)"
18  exit 1
19}
20
21
22HOL4_DIR=$(ls -d HOL4 ../HOL4 ../../HOL4 2> /dev/null | head -n 1)
23if [[ -e $HOL4_DIR ]]
24then
25  HOL4_DIR=$(readlink -f $HOL4_DIR)
26  echo "Setting up HOL4 in $HOL4_DIR"
27else
28  echo "No HOL4 found"
29  exit 1
30fi
31
32POLY_DIR=$HOL4_DIR/polyml
33POLY=$POLY_DIR/deploy/bin/poly
34if [[ -e $POLY ]]
35then
36  echo PolyML already built.
37elif [[ -e $POLY_DIR/configure ]]
38then
39  echo Building PolyML in $POLY_DIR
40  echo '  (tracing build progress to poly_output.txt)'
41  OUT=$(readlink -f poly_output.txt)
42  pushd $POLY_DIR
43  echo '  (configuring)'
44  (./configure --prefix=$POLY_DIR/deploy) &> $OUT
45  echo '  (building)'
46  (make && make install) &>> $OUT
47  if [[ -e $POLY ]]
48  then
49    echo Built PolyML
50  else
51    report_err poly_output.txt
52    exit 1
53  fi
54  popd
55elif [[ -e $POLY_DIR ]]
56then
57  echo Missing PolyML source in $POLY_DIR
58  exit 1
59else
60  echo No PolyML dir $POLY_DIR
61  exit 1
62fi
63
64# this script cleans any previous build of HOL4
65# this is needed when pulling in new revisions to the base system
66OUT=$(readlink -f hol4_output.txt)
67echo output is $OUT
68pushd $HOL4_DIR
69
70echo Cleaning HOL4 build in $HOL4_DIR
71git clean -fdX -e polyml &> /dev/null
72
73echo Building HOL4 now.
74echo '  (tracing build progress to hol4_output.txt)'
75echo '  (configuring)'
76$POLY < tools-poly/smart-configure.sml &> $OUT
77
78if [[ ! -e $HOL4_DIR/bin/build ]]
79then
80  report_err hol4_output.txt
81  exit 1
82fi
83
84echo '  (building)'
85PATH=$HOL4_DIR/bin:$PATH build &>> $OUT
86
87if ( tail $OUT | grep 'built successfully' )
88then
89  echo 'Built HOL4.'
90else
91  report_err hol4_output.txt
92  exit 1
93fi
94popd
95
96