1 #!/usr/bin/env bash |
1 #!/usr/bin/env bash |
2 # |
2 # |
3 # Author: Gerwin Klein, TU Muenchen |
3 # Author: Gerwin Klein, TU Muenchen |
4 # |
4 # |
5 # DESCRIPTION: Run isabelle makeall from specified distribution and settings. |
5 # DESCRIPTION: Run isabelle build from specified distribution and settings. |
6 |
6 |
7 ## global settings |
7 ## global settings |
8 . ~/admin/isatest/isatest-settings |
8 . ~/admin/isatest/isatest-settings |
9 |
9 |
10 # max time until test is aborted (in sec) |
10 # max time until test is aborted (in sec) |
16 PRG="$(basename "$0")" |
16 PRG="$(basename "$0")" |
17 |
17 |
18 function usage() |
18 function usage() |
19 { |
19 { |
20 echo |
20 echo |
21 echo "Usage: $PRG [-l logic targets] settings1 [settings2 ...]" |
21 echo "Usage: $PRG [-l targets] settings1 [settings2 ...]" |
22 echo |
22 echo |
23 echo " Runs isabelle makeall for specified settings." |
23 echo " Runs isabelle build for specified settings." |
24 echo " Leaves messages in ${ERRORLOG} and ${LOGPREFIX} if it fails." |
24 echo " Leaves messages in ${ERRORLOG} and ${LOGPREFIX} if it fails." |
25 echo |
25 echo |
26 echo "Examples:" |
26 echo "Examples:" |
27 echo " $PRG ~/settings/at-poly ~/settings/at-sml" |
27 echo " $PRG ~/settings/at-poly ~/settings/at-sml" |
28 echo " $PRG -l HOL \"HOL-Library HOL-Bali\" ~/settings/at-poly" |
28 echo " $PRG -l \"HOL-Library HOL-Bali\" ~/settings/at-poly" |
29 exit 1 |
29 exit 1 |
30 } |
30 } |
31 |
31 |
32 function fail() |
32 function fail() |
33 { |
33 { |
44 [ "$1" = "-?" ] && usage |
44 [ "$1" = "-?" ] && usage |
45 [ "$#" -lt "1" ] && usage |
45 [ "$#" -lt "1" ] && usage |
46 |
46 |
47 [ -d $DISTPREFIX ] || fail "$DISTPREFIX is not a directory." |
47 [ -d $DISTPREFIX ] || fail "$DISTPREFIX is not a directory." |
48 |
48 |
49 TARGETS=all |
49 # build args and nice setup for different target platforms |
50 |
50 BUILD_ARGS="-v" |
51 # make file flags and nice setup for different target platforms |
|
52 MFLAGS="-k" |
|
53 NICE="nice" |
51 NICE="nice" |
54 case $HOSTNAME in |
52 case $HOSTNAME in |
55 macbroy2 | macbroy6 | macbroy30) |
53 macbroy2 | macbroy6 | macbroy30) |
56 NICE="" |
54 NICE="" |
57 ;; |
55 ;; |
58 lxbroy[234]) |
56 lxbroy[234]) |
59 MFLAGS="-k -j 2" |
57 BUILD_ARGS="$BUILD_ARGS -j 2" |
60 NICE="" |
58 NICE="" |
61 ;; |
59 ;; |
62 |
60 |
63 esac |
61 esac |
64 |
62 |
65 ISABELLE_TOOL="$DISTPREFIX/Isabelle/bin/isabelle" |
63 ISABELLE_TOOL="$DISTPREFIX/Isabelle/bin/isabelle" |
|
64 [ -x $ISABELLE_TOOL ] || fail "Cannot run $ISABELLE_TOOL" |
66 |
65 |
67 [ -x $ISABELLE_TOOL ] || fail "Cannot run $ISABELLE_TOOL" |
66 ISABELLE_HOME="$($ISABELLE_TOOL getenv -b ISABELLE_HOME)" |
68 |
67 |
69 if [ "$1" = "-l" ]; then |
68 if [ "$1" = "-l" ]; then |
70 shift |
69 shift |
71 [ "$#" -lt "3" ] && usage |
70 [ "$#" -lt 2 ] && usage |
72 LOGIC="$1" |
71 BUILD_ARGS="$BUILD_ARGS $1" |
73 TARGETS="$2" |
72 shift |
74 shift 2 |
|
75 ISABELLE_HOME="$($ISABELLE_TOOL getenv -b ISABELLE_HOME)" |
|
76 if [ "$LOGIC" = "." ]; then |
|
77 DIR="." |
|
78 TOOL="$ISABELLE_TOOL makeall $MFLAGS $TARGETS" |
|
79 else |
|
80 DIR="$ISABELLE_HOME/src/$LOGIC" |
|
81 TOOL="$ISABELLE_TOOL make $MFLAGS $TARGETS" |
|
82 fi |
|
83 else |
73 else |
84 DIR="." |
74 BUILD_ARGS="$BUILD_ARGS -a" |
85 TOOL="$ISABELLE_TOOL makeall $MFLAGS $TARGETS" |
|
86 fi |
75 fi |
87 |
76 |
88 IDENT=$(cat "$DISTPREFIX/ISABELLE_IDENT") |
77 IDENT=$(cat "$DISTPREFIX/ISABELLE_IDENT") |
89 |
78 |
90 |
79 |
122 rm -rf $ISABELLE_HOME_USER |
111 rm -rf $ISABELLE_HOME_USER |
123 fi |
112 fi |
124 |
113 |
125 cp $DISTPREFIX/Isabelle/etc/settings.orig $DISTPREFIX/Isabelle/etc/settings |
114 cp $DISTPREFIX/Isabelle/etc/settings.orig $DISTPREFIX/Isabelle/etc/settings |
126 cat $SETTINGS >> $DISTPREFIX/Isabelle/etc/settings |
115 cat $SETTINGS >> $DISTPREFIX/Isabelle/etc/settings |
127 (ulimit -t $MAXTIME; cd $DIR; $NICE $TOOL >> $TESTLOG 2>&1) |
116 (ulimit -t $MAXTIME; $NICE "$ISABELLE_TOOL" build $BUILD_ARGS >> $TESTLOG 2>&1) |
128 |
117 |
129 if [ $? -eq 0 ] |
118 if [ $? -eq 0 ] |
130 then |
119 then |
131 # test log and cleanup |
120 # test log and cleanup |
132 echo ------------------- test successful --- `date` --- $HOSTNAME >> $TESTLOG 2>&1 |
121 echo ------------------- test successful --- `date` --- $HOSTNAME >> $TESTLOG 2>&1 |