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