1#! /bin/bash
2
3# * Copyright 2016, NICTA
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(NICTA_BSD)
10
11# setup Isabelle
12ISABELLE=../../isabelle/bin/isabelle
13if [[ -e ~/.isabelle/etc/settings ]]
14then
15  ISA_PLAT=$($ISABELLE env bash -c 'echo $ML_PLATFORM')
16  if echo $ISA_PLAT | grep -q 64
17  then
18    echo Isabelle platform is $ISA_PLAT
19  else
20    echo Isabelle platform $ISA_PLAT not 64-bit
21    echo Will not be able to build seL4 C models.
22    echo Reconfigure in ~/.isabelle/etc/settings
23    exit 1
24  fi
25else
26  echo No Isabelle settings, setting defaults.
27  mkdir -p ~/.isabelle/etc/
28  cp ../../l4v/misc/etc/settings ~/.isabelle/etc/
29fi
30$ISABELLE components -a
31
32HOL4_DIR=$(readlink -f ../../HOL4)
33POLY_DIR=$HOL4_DIR/polyml
34
35function mk_build_summ {
36  SUMM=$(readlink -f $HOL4_DIR/bin/$1)
37  pushd $HOL4_DIR
38  echo Results of '"git show"' in $HOL4_DIR before building. > $SUMM
39  git show >> $SUMM
40  popd
41  echo Results of '"find $POLY_DIR/deploy -type f | xargs md5sum"' before building. >> $SUMM
42  find $POLY_DIR/deploy -type f | xargs md5sum >> $SUMM
43}
44
45# check if HOL4 is built, and if it is up to date
46if [[ ! -e $HOL4_DIR/bin/build ]]
47then
48  echo 'HOL4 not built.'
49  REBUILD='true'
50elif [[ ! -e $HOL4_DIR/sigobj/realTheory.sig ]]
51then
52  echo 'HOL4 theories not built'
53  REBUILD='true'
54elif [[ -e $HOL4_DIR/bin/build_summ ]]
55then
56  mk_build_summ build_summ2
57  if ( diff -q $HOL4_DIR/bin/build_summ $HOL4_DIR/bin/build_summ2 )
58  then
59    # curiously this is the equal case of diff
60    echo HOL4 matches last build status.
61    REBUILD='false'
62  else
63    echo HOL4 configuration changed from previous build.
64    REBUILD='true'
65  fi
66fi
67
68if [[ $REBUILD == 'true' ]]
69then
70  bash ../scripts/setup-HOL4.sh
71fi
72
73# setup graph-refine to use CVC4 from Isabelle
74SVFL=../../.solverlist
75if python ../solver.py testq | grep -q 'Solver self-test succ'
76then
77  echo Solvers already configured.
78else if [[ -e $SVFL ]]
79then
80  echo Solvers configured but self-test failed.
81  echo Try python ../solver.py test
82  echo   and adjust $SVFL to succeed.
83  exit 1
84else
85  ISA_CVC4=$($ISABELLE env bash -c 'echo $CVC4_SOLVER')
86  echo '# minimum autogenerated .solverlist' > $SVFL
87  echo CVC4: online: $ISA_CVC4 --incremental --lang smt --tlimit=5000 >> $SVFL
88  echo CVC4: offline: $ISA_CVC4 --lang smt >> $SVFL
89  echo Configured graph-refine to use CVC4 SMT solver.
90  if python ../solver.py testq | grep -q 'Solver self-test succ'
91  then
92    echo Self test passed.
93  else
94    echo Self test failed!
95    echo Try python ../solver.py test
96    echo   and adjust $SVFL to succeed.
97    exit 1
98  fi
99fi fi
100
101if which mlton
102then
103  echo MLton available.
104else
105  echo MLton not available or not found. 
106  echo e.g. 'which mlton' should succeed.
107  exit 1
108fi
109
110
111