Admin/makedist
author wenzelm
Tue Feb 25 16:57:25 1997 +0100 (1997-02-25)
changeset 2684 9781d63ef063
parent 2668 72a962676702
child 2686 351c45bb338d
permissions -rwxr-xr-x
added proper subset symbols syntax;
     1 #!/bin/bash -norc
     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 LK Modal Provers Pure Sequents TFL Tools ZF"
    11 DOCS="Intro Ref Logics"
    12 
    13 CVSROOT=/isabelle/archive
    14 DISTBASE=~/tmp/isadist
    15 
    16 
    17 ## diagnostics
    18 
    19 PRG=$(basename $0)
    20 
    21 function usage()
    22 {
    23   echo
    24   echo "Usage: $PRG VERSION"
    25   echo
    26   cat <<EOF
    27   Make Isabelle distribution from the master sources at TUM.
    28 
    29   VERSION may be either a tag like "Isabelle94-XX" that specifies the
    30   release to be exported from the repository, or "-" to checkout the
    31   current sources as an unofficial release.
    32 
    33   Checklist for official releases (before running this script):
    34 
    35     * Check that README files are up to date (should have Id: lines).
    36     * Check that Pure/ROOT.ML/version is up to date!
    37     * Make sure that the repository version of Doc is consistent
    38       (watch out for *.bbl, *.rao, *.ind)!
    39 EOF
    40   #Wicked! We just won't tell other users ...
    41   if [ $LOGNAME = paulson -o $LOGNAME = nipkow -o $LOGNAME = wenzelm ]; then
    42     cat <<EOF
    43     * Tag the current repository version, e.g.:
    44         cvs rtag Isabelle94-XX isabelle
    45       PLEASE DON'T DO THIS UNLESS YOU KNOW WHAT YOU'RE DOING!
    46 EOF
    47   fi
    48   cat <<EOF
    49 
    50   After the distribution has been created succesfully, you might want
    51   to run some makeall tests using different ML systems.
    52   
    53 EOF
    54   exit 1
    55 }
    56 
    57 function fail()
    58 {
    59   echo "$1" >&2
    60   exit 2
    61 }
    62 
    63 
    64 ## process command line
    65 
    66 [ $# -ne 1 ] && usage
    67 
    68 VERSION="$1"
    69 shift
    70 
    71 
    72 ## main
    73 
    74 # dist version
    75 
    76 DATE=$(date "+%d-%b-%Y")
    77 
    78 if [ "$VERSION" = "-" ]; then
    79   DISTNAME=Isabelle_$DATE
    80   EXPORT="checkout"
    81   UNOFFICIAL=true
    82 else
    83   DISTNAME="$VERSION"
    84   EXPORT="export -r $VERSION"
    85   UNOFFICIAL=""
    86 fi
    87 
    88 mkdir -p $DISTBASE || fail "Unable to create distribution base dir $DISTBASE!"
    89 [ -e $DISTBASE/$DISTNAME ] && fail "$DISTBASE/$DISTNAME already exists!"
    90 
    91 
    92 # export from repository
    93 
    94 echo
    95 echo "Exporting $DISTNAME from repository. Please be patient ..."
    96 echo
    97 
    98 cd $DISTBASE
    99 
   100 export CVSROOT
   101 cvs -f -q $EXPORT -d $DISTNAME isabelle
   102 
   103 
   104 # make docs
   105 
   106 for D in $DOCS
   107 do
   108   cd $DISTBASE/$DISTNAME/Doc/$D
   109   make dist
   110 done
   111 
   112 
   113 # prepare dist dir for release
   114 
   115 cd $DISTBASE/$DISTNAME
   116 
   117 find . -name CVS -exec rm -rf {} \;
   118 
   119 find Doc -name \*.dvi -exec mv {} Distribution/doc \;
   120 rm -rf Admin Doc examples index.html
   121 
   122 mkdir src
   123 mv $LOGICS src
   124 
   125 mv Distribution/* .
   126 rmdir Distribution
   127 
   128 if [ -n "$UNOFFICIAL" ]; then
   129   {
   130     echo
   131     echo "IMPORTANT NOTE"
   132     echo "=============="
   133     echo
   134     echo "This is an unofficial release of Isabelle, created by $LOGNAME $DATE."
   135     echo
   136   } >UNOFFICIAL
   137 fi
   138 
   139 
   140 # create archive
   141 
   142 cd $DISTBASE
   143 
   144 chown -R $LOGNAME:isabelle $DISTNAME
   145 chmod -R u+w $DISTNAME
   146 chmod -R g-w $DISTNAME
   147 
   148 tar cf - $DISTNAME | gzip >$DISTNAME.tar.gz
   149 
   150 
   151 # final note
   152 
   153 echo
   154 echo "That's it. You'll find the distribution in $DISTBASE."
   155 echo