lib/Tools/makeall
author wenzelm
Fri, 07 Mar 1997 11:48:46 +0100
changeset 2754 59bd96046ad6
parent 2592 a17f46352df3
child 2811 27dd00d74e5a
permissions -rwxr-xr-x
moved settings comment to build;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2502
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
     1
#!/bin/bash -norc
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
     2
#
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
     3
# $Id$
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
     4
#
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
     5
# DESCRIPTION: make all Isabelle systems afresh
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
     6
#
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
     7
# FIXME TODO:
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
     8
#  - clean
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
     9
#  - usage
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    10
#  - getopts (i.e. *short* options) (?)
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    11
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    12
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    13
# Creates gzipped log files called makeNNNN.log.gz on each subdirectory and
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    14
# displays the last few lines of these files -- this indicates whether
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    15
# the make failed (whether it terminated due to an error)
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    16
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    17
# switches are
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    18
#     -noforce	don't delete old databases/images first
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    19
#     -clean	delete databases/images after use (leaving Pure)
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    20
#     -notest	make databases/images w/o running the examples
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    21
#     -noexec	don't execute, just check settings and IsaMakefiles
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    22
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    23
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    24
set -e			#fail immediately upon errors
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    25
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    26
# process command line switches
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    27
CLEAN="off";
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    28
FORCE="on";
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    29
TEST="test";
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    30
EXEC="on";
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    31
NO="";
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    32
for A in $*
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    33
do
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    34
	case $A in
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    35
	-clean) CLEAN="on" ;;
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    36
	-noforce) FORCE="off" ;;
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    37
	-notest) TEST="" ;;
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    38
	-noexec) EXEC="off"
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    39
                 NO="-n" ;;
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    40
	*)	echo "Bad flag for makeall: $A"
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    41
		echo "Usage: makeall [-noforce] [-clean] [-notest] [-noexec]"
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    42
		exit ;;
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    43
	esac
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    44
done
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    45
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    46
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    47
echo Started at `date`
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    48
echo Source=`pwd`
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    49
echo Destination=$ISABELLE_OUTPUT_DIR
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    50
echo force=$FORCE '    ' clean=$CLEAN '    '
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    51
echo Compiler=$ML_SYSTEM
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    52
echo Running on `hostname`
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    53
echo Log files will be called make$$.log.gz
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    54
case $TEST in
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    55
  test) echo; echo '		**** Full test: WILL TAKE MANY HOURS ****'
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    56
        echo '		**** Consider the -notest switch ****'
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    57
esac
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    58
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    59
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    60
case $FORCE.$EXEC in
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    61
  on.on) (cd $ISABELLE_OUTPUT_DIR;
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    62
          for f in Pure FOL ZF CCL LCF CTT Sequents HOL HOLCF Cube FOLP
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    63
	  do 
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    64
	   rm -f $f
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    65
	  done)
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    66
esac
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    67
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    68
set +e			#no longer fail upon errors -- e.g. if a make fails
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    69
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    70
echo
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    71
echo
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    72
echo '*****Pure Isabelle*****'
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    73
( cd Pure; $ISATOOL make $NO > make$$.log )
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    74
tail Pure/make$$.log
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    75
gzip Pure/make$$.log
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    76
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    77
echo
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    78
echo
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    79
echo '*****First-Order Logic (FOL)*****'
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    80
(cd FOL; $ISATOOL make $NO $TEST > make$$.log)
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    81
tail FOL/make$$.log
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    82
gzip FOL/make$$.log
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    83
#cannot delete FOL yet... it is needed for ZF, CCL and LCF!
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    84
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    85
echo
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    86
echo
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    87
echo '*****Set theory (ZF)*****'
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    88
(cd ZF; $ISATOOL make $NO $TEST > make$$.log)
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    89
tail ZF/make$$.log
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    90
gzip ZF/make$$.log
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    91
case $CLEAN.$EXEC in
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    92
    on.on)	rm -f $ISABELLE_OUTPUT_DIR/ZF
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    93
esac
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    94
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    95
echo
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    96
echo
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    97
echo '*****Classical Computational Logic (CCL)*****'
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    98
(cd CCL; $ISATOOL make $NO $TEST > make$$.log)
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
    99
tail CCL/make$$.log
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   100
gzip CCL/make$$.log
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   101
case $CLEAN.$EXEC in
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   102
    on.on)	rm -f $ISABELLE_OUTPUT_DIR/CCL
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   103
esac
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   104
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   105
echo
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   106
echo
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   107
echo '*****Domain Theory (LCF)*****'
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   108
(cd LCF; $ISATOOL make $NO $TEST > make$$.log)
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   109
tail LCF/make$$.log
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   110
gzip LCF/make$$.log
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   111
case $CLEAN.$EXEC in
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   112
  on.on)	rm -f $ISABELLE_OUTPUT_DIR/FOL $ISABELLE_OUTPUT_DIR/LCF
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   113
esac
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   114
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   115
echo
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   116
echo
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   117
echo '*****Constructive Type Theory (CTT)*****'
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   118
(cd CTT; $ISATOOL make $NO $TEST > make$$.log)
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   119
tail CTT/make$$.log
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   120
gzip CTT/make$$.log
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   121
case $CLEAN.$EXEC in
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   122
    on.on)	rm -f $ISABELLE_OUTPUT_DIR/CTT
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   123
esac
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   124
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   125
echo
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   126
echo
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   127
echo '*****Sequent Calculi (Sequents)*****'
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   128
(cd Sequents; $ISATOOL make $NO $TEST > make$$.log)
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   129
tail Sequents/make$$.log
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   130
gzip Sequents/make$$.log
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   131
case $CLEAN.$EXEC in
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   132
    on.on)	rm -f $ISABELLE_OUTPUT_DIR/Sequents
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   133
esac
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   134
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   135
echo
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   136
echo
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   137
echo '*****Higher-Order Logic (HOL)*****'
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   138
(cd HOL; $ISATOOL make $NO $TEST > make$$.log)
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   139
tail HOL/make$$.log
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   140
gzip HOL/make$$.log
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   141
#cannot delete HOL yet... it is needed for HOLCF!
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   142
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   143
echo
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   144
echo
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   145
echo '*****LCF in HOL (HOLCF)*****'
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   146
(cd HOLCF; $ISATOOL make $NO $TEST > make$$.log)
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   147
tail HOLCF/make$$.log
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   148
gzip HOLCF/make$$.log
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   149
case $CLEAN.$EXEC in
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   150
  on.on)	rm -f $ISABELLE_OUTPUT_DIR/HOL $ISABELLE_OUTPUT_DIR/HOLCF
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   151
esac
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   152
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   153
echo
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   154
echo
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   155
echo '*****The Lambda-Cube (Cube)*****'
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   156
(cd Cube; $ISATOOL make $NO $TEST > make$$.log)
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   157
case $CLEAN.$EXEC in
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   158
    on.on)	rm -f $ISABELLE_OUTPUT_DIR/Cube
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   159
esac
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   160
tail Cube/make$$.log 
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   161
gzip Cube/make$$.log 
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   162
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   163
echo
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   164
echo
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   165
echo '*****First-Order Logic with Proof Terms (FOLP)*****'
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   166
(cd FOLP; $ISATOOL make $NO $TEST > make$$.log)
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   167
case $CLEAN.$EXEC in
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   168
    on.on)	rm -f $ISABELLE_OUTPUT_DIR/FOLP
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   169
esac
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   170
tail FOLP/make$$.log 
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   171
gzip FOLP/make$$.log 
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   172
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   173
case $TEST.$EXEC in
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   174
    test.on)	echo
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   175
	        echo '***** Now check the dates on the "test" files *****'
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   176
        	ls -lrt FOL/test ZF/test CCL/test LCF/test CTT/test\
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   177
              	        Sequents/test HOL/test HOLCF/test\
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   178
                        Cube/test FOLP/test
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   179
esac
dcf928805273 make all Isabelle systems afresh;
wenzelm
parents:
diff changeset
   180
echo Finished at `date`