make-all
author lcp
Mon Dec 13 18:50:03 1993 +0100 (1993-12-13)
changeset 196 7646f5b4653c
parent 9 c1795fac88c3
child 246 e5d184710a0b
permissions -rwxr-xr-x
added isabelle-users paragraph
clasohm@0
     1
#! /bin/sh
clasohm@0
     2
#
clasohm@0
     3
#make-all: make all systems afresh
clasohm@0
     4
clasohm@0
     5
# Creates gzipped log files called makeNNNN.log.gz on each subdirectory and
clasohm@0
     6
# displays the last few lines of these files -- this indicates whether
clasohm@0
     7
# the "make" failed (whether it terminated due to an error)
clasohm@0
     8
clasohm@0
     9
# switches are
clasohm@0
    10
#     -noforce	don't delete old databases/images first
clasohm@0
    11
#     -clean	delete databases/images after use (leaving Pure)
clasohm@0
    12
#     -notest	make databases/images w/o running the examples
clasohm@0
    13
#     -noexec	don't execute, just check settings and Makefiles
clasohm@0
    14
clasohm@0
    15
#Environment variables required:
clasohm@0
    16
# ISABELLEBIN: the directory to hold Poly/ML databases or New Jersey ML images
clasohm@0
    17
# ISABELLECOMP: the ML compiler
clasohm@0
    18
clasohm@0
    19
# A typical shell script for /bin/sh is...
clasohm@0
    20
# ML_DBASE=/usr/groups/theory/poly2.04/`arch`/ML_dbase
clasohm@0
    21
# ISABELLEBIN=/homes/`whoami`/bin
clasohm@0
    22
# ISABELLECOMP="poly -noDisplay"
clasohm@0
    23
# export ML_DBASE ISABELLEBIN ISABELLECOMP 
clasohm@0
    24
# nohup make-all $*
clasohm@0
    25
clasohm@0
    26
set -e			#fail immediately upon errors
clasohm@0
    27
clasohm@0
    28
# process command line switches
clasohm@0
    29
CLEAN="off";
clasohm@0
    30
FORCE="on";
clasohm@0
    31
TEST="test";
clasohm@0
    32
EXEC="on";
clasohm@0
    33
NO="";
clasohm@0
    34
for A in $*
clasohm@0
    35
do
clasohm@0
    36
	case $A in
clasohm@0
    37
	-clean) CLEAN="on" ;;
clasohm@0
    38
	-noforce) FORCE="off" ;;
clasohm@0
    39
	-notest) TEST="" ;;
clasohm@0
    40
	-noexec) EXEC="off"
clasohm@0
    41
                 NO="-n" ;;
clasohm@0
    42
	*)	echo "Bad flag for make-all: $A"
clasohm@0
    43
		echo "Usage: make-all [-noforce] [-clean] [-notest] [-noexec]"
clasohm@0
    44
		exit ;;
clasohm@0
    45
	esac
clasohm@0
    46
done
clasohm@0
    47
clasohm@0
    48
echo Started at `date`
clasohm@0
    49
echo Source=`pwd`
clasohm@0
    50
echo Destination=${ISABELLEBIN?'No destination directory specified'}
clasohm@0
    51
echo force=$FORCE '    ' clean=$CLEAN '    '
clasohm@0
    52
echo Compiler=${ISABELLECOMP?'No compiler specified'} 
clasohm@0
    53
echo Running on `hostname`
clasohm@0
    54
echo Log files will be called make$$.log.gz
clasohm@0
    55
clasohm@0
    56
case $FORCE.$EXEC in
clasohm@0
    57
    on.on) (cd $ISABELLEBIN; rm -f Pure FOL ZF CCL LCF CTT LK Modal HOL Cube FOLP)
clasohm@0
    58
esac
clasohm@0
    59
lcp@9
    60
set +e			#no longer fail upon errors -- e.g. if a "make" fails
lcp@9
    61
clasohm@0
    62
echo
clasohm@0
    63
echo
clasohm@0
    64
echo '*****Pure Isabelle*****'
clasohm@0
    65
(cd Pure; make $NO > make$$.log)
clasohm@0
    66
tail Pure/make$$.log
clasohm@0
    67
gzip Pure/make$$.log
clasohm@0
    68
clasohm@0
    69
echo
clasohm@0
    70
echo
clasohm@0
    71
echo '*****First-Order Logic (FOL)*****'
clasohm@0
    72
(cd FOL;  make $NO $TEST > make$$.log)
clasohm@0
    73
tail FOL/make$$.log
clasohm@0
    74
gzip FOL/make$$.log
clasohm@0
    75
#cannot delete FOL yet... it is needed for ZF, CCL and LCF!
clasohm@0
    76
clasohm@0
    77
echo
clasohm@0
    78
echo
clasohm@0
    79
echo '*****Set theory (ZF)*****'
clasohm@0
    80
(cd ZF;  make $NO $TEST > make$$.log)
clasohm@0
    81
tail ZF/make$$.log
clasohm@0
    82
gzip ZF/make$$.log
clasohm@0
    83
case $CLEAN.$EXEC in
clasohm@0
    84
    on.on)	rm $ISABELLEBIN/ZF
clasohm@0
    85
esac
clasohm@0
    86
clasohm@0
    87
echo
clasohm@0
    88
echo
clasohm@0
    89
echo '*****Classical Computational Logic (CCL)*****'
clasohm@0
    90
(cd CCL;  make $NO $TEST > make$$.log)
clasohm@0
    91
tail CCL/make$$.log
clasohm@0
    92
gzip CCL/make$$.log
clasohm@0
    93
case $CLEAN.$EXEC in
clasohm@0
    94
    on.on)	rm $ISABELLEBIN/CCL
clasohm@0
    95
esac
clasohm@0
    96
clasohm@0
    97
echo
clasohm@0
    98
echo
clasohm@0
    99
echo '*****Domain Theory (LCF)*****'
clasohm@0
   100
(cd LCF;  make $NO $TEST > make$$.log)
clasohm@0
   101
tail LCF/make$$.log
clasohm@0
   102
gzip LCF/make$$.log
clasohm@0
   103
case $CLEAN.$EXEC in
clasohm@0
   104
    on.on)	rm $ISABELLEBIN/FOL $ISABELLEBIN/LCF
clasohm@0
   105
esac
clasohm@0
   106
clasohm@0
   107
echo
clasohm@0
   108
echo
clasohm@0
   109
echo '*****Constructive Type Theory (CTT)*****'
clasohm@0
   110
(cd CTT;  make $NO $TEST > make$$.log)
clasohm@0
   111
tail CTT/make$$.log
clasohm@0
   112
gzip CTT/make$$.log
clasohm@0
   113
case $CLEAN.$EXEC in
clasohm@0
   114
    on.on)	rm $ISABELLEBIN/CTT
clasohm@0
   115
esac
clasohm@0
   116
clasohm@0
   117
echo
clasohm@0
   118
echo
clasohm@0
   119
echo '*****Classical Sequent Calculus (LK)*****'
clasohm@0
   120
(cd LK;  make $NO $TEST > make$$.log)
clasohm@0
   121
tail LK/make$$.log
clasohm@0
   122
gzip LK/make$$.log
clasohm@0
   123
#cannot delete LK yet... it is needed for Modal!
clasohm@0
   124
clasohm@0
   125
echo
clasohm@0
   126
echo
clasohm@0
   127
echo '*****Modal logic (Modal)*****'
clasohm@0
   128
(cd Modal;  make $NO $TEST > make$$.log)
clasohm@0
   129
tail Modal/make$$.log
clasohm@0
   130
gzip Modal/make$$.log
clasohm@0
   131
case $CLEAN.$EXEC in
clasohm@0
   132
    on.on)	rm $ISABELLEBIN/LK $ISABELLEBIN/Modal
clasohm@0
   133
esac
clasohm@0
   134
clasohm@0
   135
echo
clasohm@0
   136
echo
clasohm@0
   137
echo '*****Higher-Order Logic (HOL)*****'
clasohm@0
   138
(cd HOL;  make $NO $TEST > make$$.log)
clasohm@0
   139
tail HOL/make$$.log
clasohm@0
   140
gzip HOL/make$$.log
clasohm@0
   141
case $CLEAN.$EXEC in
clasohm@0
   142
    on.on)	rm $ISABELLEBIN/HOL
clasohm@0
   143
esac
clasohm@0
   144
clasohm@0
   145
echo
clasohm@0
   146
echo
clasohm@0
   147
echo '*****The Lambda-Cube (Cube)*****'
clasohm@0
   148
(cd Cube;  make $NO $TEST > make$$.log)
clasohm@0
   149
case $CLEAN.$EXEC in
clasohm@0
   150
    on.on)	rm $ISABELLEBIN/Cube
clasohm@0
   151
esac
clasohm@0
   152
tail Cube/make$$.log 
clasohm@0
   153
gzip Cube/make$$.log 
clasohm@0
   154
clasohm@0
   155
echo
clasohm@0
   156
echo
clasohm@0
   157
echo '*****First-Order Logic with Proof Terms (FOLP)*****'
clasohm@0
   158
(cd FOLP;  make $NO $TEST > make$$.log)
clasohm@0
   159
case $CLEAN.$EXEC in
clasohm@0
   160
    on.on)	rm $ISABELLEBIN/FOLP
clasohm@0
   161
esac
clasohm@0
   162
tail FOLP/make$$.log 
clasohm@0
   163
gzip FOLP/make$$.log 
clasohm@0
   164
clasohm@0
   165
case $TEST.$EXEC in
clasohm@0
   166
    test.on)	echo
clasohm@0
   167
	        echo '***** Now check the dates on the "test" files *****'
clasohm@0
   168
        	ls -lrt FOL/test ZF/test CCL/test LCF/test CTT/test\
clasohm@0
   169
              	        LK/test Modal/test HOL/test Cube/test FOLP/test
clasohm@0
   170
esac
clasohm@0
   171
echo Finished at `date`