make-all
author nipkow
Tue May 09 22:10:08 1995 +0200 (1995-05-09)
changeset 1114 c8dfb56a7e95
parent 262 024b242bc26f
permissions -rwxr-xr-x
Prod is now a parent of Lfp.
Added thm induct2 to Lfp.
Changed the way patterns in abstractions are pretty printed.
It has become simpler now but fails if split has more than one argument
because then the ast-translation does not match.
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
nipkow@246
    57
    on.on) (cd $ISABELLEBIN; rm -f Pure FOL ZF CCL LCF CTT LK Modal HOL HOLCF 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
nipkow@246
   141
#cannot delete HOL yet... it is needed for HOLCF!
nipkow@246
   142
nipkow@246
   143
echo
nipkow@246
   144
echo
lcp@262
   145
echo '*****LCF in HOL (HOLCF)*****'
nipkow@246
   146
(cd HOLCF;  make $NO $TEST > make$$.log)
nipkow@246
   147
tail HOLCF/make$$.log
nipkow@246
   148
gzip HOLCF/make$$.log
clasohm@0
   149
case $CLEAN.$EXEC in
nipkow@246
   150
    on.on)	rm $ISABELLEBIN/HOL $ISABELLEBIN/HOLCF
clasohm@0
   151
esac
clasohm@0
   152
clasohm@0
   153
echo
clasohm@0
   154
echo
clasohm@0
   155
echo '*****The Lambda-Cube (Cube)*****'
clasohm@0
   156
(cd Cube;  make $NO $TEST > make$$.log)
clasohm@0
   157
case $CLEAN.$EXEC in
clasohm@0
   158
    on.on)	rm $ISABELLEBIN/Cube
clasohm@0
   159
esac
clasohm@0
   160
tail Cube/make$$.log 
clasohm@0
   161
gzip Cube/make$$.log 
clasohm@0
   162
clasohm@0
   163
echo
clasohm@0
   164
echo
clasohm@0
   165
echo '*****First-Order Logic with Proof Terms (FOLP)*****'
clasohm@0
   166
(cd FOLP;  make $NO $TEST > make$$.log)
clasohm@0
   167
case $CLEAN.$EXEC in
clasohm@0
   168
    on.on)	rm $ISABELLEBIN/FOLP
clasohm@0
   169
esac
clasohm@0
   170
tail FOLP/make$$.log 
clasohm@0
   171
gzip FOLP/make$$.log 
clasohm@0
   172
clasohm@0
   173
case $TEST.$EXEC in
clasohm@0
   174
    test.on)	echo
clasohm@0
   175
	        echo '***** Now check the dates on the "test" files *****'
clasohm@0
   176
        	ls -lrt FOL/test ZF/test CCL/test LCF/test CTT/test\
nipkow@246
   177
              	        LK/test Modal/test HOL/test HOLCF/test Cube/test\
nipkow@246
   178
                        FOLP/test
clasohm@0
   179
esac
clasohm@0
   180
echo Finished at `date`