tuned;
authorwenzelm
Mon, 11 Sep 2000 20:23:24 +0200
changeset 9925 40f02ebcb3c0
parent 9924 3370f6aa3200
child 9926 bc2c0a26bd04
tuned;
Admin/README-rpm.html
Admin/makedist
Admin/makepage
Admin/makerpm
Admin/page/common/functions.pl
Admin/page/dist-content/binary.content
--- a/Admin/README-rpm.html	Mon Sep 11 18:00:47 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,29 +0,0 @@
-<html>
-
-<head>
-<!-- $Id$ -->
-<title>Isabelle Binary Distribution</title>
-</head>
-
-<body>
-
-<h1>Isabelle Binary Distribution</h1>
-
-This is your fast path to Isabelle on Linux/x86 systems (with rpm
-package management):
-
-<p>
-
-<pre>
-rpm -i <a
-href="ftp://ftp.cl.cam.ac.uk/MIRRORED/smlnj/release/110/smlnj-110.0-3.i386.rpm">smlnj-110.0-3.i386.rpm</a>                           # mandatory
-rpm -i --prefix /usr/share <a href="isabelle.rpm">isabelle.rpm</a>                 # mandatory
-rpm -i --prefix /usr/share <a href="isabelle-HOL.i386.rpm">isabelle-HOL.i386.rpm</a>        # recommended
-rpm -i --prefix /usr/share <a href="isabelle-HOL-Real.i386.rpm">isabelle-HOL-Real.i386.rpm</a>   # optional
-rpm -i --prefix /usr/share <a href="isabelle-ZF.i386.rpm">isabelle-ZF.i386.rpm</a>         # optional
-rpm -i --prefix /usr/share <a href="isabelle-pdfdocs.rpm">isabelle-pdfdocs.rpm</a>         # optional
-</pre>
-
-</body>
-
-</html>
--- a/Admin/makedist	Mon Sep 11 18:00:47 2000 +0200
+++ b/Admin/makedist	Mon Sep 11 20:23:24 2000 +0200
@@ -85,15 +85,15 @@
 DISTDATE=$(date "+%B %Y")
 
 if [ "$VERSION" = "--" ]; then
-  DISTNAME="Isabelle_${DATE}_test"
+  DISTNAME="Isabelle_$DATE"
   DISTVERSION="$DISTNAME"
   EXPORT="$THIS/cvs-copy $THIS/.. $DISTNAME"
-  UNOFFICIAL=""
+  UNOFFICIAL="unofficial test"
 elif [ "$VERSION" = "-" ]; then
   DISTNAME="Isabelle_$DATE"
   DISTVERSION="$DISTNAME"
   EXPORT="cvs -f -q checkout -P -d $DISTNAME isabelle"
-  UNOFFICIAL=true
+  UNOFFICIAL="unofficial"
 else
   DISTNAME="$VERSION"
   DISTVERSION="$DISTNAME: $DISTDATE"
@@ -134,8 +134,8 @@
 for DOC in $(cat Contents)
 do
   cd "$DOC"
-  #FIXME make dvi
-  #FIXME [ -n "$PDFLATEX" ] && make clean pdf
+  make dvi
+  [ -n "$PDFLATEX" ] && make clean pdf
   cd ..
 done
 
@@ -148,8 +148,8 @@
 
 cd "$DISTBASE/$DISTNAME"
 
-cp -R Admin/page ../page
-cp Distribution/Doc/Contents ../page/Contents
+cp -R Admin/page ..
+cp Distribution/doc/Contents ../page
 cp Distribution/lib/logo/isabelle.gif ../page/main-content
 cp Distribution/lib/logo/isabelle.gif ../page/dist-content
 echo "$DISTNAME" > ../page/DISTNAME
@@ -176,9 +176,9 @@
     echo "IMPORTANT NOTE"
     echo "=============="
     echo
-    echo "This is an unofficial release of Isabelle, created by $LOGNAME $DATE."
+    echo "This is an $UNOFFICIAL release of Isabelle, created by $LOGNAME $DATE."
     echo
-  } >UNOFFICIAL
+  } >ANNOUNCE
 fi
 
 perl -pi -e "s/{ISABELLE}/$DISTNAME/g;" lib/html/index.html
@@ -223,7 +223,7 @@
 
 mv "${DISTNAME}-old/README.html" "${DISTNAME}-old/INSTALL" "$DISTNAME"
 mkdir "$DISTNAME/doc"
-mv "${DISTNAME}-old/doc/"*.pdf "${DISTNAME}-old/doc/Contents" "$DISTNAME/doc"
+mv "${DISTNAME}-old/doc/"*.pdf "$DISTNAME/doc"
 
 chgrp -R isabelle "$DISTNAME"
 
--- a/Admin/makepage	Mon Sep 11 18:00:47 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,67 +0,0 @@
-#!/bin/bash
-#
-# $Id$
-#
-# makemainpage -- make main Isabelle web pages
-
-TARGET=/usr/proj/isabelle-repository/www
-FILES="index.html docs.html logics.html cambridge.gif munich.gif"
-PREFIX=main
-
-PRG=$(basename $0)
-THIS=$(cd $(dirname "$0"); echo $PWD)
-
-function usage()
-{
-  echo
-  echo "Usage: $PRG VERSION DIST"
-  echo
-  cat <<EOF
-  Make Isabelle main web pages with links to documentation for VERSION
-
-  VERSION should be the Isabelle version contained in DIST
-  DIST should be an Isabelle distribution archive or directory
-
-EOF
-  exit 1
-}
-
-function fail()
-{
-  echo "$1" >&2
-  exit 2
-}
-
-
-## process command line
-
-[ $# -ne 2 ] && usage
-
-export DISTNAME=$1
-shift
-DIST=$1
-
-cd $THIS/page
-
-if [ -d $DIST ]; then
-    cp $DIST/doc/Contents .
-else
-  if [ -f $DIST ]; then
-      gzip -dc $DIST | tar -Bxf - $DISTNAME/doc/Contents 
-      mv $DISTNAME/doc/Contents .
-      rmdir -p $DISTNAME/doc
-  else 
-      echo error: $DIST not found
-      fail
-  fi
-fi
-
-make main
-
-for FILE in $FILES; do
-    cp -f $PREFIX/$FILE $TARGET
-done
-
-chmod g=u $TARGET/*
-
-( cd $TARGET; echo -e "\nYou should find the Isabelle pages in $PWD"; )
--- a/Admin/makerpm	Mon Sep 11 18:00:47 2000 +0200
+++ b/Admin/makerpm	Mon Sep 11 20:23:24 2000 +0200
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/bin/bash -x
 #
 # $Id$
 #
@@ -12,12 +12,12 @@
 DISTBASE=~/tmp/isadist
 ROOT=/usr/share
 BIN=/usr/bin
-RPMRELEASE=2
+RPMRELEASE=1
 
 
 ## diagnostics
 
-PRG=$(basename $0)
+PRG=$(basename "$0")
 
 function usage()
 {
@@ -38,7 +38,7 @@
 
 ## process command line
 
-[ $# -gt 1 ] && usage
+[ "$#" -gt 1 ] && usage
 
 ARCHIVE="$1"; shift
 
@@ -48,7 +48,7 @@
 
 [ ! -f "$ARCHIVE" ] && fail "Bad archive file $ARCHIVE"
 ARCHIVE_BASE=$(basename "$ARCHIVE")
-ARCHIVE_DIR=$(cd $(dirname "$ARCHIVE"); echo $PWD)
+ARCHIVE_DIR=$(cd $(dirname "$ARCHIVE"); echo "$PWD")
 ARCHIVE_FULL=$ARCHIVE_DIR/$ARCHIVE_BASE
 
 ISABELLE_NAME=$(basename "$ARCHIVE_BASE" .tar.gz)
@@ -121,7 +121,6 @@
 the ML compiler and any of the precompiled Isabelle object-logics
 (e.g. package isabelle-HOL).
 
-
 Isabelle is a popular generic theorem proving environment developed at
 Cambridge University (Larry Paulson) and TU Munich (Tobias Nipkow).
 The system can be viewed from two main perspectives.  On the one hand
@@ -188,7 +187,6 @@
 This package contains the Isabelle documentation in PDF.  Note that
 the dvi version is already part of the base package.
 
-
 %prep
 
 %build
--- a/Admin/page/common/functions.pl	Mon Sep 11 18:00:47 2000 +0200
+++ b/Admin/page/common/functions.pl	Mon Sep 11 20:23:24 2000 +0200
@@ -98,7 +98,7 @@
       my @s = stat $filename;
       my $size = defined $s[7] ? $s[7]/1024 : 0;
 
-      return sprintf("%.1f", $size);
+      return sprintf("%d", $size);
     }
 
     sub setdowncolor {
--- a/Admin/page/dist-content/binary.content	Mon Sep 11 18:00:47 2000 +0200
+++ b/Admin/page/dist-content/binary.content	Mon Sep 11 20:23:24 2000 +0200
@@ -7,8 +7,7 @@
 
 This is the binary distribution of <!-- _GP_ distname --> for
 Linux/x86 systems.  It requires RPM based package management (as used
-by most Linux distributions), and <em>root</em> user access to
-install.
+by most Linux distributions), and root user access to install.
 
 <p>
 
@@ -28,14 +27,14 @@
 
 <p>
 
-Example installation in <tt>/usr/share</tt> (the default location).
+Example installation in <tt>/usr/share</tt> (the default location):
 
 <pre>
 rpm -i --prefix /usr/share polyml.i386.rpm
 rpm -i --prefix /usr/share isabelle.rpm
 rpm -i --prefix /usr/share isabelle-HOL.i386.rpm
 rpm -i --prefix /usr/share proofgeneral.rpm               #requires XEmacs-21
-rpm -i --prefix /usr/share xsymbol.rpm                    #requires XEmacs-21
+rpm -i --prefix /usr/share xsymbol.rpm
 </pre>
 
 <p>
@@ -53,25 +52,25 @@
 <!-- _GP_ setdowncolor("#E0E0E0") -->
 <center>
 <table border="0" cellspacing="5" cellpadding="4" width="520">
-  <!-- _GP_ download("Poly/ML base system", "contrib/polyml.tar.gz", "../..") -->
+  <!-- _GP_ download("Poly/ML base system", "contrib/polyml_base.tar.gz", "../..") -->
   <!-- _GP_ download("Poly/ML module for Linux/x86", "contrib/polyml_x86-linux.tar.gz", "../..") -->
   <!-- _GP_ download("Poly/ML module for Solaris/Sparc", "contrib/polyml_sparc-solaris.tar.gz", "../..") -->
   <!-- _GP_ download("Isabelle main system", distname . ".tar.gz", "../..") -->
-  <!-- _GP_ download("Isabelle pdf documentation (optional)", distname . "_pdf.tar.gz", "../..") -->  <!-- _GP_ download("Proof General system (recommended)", "contrib/proofgeneral.tar.gz", "../..") -->
-  <!-- _GP_ download("X-Symbol package (recommended)", "contrib/xsymbol.tar.gz", "../..") -->
+  <!-- _GP_ download("Isabelle pdf documentation (optional)", distname . "_pdf.tar.gz", "../..") -->  <!-- _GP_ download("Proof General system (recommended)", "contrib/ProofGeneral.tar.gz", "../..") -->
+  <!-- _GP_ download("X-Symbol package (recommended)", "contrib/x-symbol.tar.gz", "../..") -->
 </table>
 </center>
 
 <p>
 
-Example installation in <tt>/usr/share</tt> for Linux/x86.
+Example installation in <tt>/usr/share</tt> for Linux/x86:
 
 <pre>
-tar -C /usr/share -x -z -f polyml.tar.gz
+tar -C /usr/share -x -z -f polyml_base.tar.gz
 tar -C /usr/share -x -z -f polyml_x86-linux.tar.gz
 tar -C /usr/share -x -z -f <!-- _GP_ distname . ".tar.gz"-->
-tar -C /usr/share -x -z -f proofgeneral.tar.gz            #requires XEmacs-21
-tar -C /usr/share -x -z -f xsymbol.tar.gz                 #requires XEmacs-21
+tar -C /usr/share -x -z -f ProofGeneral.tar.gz            #requires XEmacs-21
+tar -C /usr/share -x -z -f x-symbol.tar.gz
 
 cd <!-- _GP_ "/usr/share/" . distname -->
 ./configure