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