Admin/makedist
author wenzelm
Wed Nov 05 11:41:18 1997 +0100 (1997-11-05)
changeset 4145 ffb0c9670597
parent 3698 0b8986fd9bfc
child 4176 84a0bfbd74e5
permissions -rwxr-xr-x
adapted extend_trfunsT;
     1 #!/bin/bash
     2 #
     3 # $Id$
     4 #
     5 # makedist -- make Isabelle distribution.
     6 
     7 
     8 ## global settings
     9 
    10 LOGICS="CCL CTT Cube FOL FOLP HOL HOLCF LCF Provers Pure Sequents TFL Tools ZF"
    11 
    12 CVSROOT=/isabelle/archive
    13 DISTBASE=~/tmp/isadist
    14 
    15 
    16 ## diagnostics
    17 
    18 PRG=$(basename $0)
    19 
    20 function usage()
    21 {
    22   echo
    23   echo "Usage: $PRG VERSION"
    24   echo
    25   cat <<EOF
    26   Make Isabelle distribution from the master sources at TUM.
    27 
    28   VERSION may be either a tag like "Isabelle94-XX" that specifies the
    29   release to be exported from the repository, or "-" to checkout the
    30   current sources as an unofficial release.
    31 
    32   Checklist for official releases (before running this script):
    33 
    34     * Check that README files are up to date (should have Id: lines).
    35     * Check that Pure/ROOT.ML/version is up to date!
    36     * Check release name and date in NEWS!
    37     * Make sure that encoding info is consistent (fixencoding)!
    38     * Make sure that the repository version of Doc is consistent
    39       (watch out for *.bbl, *.rao, *.ind)!
    40     * Check ML_SYSTEM defaults!
    41 EOF
    42   #Wicked! We just won't tell other users ...
    43   if [ $LOGNAME = paulson -o $LOGNAME = nipkow -o $LOGNAME = wenzelm ]; then
    44     cat <<EOF
    45     * Tag the current repository version, e.g.:
    46         cvs rtag Isabelle94-XX isabelle
    47       PLEASE DON'T DO THIS UNLESS YOU KNOW WHAT YOU'RE DOING!
    48 EOF
    49   fi
    50   cat <<EOF
    51 
    52   After the distribution has been created succesfully, you might want
    53   to run some makeall tests using different ML systems.
    54   
    55 EOF
    56   exit 1
    57 }
    58 
    59 function fail()
    60 {
    61   echo "$1" >&2
    62   exit 2
    63 }
    64 
    65 
    66 ## process command line
    67 
    68 [ $# -ne 1 ] && usage
    69 
    70 VERSION="$1"
    71 shift
    72 
    73 
    74 ## main
    75 
    76 # dist version
    77 
    78 DATE=$(date "+%d-%b-%Y")
    79 
    80 if [ "$VERSION" = "-" ]; then
    81   DISTNAME=Isabelle_$DATE
    82   EXPORT="checkout -P"
    83   UNOFFICIAL=true
    84 else
    85   DISTNAME="$VERSION"
    86   EXPORT="export -r $VERSION"
    87   UNOFFICIAL=""
    88 fi
    89 
    90 mkdir -p $DISTBASE || fail "Unable to create distribution base dir $DISTBASE!"
    91 [ -e $DISTBASE/$DISTNAME ] && fail "$DISTBASE/$DISTNAME already exists!"
    92 
    93 
    94 # export from repository
    95 
    96 echo
    97 echo "Exporting $DISTNAME from repository. Please be patient ..."
    98 echo
    99 
   100 cd $DISTBASE
   101 
   102 export CVSROOT
   103 cvs -f -q $EXPORT -d $DISTNAME isabelle
   104 
   105 
   106 # make docs
   107 
   108 cd $DISTBASE/$DISTNAME/Doc
   109 
   110 for DOC in $(cat Contents)
   111 do
   112   cd $DOC
   113   make dist
   114   cd ..
   115 done
   116 
   117 
   118 # prepare dist dir for release
   119 
   120 cd $DISTBASE/$DISTNAME
   121 
   122 find . -name CVS -exec rm -rf {} \;
   123 
   124 mkdir -p Tools/8bit/bin    #FIXME tmp
   125 find Doc \( -name \*.dvi -o -name \*.eps -o -name \*.ps \) -exec mv {} Distribution/doc \;
   126 rm Distribution/doc/Isa-logics.eps
   127 rm -rf Admin Doc
   128 
   129 mkdir src
   130 mv $LOGICS src
   131 
   132 mv Distribution/* .
   133 rmdir Distribution
   134 
   135 # build theory browser
   136 
   137 cd lib/browser
   138 make
   139 cd ../..
   140 
   141 if [ -n "$UNOFFICIAL" ]; then
   142   {
   143     echo
   144     echo "IMPORTANT NOTE"
   145     echo "=============="
   146     echo
   147     echo "This is an unofficial release of Isabelle, created by $LOGNAME $DATE."
   148     echo
   149   } >UNOFFICIAL
   150 fi
   151 
   152 lynx -dump README.html >README
   153 
   154 
   155 # create archive
   156 
   157 cd $DISTBASE
   158 
   159 #FIXME sometimes doesn't work!?
   160 chown -R $LOGNAME:isabelle $DISTNAME
   161 chmod -R u+w $DISTNAME
   162 chmod -R g+w $DISTNAME
   163 
   164 tar cf - $DISTNAME | gzip >$DISTNAME.tar.gz
   165 
   166 
   167 # final note
   168 
   169 echo
   170 echo "That's it. You'll find the distribution in $DISTBASE."
   171 echo