# HG changeset patch # User wenzelm # Date 968686894 -7200 # Node ID 9734f27172039dac9e43ea1159154bdaec354a42 # Parent 3cf12ab0b8aca356e950532eac2a21e75dcdb29f improved WWW page generation (still somewhat experimental); diff -r 3cf12ab0b8ac -r 9734f2717203 Admin/filesizes --- a/Admin/filesizes Mon Sep 11 17:40:41 2000 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,94 +0,0 @@ -#!/bin/bash -# -# $Id$ -# -# filesizes -- calculate and substitute file sizes in isabelle web pages -# -# needs: -# working directory in dist, rpms + webpages generated and copied to dist -# $DISTNAME -# -# substitutes: -# -norpm: -# {PACKED_SIZE} {PACKED_SIZE_PDF} {UNPACKED_SIZE} -# -rpm: -# {RPM_SML_SIZE} {RPM_BASE_SIZE} {RPM_HOL_SIZE} {RPM_REAL_SIZE} -# {RPM_ZF_SIZE} {RPM_DOCS_SIZE} - - -PRG=$(basename $0) - -function usage() -{ - echo - echo "Usage: $PRG [-rpm|-norpm]" - echo - echo "fill in file sizes and distname in isabelle dist web pages" - echo - echo " Options are:" - echo " -rpm only fill in rpm sizes" - echo " -norpm only fille in other sizes" - echo " (do both by default)" - echo - echo "needs \$DISTNAME environment variable" - echo "expects to be startet in isabelle dist dir" - echo - exit 1 -} - -function fail() -{ - echo "$1" >&2 - exit 2 -} - -# check options - -if [ $# -ge 2 ]; then - usage -fi - -if [ $# -eq 1 -a "$1" != "-rpm" -a "$1" != "-norpm" ]; then - usage -fi - - -# begin work - -if [ $# -eq 0 -o "$1" = "-norpm" ]; then - - # check for $DISTNAME - if [ "$DISTNAME" = "" ]; then - echo "Error: \$DISTNAME not set" - usage - fi - - PACKED_SIZE=$[ $(wc -c < $DISTNAME.tar.gz) / 1024 ] - PACKED_SIZE_PDF=$[ $(wc -c < ${DISTNAME}_pdf.tar.gz) / 1024 ] - - UNPACKED_SIZE=$[ $(cat $DISTNAME.tar.gz ${DISTNAME}_pdf.tar.gz | gunzip | wc -c) / 1024 ] - - perl -pi -e \ - "s/{UNPACKED_SIZE}/$UNPACKED_SIZE/g; \ - s/{PACKED_SIZE}/$PACKED_SIZE/g; \ - s/{PACKED_SIZE_PDF}/$PACKED_SIZE_PDF/g;" \ - *.html -fi - -if [ $# -eq 0 -o "$1" = "-rpm" ]; then - RPM_SML_SIZE=$[ $(wc -c < rpm/polyml-3X-1.i386.rpm) / 1024 ] - RPM_BASE_SIZE=$[ $(wc -c < rpm/isabelle.rpm) / 1024 ] - RPM_HOL_SIZE=$[ $(wc -c < rpm/isabelle-HOL.i386.rpm) / 1024 ] - RPM_REAL_SIZE=$[ $(wc -c < rpm/isabelle-HOL-Real.i386.rpm) / 1024 ] - RPM_ZF_SIZE=$[ $(wc -c < rpm/isabelle-ZF.i386.rpm) / 1024 ] - RPM_DOCS_SIZE=$[ $(wc -c < rpm/isabelle-pdfdocs.rpm) / 1024 ] - - perl -pi -e \ - "s/{RPM_SML_SIZE}/$RPM_SML_SIZE/g; \ - s/{RPM_BASE_SIZE}/$RPM_BASE_SIZE/g; \ - s/{RPM_HOL_SIZE}/$RPM_HOL_SIZE/g; \ - s/{RPM_REAL_SIZE}/$RPM_REAL_SIZE/g; \ - s/{RPM_ZF_SIZE}/$RPM_ZF_SIZE/g; \ - s/{RPM_DOCS_SIZE}/$RPM_DOCS_SIZE/g;" \ - *.html -fi diff -r 3cf12ab0b8ac -r 9734f2717203 Admin/makedist --- a/Admin/makedist Mon Sep 11 17:40:41 2000 +0200 +++ b/Admin/makedist Mon Sep 11 17:41:34 2000 +0200 @@ -14,6 +14,12 @@ umask 022 +TAR=tar +type -path gtar >/dev/null && TAR=gtar + +FIND=find +type -path gfind >/dev/null && FIND=gfind + ## diagnostics @@ -110,10 +116,10 @@ cd "$DISTBASE" $EXPORT -find . -name CVS -print | xargs rm -rf -find . "(" -type d -a -empty ")" -print | xargs rm -f -find . "(" -type d -a -empty ")" -print | xargs rm -f -find . "(" -type d -a -empty ")" -print | xargs rm -f +$FIND . -name CVS -print | xargs rm -rf +$FIND . "(" -type d -a -empty ")" -print | xargs rm -rf +$FIND . "(" -type d -a -empty ")" -print | xargs rm -rf +$FIND . "(" -type d -a -empty ")" -print | xargs rm -rf # build docs @@ -128,24 +134,27 @@ for DOC in $(cat Contents) do cd "$DOC" - make dvi - [ -n "$PDFLATEX" ] && make clean pdf + #FIXME make dvi + #FIXME [ -n "$PDFLATEX" ] && make clean pdf cd .. done -# make WWW pages +# prepare dist dir for release -#FIXME -#export DISTNAME -#( cd "$DISTBASE/$DISTNAME/Admin/page"; make clean; make dist; cd dist; cp * "$DISTBASE"; ) - - -# prepare dist dir for release +echo "###" +echo "### Preparing distribution ..." +echo "###" cd "$DISTBASE/$DISTNAME" -MOVE=$(find Doc \( -type f -a \( -name \*.dvi -o -name \*.eps -o -name \*.ps -o -name \*.pdf \) -a -print \) | grep -v 'gfx/.*pdf') +cp -R Admin/page ../page +cp Distribution/Doc/Contents ../page/Contents +cp Distribution/lib/logo/isabelle.gif ../page/main-content +cp Distribution/lib/logo/isabelle.gif ../page/dist-content +echo "$DISTNAME" > ../page/DISTNAME + +MOVE=$($FIND Doc \( -type f -a \( -name \*.dvi -o -name \*.eps -o -name \*.ps -o -name \*.pdf \) -a -print \) | grep -v 'gfx/.*pdf') mv -f $MOVE Distribution/doc rm Distribution/doc/Isa-logics.eps rm -rf Doc Tools @@ -194,9 +203,6 @@ chmod -R u+w "$DISTNAME" chmod -R g=o "$DISTNAME" -TAR=tar -type -path gtar >/dev/null && TAR=gtar - mkdir -p "pdf/$DISTNAME/doc" mv "$DISTNAME/doc/"*.pdf "pdf/$DISTNAME/doc" @@ -215,7 +221,6 @@ mv "$DISTNAME" "${DISTNAME}-old" mkdir "$DISTNAME" -mv "${DISTNAME}-old/lib/logo/isabelle.gif" . mv "${DISTNAME}-old/README.html" "${DISTNAME}-old/INSTALL" "$DISTNAME" mkdir "$DISTNAME/doc" mv "${DISTNAME}-old/doc/"*.pdf "${DISTNAME}-old/doc/Contents" "$DISTNAME/doc" @@ -225,14 +230,8 @@ rm -rf "${DISTNAME}-old" -# prepare web pages - -#FIXME -#$THIS/filesizes -norpm - - # final note echo "###" -echo "### Finished. You will find the distribution in $DISTBASE." +echo "### Finished." echo "###" diff -r 3cf12ab0b8ac -r 9734f2717203 Admin/page/Makefile --- a/Admin/page/Makefile Mon Sep 11 17:40:41 2000 +0200 +++ b/Admin/page/Makefile Mon Sep 11 17:41:34 2000 +0200 @@ -1,12 +1,10 @@ -# --- uses $DISTNAME environment variable - # -- makefile for Isabelle web pages (dist and main) # -- $Id$ -# --- perl scripts used in this makefile +# --- external tools -GENPAGE = bin/genpage -MKCONTENT = bin/mkcontents +GENPAGE = ./bin/genpage +MKCONTENT = ./bin/mkcontents # --- # --- genpage stuff @@ -30,11 +28,7 @@ # --- doc content generation # --- location of the Contents file of the Isabelle documentation -DOC_CONTENT_FILE = ../../Distribution/doc/Contents - -# --- url prefixes for documentation links in main and dist dirs -DIST_DOCU_PREFIX = $(DISTNAME)/doc/ -MAIN_DOCU_PREFIX = dist/$(DISTNAME)/doc/ +DOC_CONTENT_FILE = Contents # --- target include files with documentation links DOC_CONTENTS_MAIN = docu-contents.main @@ -43,28 +37,24 @@ # --- # --- begin rules -all: clean gen - -gen: main dist - -main: check - $(MKCONTENT) -p $(MAIN_DOCU_PREFIX) Contents $(DOC_CONTENTS_MAIN) - $(GENPAGE) -t $(MAIN_LAYOUT)/$(TEMPLATE_NAME) -c $(MAIN_CONTENT) -o $(MAIN_TARGET) +all: clean main dist + @echo "###" + @echo "### Finished. See main/ and dist/ for the resulting pages." + @echo "###" - cd $(MAIN_TARGET); perl -pi -e "s/{ISABELLE}/$(DISTNAME)/g;" *.html +main: + @$(MKCONTENT) -p dist/`cat DISTNAME`/doc/ $(DOC_CONTENT_FILE) $(DOC_CONTENTS_MAIN) + @env DISTNAME=`cat DISTNAME` \ + $(GENPAGE) -t $(MAIN_LAYOUT)/$(TEMPLATE_NAME) -c $(MAIN_CONTENT) -o $(MAIN_TARGET) -dist: check - $(MKCONTENT) -p $(DIST_DOCU_PREFIX) $(DOC_CONTENT_FILE) $(DOC_CONTENTS_DIST) - $(GENPAGE) -t $(DIST_LAYOUT)/$(TEMPLATE_NAME) -c $(DIST_CONTENT) -o $(DIST_TARGET) - - cd $(DIST_TARGET); perl -pi -e "s/{ISABELLE}/$(DISTNAME)/g;" *.html +dist: + @$(MKCONTENT) -p `cat DISTNAME`/doc/ $(DOC_CONTENT_FILE) $(DOC_CONTENTS_DIST) + @env DISTNAME=`cat DISTNAME` \ + $(GENPAGE) -t $(DIST_LAYOUT)/$(TEMPLATE_NAME) -c $(DIST_CONTENT) -o $(DIST_TARGET) clean: - rm -rf $(MAIN_TARGET) - rm -rf $(DIST_TARGET) - rm -rf $(DOC_CONTENTS_MAIN) - rm -rf $(DOC_CONTENTS_DIST) - rm -f `find . -name "*~" -type f` - -check: - @if [ "$(DISTNAME)" = "" ]; then echo "Error: \$$DISTNAME not set."; exit 1; fi + @rm -rf $(MAIN_TARGET) + @rm -rf $(DIST_TARGET) + @rm -rf $(DOC_CONTENTS_MAIN) + @rm -rf $(DOC_CONTENTS_DIST) + @find . -name "*~" -type f -print | xargs rm -f diff -r 3cf12ab0b8ac -r 9734f2717203 Admin/page/bin/genpage --- a/Admin/page/bin/genpage Mon Sep 11 17:40:41 2000 +0200 +++ b/Admin/page/bin/genpage Mon Sep 11 17:41:34 2000 +0200 @@ -1,7 +1,4 @@ -#!/bin/sh -exec perl -x. $0 ${1+"$@"} -# -#!perl -w +#!/usr/bin/perl -w # Genpage - Webpage Generator. # diff -r 3cf12ab0b8ac -r 9734f2717203 Admin/page/common/functions.pl --- a/Admin/page/common/functions.pl Mon Sep 11 17:40:41 2000 +0200 +++ b/Admin/page/common/functions.pl Mon Sep 11 17:41:34 2000 +0200 @@ -1,9 +1,12 @@ for +Linux/x86 systems. It requires RPM based package management (as used +by most Linux distributions), and root user access to +install.

- - - - - - - - + + + + + + + +
-

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

-rpm -i smlnj-110.0-3.i386.rpm 
-rpm -i --prefix /usr/share isabelle.rpm             
-rpm -i --prefix /usr/share isabelle-HOL.i386.rpm    
+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

-Use the mailing list isabelle-users@cl.cam.ac.uk -to discuss problems and results. (Why not subscribe?) + +

(2) Generic Linux/x86 or Solaris/Sparc systems

+ +The following distribution of works for any +Linux/x86 or Solaris/Sparc system -- only Poly/ML is platform +dependent. Installation does not rely on package management; it may +be performed by non-root users as well. + +

+ + +

+ + + + + + + +
+
+ +

+ +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_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
+
+cd 
+./configure
+./build
+./bin/isatool install -p /usr/bin
+
+ +

+ +

diff -r 3cf12ab0b8ac -r 9734f2717203 Admin/page/dist-content/docs.content --- a/Admin/page/dist-content/docs.content Mon Sep 11 17:40:41 2000 +0200 +++ b/Admin/page/dist-content/docs.content Mon Sep 11 17:41:34 2000 +0200 @@ -6,4 +6,5 @@ -All this documentation is also part of the Isabelle distribution. +All this documentation is also part of the Isabelle distribution (both as dvi and pdf). diff -r 3cf12ab0b8ac -r 9734f2717203 Admin/page/dist-content/index.content --- a/Admin/page/dist-content/index.content Mon Sep 11 17:40:41 2000 +0200 +++ b/Admin/page/dist-content/index.content Mon Sep 11 17:41:34 2000 +0200 @@ -21,5 +21,3 @@

  • Stanford (USA)
     
    • - - diff -r 3cf12ab0b8ac -r 9734f2717203 Admin/page/dist-content/past.content --- a/Admin/page/dist-content/past.content Mon Sep 11 17:40:41 2000 +0200 +++ b/Admin/page/dist-content/past.content Mon Sep 11 17:41:34 2000 +0200 @@ -4,9 +4,10 @@ %body%

    -The past releases of Isabelle from the Cambrige ftp archive: +Past releases of Isabelle are available from the Cambrige ftp archive: