Admin/filesizes
author wenzelm
Wed, 09 Feb 2000 14:03:29 +0100
changeset 8222 55fed562d8ed
parent 8071 49dfba2f2325
child 8852 0a129bdd77d7
permissions -rwxr-xr-x
mirror main page;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
8058
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
     1
#!/bin/bash
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
     2
#
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
     3
# $Id$
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
     4
#
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
     5
# filesizes -- calculate and substitute file sizes in isabelle web pages
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
     6
#
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
     7
# needs:
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
     8
# working directory in dist, rpms + webpages generated and copied to dist
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
     9
# $DISTNAME
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    10
# 
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    11
# substitutes:
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    12
# -norpm:
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    13
# {PACKED_SIZE} {PACKED_SIZE_PDF} {UNPACKED_SIZE}
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    14
# -rpm:
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    15
# {RPM_SML_SIZE} {RPM_BASE_SIZE} {RPM_HOL_SIZE} {RPM_REAL_SIZE}
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    16
# {RPM_ZF_SIZE} {RPM_DOCS_SIZE}
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    17
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    18
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    19
PRG=$(basename $0)
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    20
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    21
function usage()
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    22
{
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    23
  echo
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    24
  echo "Usage: $PRG [-rpm|-norpm]"
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    25
  echo
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    26
  echo "fill in file sizes and distname in isabelle dist web pages"
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    27
  echo
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    28
  echo "  Options are:"
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    29
  echo "    -rpm     only fill in rpm sizes"
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    30
  echo "    -norpm   only fille in other sizes"
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    31
  echo "  (do both by default)" 
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    32
  echo 
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    33
  echo "needs \$DISTNAME environment variable"
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    34
  echo "expects to be startet in isabelle dist dir"
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    35
  echo
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    36
  exit 1
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    37
}
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    38
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    39
function fail()
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    40
{
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    41
  echo "$1" >&2
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    42
  exit 2
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    43
}
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    44
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    45
# check options
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    46
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    47
if [ $# -ge 2 ]; then
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    48
  usage
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    49
fi
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    50
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    51
if [ $# -eq 1 -a "$1" != "-rpm" -a "$1" != "-norpm" ]; then
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    52
  usage
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    53
fi
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    54
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    55
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    56
# begin work
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    57
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    58
if [ $# -eq 0 -o "$1" = "-norpm" ]; then
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    59
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    60
  # check for $DISTNAME
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    61
  if [ "$DISTNAME" = "" ]; then    
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    62
    echo "Error: \$DISTNAME not set"
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    63
    usage
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    64
  fi
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    65
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    66
  PACKED_SIZE=$[ $(wc -c < $DISTNAME.tar.gz) / 1024 ]
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    67
  PACKED_SIZE_PDF=$[ $(wc -c < ${DISTNAME}_pdf.tar.gz) / 1024 ]
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    68
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    69
  UNPACKED_SIZE=$[ $(cat $DISTNAME.tar.gz ${DISTNAME}_pdf.tar.gz | gunzip | wc -c) / 1024 ]
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    70
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    71
  perl -pi -e \
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    72
   "s/{UNPACKED_SIZE}/$UNPACKED_SIZE/g; \ 
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    73
    s/{PACKED_SIZE}/$PACKED_SIZE/g; \
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    74
    s/{PACKED_SIZE_PDF}/$PACKED_SIZE_PDF/g;" \
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    75
      *.html
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    76
fi
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    77
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    78
if [ $# -eq 0 -o "$1" = "-rpm" ]; then
8071
49dfba2f2325 back to old sml version (due to c library problems)
kleing
parents: 8058
diff changeset
    79
  RPM_SML_SIZE=$[ $(wc -c < rpm/smlnj-110.0-3.i386.rpm) / 1024 ]
8058
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    80
  RPM_BASE_SIZE=$[ $(wc -c < rpm/isabelle.rpm) / 1024 ]
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    81
  RPM_HOL_SIZE=$[ $(wc -c < rpm/isabelle-HOL.i386.rpm) / 1024 ]
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    82
  RPM_REAL_SIZE=$[ $(wc -c < rpm/isabelle-HOL-Real.i386.rpm) / 1024 ]
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    83
  RPM_ZF_SIZE=$[ $(wc -c < rpm/isabelle-ZF.i386.rpm) / 1024 ]
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    84
  RPM_DOCS_SIZE=$[ $(wc -c < rpm/isabelle-pdfdocs.rpm) / 1024 ]
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    85
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    86
  perl -pi -e \
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    87
   "s/{RPM_SML_SIZE}/$RPM_SML_SIZE/g; \
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    88
    s/{RPM_BASE_SIZE}/$RPM_BASE_SIZE/g; \
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    89
    s/{RPM_HOL_SIZE}/$RPM_HOL_SIZE/g; \
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    90
    s/{RPM_REAL_SIZE}/$RPM_REAL_SIZE/g; \
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    91
    s/{RPM_ZF_SIZE}/$RPM_ZF_SIZE/g; \
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    92
    s/{RPM_DOCS_SIZE}/$RPM_DOCS_SIZE/g;" \
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    93
      *.html
779e0d2175b7 used for new weg page layout
kleing
parents:
diff changeset
    94
fi