# HG changeset patch # User wenzelm # Date 968696604 -7200 # Node ID 40f02ebcb3c04e47699f31432d8a720894dd4fe9 # Parent 3370f6aa32001e2775b8acce58e799c30d954447 tuned; diff -r 3370f6aa3200 -r 40f02ebcb3c0 Admin/README-rpm.html --- 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 @@ - - - - -Isabelle Binary Distribution - - - - -

Isabelle Binary Distribution

- -This is your fast path to Isabelle on Linux/x86 systems (with rpm -package management): - -

- -

-rpm -i smlnj-110.0-3.i386.rpm                           # mandatory
-rpm -i --prefix /usr/share isabelle.rpm                 # mandatory
-rpm -i --prefix /usr/share isabelle-HOL.i386.rpm        # recommended
-rpm -i --prefix /usr/share isabelle-HOL-Real.i386.rpm   # optional
-rpm -i --prefix /usr/share isabelle-ZF.i386.rpm         # optional
-rpm -i --prefix /usr/share isabelle-pdfdocs.rpm         # optional
-
- - - - diff -r 3370f6aa3200 -r 40f02ebcb3c0 Admin/makedist --- 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" diff -r 3370f6aa3200 -r 40f02ebcb3c0 Admin/makepage --- 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 <&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"; ) diff -r 3370f6aa3200 -r 40f02ebcb3c0 Admin/makerpm --- 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 diff -r 3370f6aa3200 -r 40f02ebcb3c0 Admin/page/common/functions.pl --- 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 { diff -r 3370f6aa3200 -r 40f02ebcb3c0 Admin/page/dist-content/binary.content --- 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 for Linux/x86 systems. It requires RPM based package management (as used -by most Linux distributions), and root user access to -install. +by most Linux distributions), and root user access to install.

@@ -28,14 +27,14 @@

-Example installation in /usr/share (the default location). +Example installation in /usr/share (the default location): 

 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

@@ -53,25 +52,25 @@

- + - - + +

-Example installation in /usr/share for Linux/x86. +Example installation in /usr/share for Linux/x86: 

-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 
-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 
 ./configure