website preparation for Isabelle2005
authorhaftmann
Tue Sep 27 15:30:37 2005 +0200 (2005-09-27)
changeset 17671e9e341bc7d42
parent 17670 bf4f2c1b26cc
child 17672 25d8a4586836
website preparation for Isabelle2005
Admin/isasync
Admin/mirror-main
Admin/mirror-website
Admin/rsyncd.conf
Admin/website/build/localconf.at.template.mak
Admin/website/build/localconf.sun.template.mak
Admin/website/build/main.mak
Admin/website/build/project.mak
Admin/website/documentation.html
Admin/website/include/documentationdist.include.html
Admin/website/include/downloadtable.include.html
Admin/website/index.html
Admin/website/installation.html
Admin/website/overview.html
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/Admin/isasync	Tue Sep 27 15:30:37 2005 +0200
     1.3 @@ -0,0 +1,131 @@
     1.4 +#!/usr/bin/env bash
     1.5 +#
     1.6 +# $Id$
     1.7 +#
     1.8 +# mirror script for Isabelle distribution or website
     1.9 +
    1.10 +
    1.11 +## diagnostics
    1.12 +
    1.13 +PRG=`basename "$0"`
    1.14 +
    1.15 +usage()
    1.16 +{
    1.17 +  echo
    1.18 +  echo "Usage: $PRG [OPTIONS] DEST"
    1.19 +  echo
    1.20 +  echo "  Options are:"
    1.21 +  echo "    -h    print help message"
    1.22 +  echo "    -n    dry run, don't do anything, just report what would happen"
    1.23 +  echo "    -w    mirror whole Isabelle website"
    1.24 +  echo "    -d    delete files that are not on the server (BEWARE!)"
    1.25 +  echo
    1.26 +  exit 1
    1.27 +}
    1.28 +
    1.29 +fail()
    1.30 +{
    1.31 +  echo "$1" >&2
    1.32 +  exit 2
    1.33 +}
    1.34 +
    1.35 +
    1.36 +## process command line
    1.37 +
    1.38 +# options
    1.39 +
    1.40 +HELP=""
    1.41 +ARGS=""
    1.42 +SRC="isabelle-distribution"
    1.43 +
    1.44 +while getopts "hnwd" OPT
    1.45 +do
    1.46 +  case "$OPT" in
    1.47 +    h)
    1.48 +      HELP=true
    1.49 +      ;;
    1.50 +    n)
    1.51 +      ARGS="$ARGS -n"
    1.52 +      ;;
    1.53 +    w)
    1.54 +      SRC="isabelle-website"
    1.55 +      ;;
    1.56 +    d)
    1.57 +      ARGS="$ARGS --delete"
    1.58 +      ;;
    1.59 +    \?)
    1.60 +      usage
    1.61 +      ;;
    1.62 +  esac
    1.63 +done
    1.64 +
    1.65 +shift `expr $OPTIND - 1`
    1.66 +
    1.67 +
    1.68 +# help
    1.69 +
    1.70 +if [ -n "$HELP" ]; then
    1.71 +  cat <<EOF
    1.72 +
    1.73 +Mirroring the Isabelle distribution or website
    1.74 +==============================================
    1.75 +
    1.76 +The Munich site maintains an rsync server for the Isabelle
    1.77 +distribution or website.
    1.78 +
    1.79 +The rsync tool is very smart and efficient in mirroring large
    1.80 +directory hierarchies.  See http://rsync.samba.org/ for more
    1.81 +information.  The rsync-isabelle script provides a simple front-end
    1.82 +for easy access to the Isabelle distribution.
    1.83 +
    1.84 +The script can be either run in conservative or clean-sweep mode.
    1.85 +
    1.86 +1) Basic mirroring works like this:
    1.87 +
    1.88 +  $PRG /foo/bar
    1.89 +
    1.90 +where /foo/bar refers to your local copy of the Isabelle distribution
    1.91 +(the base directory has to exist already).  This operation is
    1.92 +conservative in the sense that files are never deleted, thus garbage
    1.93 +may accumulate over time as our master copy is changed.
    1.94 +
    1.95 +Avoiding garbage in your local copy requires some care.  Rsync
    1.96 +provides a way to delete all additional local files that are absent in
    1.97 +the master copy.  This provides an efficient way to purge large
    1.98 +directory hierarchies, even unwillingly in case that a wrong
    1.99 +destination is given!
   1.100 +
   1.101 +2a) This will invoke a safe dry-run of clean-sweep mirroring:
   1.102 +
   1.103 +  $PRG -dn /foo/bar
   1.104 +
   1.105 +where additions and deletions will be printed without any actual
   1.106 +changes performed so far.
   1.107 +
   1.108 +2b) Exact mirroring with actual deletion of garbage may be performed
   1.109 +like this:
   1.110 +
   1.111 +  $PRG -d /foo/bar
   1.112 +
   1.113 +
   1.114 +After gaining some confidence in the workings of rsync-isabelle one
   1.115 +would usually set up some automatic mirror scheme, e.g. a daily cron
   1.116 +job run by the 'nobody' user.
   1.117 +
   1.118 +Add -w to the option list in order to mirror the whole Isabelle website
   1.119 +
   1.120 +EOF
   1.121 +  exit 0
   1.122 +fi
   1.123 +
   1.124 +
   1.125 +# arguments
   1.126 +
   1.127 +[ $# -ne 1 ] && { echo "Bad arguments: $*"; usage; }
   1.128 +
   1.129 +DEST="$1"; shift;
   1.130 +
   1.131 +
   1.132 +## main
   1.133 +
   1.134 +exec rsync -va $ARGS "rsync://isabelle.in.tum.de/$SRC/." "$DEST/."
     2.1 --- a/Admin/mirror-main	Tue Sep 27 14:41:41 2005 +0200
     2.2 +++ b/Admin/mirror-main	Tue Sep 27 15:30:37 2005 +0200
     2.3 @@ -31,4 +31,4 @@
     2.4  echo "Warning: this script now mirrors the *complete* Isabelle site"
     2.5  
     2.6  rsync --rsh ssh --rsync-path /usr/local/dist/bin/rsync -va --copy-links \
     2.7 -  $USER@sunbroy2.informatik.tu-muenchen.de:/usr/proj/isabelle-repository/www/. $DEST/.
     2.8 +  $USER@sunbroy2.informatik.tu-muenchen.de:/home/proj/isabelle/website/. $DEST/.
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/Admin/mirror-website	Tue Sep 27 15:30:37 2005 +0200
     3.3 @@ -0,0 +1,26 @@
     3.4 +#!/usr/bin/env bash
     3.5 +#
     3.6 +# $Id$
     3.7 +#
     3.8 +# mirrors the Isabelle website
     3.9 +
    3.10 +HOST=$(hostname)
    3.11 +
    3.12 +case ${HOST} in
    3.13 +  sunbroy2)
    3.14 +    DEST=/home/html/isabelle/html-data
    3.15 +    ;;
    3.16 +  atbroy1)
    3.17 +    DEST=/home/html/isabelle/html-data
    3.18 +    ;;
    3.19 +  *.cl.cam.ac.uk)
    3.20 +    USER=paulson
    3.21 +    DEST=/anfs/www/html/Research/HVG/Isabelle
    3.22 +    ;;
    3.23 +  *)
    3.24 +    echo "Unknown destination directory for ${HOST}"
    3.25 +    exit 2
    3.26 +    ;;
    3.27 +esac
    3.28 +
    3.29 +exec $(dirname $0)/isasync -dw $DEST
     4.1 --- a/Admin/rsyncd.conf	Tue Sep 27 14:41:41 2005 +0200
     4.2 +++ b/Admin/rsyncd.conf	Tue Sep 27 15:30:37 2005 +0200
     4.3 @@ -1,8 +1,4 @@
     4.4 -#
     4.5  # rsync server configuration
     4.6 -#
     4.7 -# $Id$
     4.8 -#
     4.9  
    4.10  uid = nobody 
    4.11  gid = nobody 
    4.12 @@ -10,7 +6,15 @@
    4.13  log file = /tmp/rsyncd.log
    4.14  read only = true
    4.15  
    4.16 +[isabelle-website]
    4.17 +    path = /home/proj/isabelle/website
    4.18 +    comment = Isabelle website
    4.19 +
    4.20 +[isabelle-distribution]
    4.21 +    path = /home/proj/isabelle/website/dist
    4.22 +    comment = Isabelle distribution
    4.23 +
    4.24 +# Sydney legacy link
    4.25  [isabelle-dist]
    4.26 -        path = /home/html/isabelle/html-data/dist/
    4.27 -        comment = Isabelle distribution area
    4.28 -
    4.29 +    path = /home/html/isabelle/html-data/dist/
    4.30 +    comment = Isabelle distribution area
     5.1 --- a/Admin/website/build/localconf.at.template.mak	Tue Sep 27 14:41:41 2005 +0200
     5.2 +++ b/Admin/website/build/localconf.at.template.mak	Tue Sep 27 15:30:37 2005 +0200
     5.3 @@ -1,29 +1,29 @@
     5.4  # isaweb configuration
     5.5  # $Id$
     5.6  
     5.7 -# python interpreter (> 2.2)
     5.8 +# python interpreter (>= 2.3)
     5.9  PYTHON=python
    5.10  
    5.11  # GNU find
    5.12  FIND=find
    5.13  
    5.14 +# GNU copy
    5.15 +COPY=cp
    5.16 +
    5.17  # HTML tidy (needs not to be set if tidy usage is disabled, see below)
    5.18  TIDY=tidy
    5.19  
    5.20  # dirs to copy to build target
    5.21 -STATICDIRS=css img media misc dist
    5.22 +STATICDIRS=css img media misc
    5.23  
    5.24  # build target (attention: ~ will not work!)
    5.25 -OUTPUTROOT=/home/proj/isabelle/website
    5.26 +OUTPUTROOT=$(HOME)/isabelle/website_test
    5.27  
    5.28  # location of isabelle distribution packages
    5.29 -ISABELLE_DIST=/home/proj/isabelle/dist/Isabelle2004
    5.30 -
    5.31 -# location of isabelle library 
    5.32 -ISABELLE_LIBR=/home/proj/isabelle/dist/library-Isabelle2004
    5.33 +ISABELLE_DIST=/home/proj/isabelle/dist/dist-Isabelle2005
    5.34  
    5.35  # location of doc content file
    5.36 -ISABELLE_DOC_CONTENT_FILE=/home/proj/isabelle/Isabelle2004/doc/Contents
    5.37 +ISABELLE_DOC_CONTENT_FILE=/home/proj/isabelle/dist/dist-Isabelle2005/doc/Contents
    5.38  
    5.39  # umask for target files
    5.40  TARGET_UMASK_FILE=664
     6.1 --- a/Admin/website/build/localconf.sun.template.mak	Tue Sep 27 14:41:41 2005 +0200
     6.2 +++ b/Admin/website/build/localconf.sun.template.mak	Tue Sep 27 15:30:37 2005 +0200
     6.3 @@ -1,29 +1,29 @@
     6.4  # isaweb configuration
     6.5  # $Id$
     6.6  
     6.7 -# python interpreter (> 2.2)
     6.8 +# python interpreter (>= 2.3)
     6.9  PYTHON=python2.3
    6.10  
    6.11  # GNU find
    6.12  FIND=gfind
    6.13  
    6.14 +# GNU copy
    6.15 +COPY=gcp
    6.16 +
    6.17  # HTML tidy (needs not to be set if tidy usage is disabled, see below)
    6.18  TIDY=tidy
    6.19  
    6.20  # dirs to copy to build target
    6.21 -STATICDIRS=css img media misc dist
    6.22 +STATICDIRS=css img media misc
    6.23  
    6.24  # build target (attention: ~ will not work!)
    6.25 -OUTPUTROOT=/home/proj/isabelle/website
    6.26 +OUTPUTROOT=$(HOME)/isabelle/website_test
    6.27  
    6.28  # location of isabelle distribution packages
    6.29 -ISABELLE_DIST=/home/proj/isabelle/dist/Isabelle2004
    6.30 -
    6.31 -# location of isabelle library 
    6.32 -ISABELLE_LIBR=/home/proj/isabelle/dist/library-Isabelle2004
    6.33 +ISABELLE_DIST=/home/proj/isabelle/dist/dist-Isabelle2005
    6.34  
    6.35  # location of doc content file
    6.36 -ISABELLE_DOC_CONTENT_FILE=/home/proj/isabelle/Isabelle2004/doc/Contents
    6.37 +ISABELLE_DOC_CONTENT_FILE=/home/proj/isabelle/dist/dist-Isabelle2005/doc/Contents
    6.38  
    6.39  # umask for target files
    6.40  TARGET_UMASK_FILE=664
     7.1 --- a/Admin/website/build/main.mak	Tue Sep 27 14:41:41 2005 +0200
     7.2 +++ b/Admin/website/build/main.mak	Tue Sep 27 15:30:37 2005 +0200
     7.3 @@ -96,7 +96,7 @@
     7.4  	done; \
     7.5  	echo "DEP_ALLSTATIC=$$allstatic" >> $(DEP_FILE); \
     7.6  	echo >> $(DEP_FILE); \
     7.7 -	echo 'DEP_HTML=$$(DEP_ALLSTATIC) $$(DEP_SYMLINKS) include/documentationdist.include.html $(DEP_FILE) $(CONF)' >> $(DEP_FILE); \
     7.8 +	echo 'DEP_HTML=$$(DEP_ALLSTATIC) include/documentationdist.include.html $(DEP_FILE) $(CONF)' >> $(DEP_FILE); \
     7.9  	echo >> $(DEP_FILE); \
    7.10  	allhtml=''; \
    7.11  	for html in `$(FIND) . -name "*.html" -a ! -name "*.include.html"`; \
     8.1 --- a/Admin/website/build/project.mak	Tue Sep 27 14:41:41 2005 +0200
     8.2 +++ b/Admin/website/build/project.mak	Tue Sep 27 15:30:37 2005 +0200
     8.3 @@ -1,35 +1,19 @@
     8.4  # isaweb makefile - project-specific dependencies
     8.5  # $Id$
     8.6  
     8.7 -project: site
     8.8 -	chmod -R g-w $(OUTPUTROOT)/dist/packages
     8.9 +project: $(OUTPUTROOT)/dist site
    8.10  .PHONY: project
    8.11  
    8.12 -#~ DEP_SYMLINKS=$(OUTPUTROOT)/dist/packages $(OUTPUTROOT)/library
    8.13 -
    8.14 -#~ $(OUTPUTROOT)/dist/packages: $(ISABELLE_DIST)
    8.15 -	#~ mkdir -p $(OUTPUTROOT)/dist
    8.16 -	#~ ln -s $< $@
    8.17 -
    8.18 -DEP_SYMLINKS=dist/packages $(OUTPUTROOT)/dist/library
    8.19 +cleanproject:
    8.20 +	rm -rf $(OUTPUTROOT)/dist
    8.21 +.PHONY: cleanproject
    8.22  
    8.23 -dist/packages: $(ISABELLE_DIST)
    8.24 -	mkdir -p dist
    8.25 -	ln -s $< $@
    8.26 -
    8.27 -#~ library: $(ISABELLE_LIBR)
    8.28 -#~	ln -s $< $@
    8.29 -
    8.30 -$(OUTPUTROOT)/dist/library: $(ISABELLE_LIBR)
    8.31 -	mkdir -p $(OUTPUTROOT)/dist
    8.32 -	ln -s $< $@
    8.33 -	chmod $(TARGET_UMASK_DIR) $@
    8.34 +$(OUTPUTROOT)/dist: $(ISABELLE_DIST)
    8.35 +	$(COPY) -vRud $< $@
    8.36 +	chmod -R g-w $@
    8.37  
    8.38  include/documentationdist.include.html: $(ISABELLE_DOC_CONTENT_FILE)
    8.39 -	perl build/mkcontents.pl -p '//dist/packages/Isabelle/doc/' $< $@
    8.40 -
    8.41 -symlinks: $(DEP_SYMLINKS)
    8.42 -.PHONY: symlinks
    8.43 +	perl build/mkcontents.pl -p '//dist/Isabelle/doc/' $< $@
    8.44  
    8.45  include conf/distname.mak
    8.46  conf/distname.mak:
    8.47 @@ -38,6 +22,6 @@
    8.48  	echo 'If you have no makedist at hand, allocate a conf/distname.mak file'; \
    8.49  	echo 'yourself, e. g. by:'; \
    8.50  	echo; \
    8.51 -	echo 'echo "DISTNAME=Isabelle2004" > conf/distname.mak'; \
    8.52 +	echo 'echo "DISTNAME=Isabelle1705" > conf/distname.mak'; \
    8.53  	echo; \
    8.54  	false; \
     9.1 --- a/Admin/website/documentation.html	Tue Sep 27 14:41:41 2005 +0200
     9.2 +++ b/Admin/website/documentation.html	Tue Sep 27 15:30:37 2005 +0200
     9.3 @@ -23,7 +23,7 @@
     9.4                  width="83" height="125"/>
     9.5          </a>
     9.6          <p>For getting started with Isabelle quickly, we recommend the <a href=
     9.7 -        "//dist/packages/Isabelle/doc/tutorial.pdf">Tutorial on
     9.8 +        "//dist/Isabelle/doc/tutorial.pdf">Tutorial on
     9.9          Isabelle/HOL</a> (published by Springer Verlag as <a href=
    9.10          "http://www4.in.tum.de/~nipkow/LNCS2283/">LNCS 2283</a>) and the <a href=
    9.11          "#course_material">course material</a>.</p>
    9.12 @@ -51,12 +51,12 @@
    9.13          <h3>Release notes</h3>
    9.14  
    9.15            <ul>
    9.16 -            <li><a href="//dist/packages/Isabelle/ANNOUNCE">ANNOUNCE</a></li>
    9.17 -            <li><a href="//dist/packages/Isabelle/README.html">README</a></li>
    9.18 -            <li><a href="//dist/packages/Isabelle/INSTALL">INSTALL</a></li>
    9.19 -            <li><a href="//dist/packages/Isabelle/NEWS">NEWS</a></li>
    9.20 -            <li><a href="//dist/packages/Isabelle/COPYRIGHT">COPYRIGHT</a></li>
    9.21 -            <li><a href="//dist/packages/Isabelle/CONTRIBUTORS">CONTRIBUTORS</a></li>
    9.22 +            <li><a href="//dist/Isabelle/ANNOUNCE">ANNOUNCE</a></li>
    9.23 +            <li><a href="//dist/Isabelle/README.html">README</a></li>
    9.24 +            <li><a href="//dist/Isabelle/INSTALL">INSTALL</a></li>
    9.25 +            <li><a href="//dist/Isabelle/NEWS">NEWS</a></li>
    9.26 +            <li><a href="//dist/Isabelle/COPYRIGHT">COPYRIGHT</a></li>
    9.27 +            <li><a href="//dist/Isabelle/CONTRIBUTORS">CONTRIBUTORS</a></li>
    9.28            </ul>
    9.29  
    9.30          <h2 id="course_material">Course Material and Exercises</h2>
    10.1 --- a/Admin/website/include/documentationdist.include.html	Tue Sep 27 14:41:41 2005 +0200
    10.2 +++ b/Admin/website/include/documentationdist.include.html	Tue Sep 27 15:30:37 2005 +0200
    10.3 @@ -2,26 +2,26 @@
    10.4  <dummy:wrapper xmlns:dummy="http://nowhere.no">
    10.5  <h3>Learning Isabelle</h3>
    10.6  <ul>
    10.7 -  <li><a target='_blank' href='//dist/packages/Isabelle/doc/tutorial.pdf'>Tutorial on Isabelle/HOL</a></li>
    10.8 -  <li><a target='_blank' href='//dist/packages/Isabelle/doc/isar-overview.pdf'>Tutorial on Isar</a></li>
    10.9 -  <li><a target='_blank' href='//dist/packages/Isabelle/doc/locales.pdf'>Tutorial on Locales</a></li>
   10.10 +  <li><a target='_blank' href='//dist/Isabelle/doc/tutorial.pdf'>Tutorial on Isabelle/HOL</a></li>
   10.11 +  <li><a target='_blank' href='//dist/Isabelle/doc/isar-overview.pdf'>Tutorial on Isar</a></li>
   10.12 +  <li><a target='_blank' href='//dist/Isabelle/doc/locales.pdf'>Tutorial on Locales</a></li>
   10.13  </ul>
   10.14  <h3>Reference Manuals</h3>
   10.15  <ul>
   10.16 -  <li><a target='_blank' href='//dist/packages/Isabelle/doc/isar-ref.pdf'>The Isabelle/Isar Reference Manual</a></li>
   10.17 -  <li><a target='_blank' href='//dist/packages/Isabelle/doc/ref.pdf'>The Isabelle Reference Manual</a></li>
   10.18 -  <li><a target='_blank' href='//dist/packages/Isabelle/doc/system.pdf'>The Isabelle System Manual</a></li>
   10.19 +  <li><a target='_blank' href='//dist/Isabelle/doc/isar-ref.pdf'>The Isabelle/Isar Reference Manual</a></li>
   10.20 +  <li><a target='_blank' href='//dist/Isabelle/doc/ref.pdf'>The Isabelle Reference Manual</a></li>
   10.21 +  <li><a target='_blank' href='//dist/Isabelle/doc/system.pdf'>The Isabelle System Manual</a></li>
   10.22  </ul>
   10.23  <h3>Logics</h3>
   10.24  <ul>
   10.25 -  <li><a target='_blank' href='//dist/packages/Isabelle/doc/logics.pdf'>Isabelle's Logics: overview and misc logics</a></li>
   10.26 -  <li><a target='_blank' href='//dist/packages/Isabelle/doc/logics-HOL.pdf'>Isabelle's Logics: HOL</a></li>
   10.27 -  <li><a target='_blank' href='//dist/packages/Isabelle/doc/logics-ZF.pdf'>Isabelle's Logics: FOL and ZF</a></li>
   10.28 +  <li><a target='_blank' href='//dist/Isabelle/doc/logics.pdf'>Isabelle's Logics: overview and misc logics</a></li>
   10.29 +  <li><a target='_blank' href='//dist/Isabelle/doc/logics-HOL.pdf'>Isabelle's Logics: HOL</a></li>
   10.30 +  <li><a target='_blank' href='//dist/Isabelle/doc/logics-ZF.pdf'>Isabelle's Logics: FOL and ZF</a></li>
   10.31  </ul>
   10.32  <h3>Specific Topics</h3>
   10.33  <ul>
   10.34 -  <li><a target='_blank' href='//dist/packages/Isabelle/doc/sugar.pdf'>LaTeX sugar for proof documents</a></li>
   10.35 -  <li><a target='_blank' href='//dist/packages/Isabelle/doc/axclass.pdf'>Tutorial on Axiomatic Type Classes</a></li>
   10.36 -  <li><a target='_blank' href='//dist/packages/Isabelle/doc/ind-defs.pdf'>(Co)Inductive Definitions in ZF</a></li>
   10.37 +  <li><a target='_blank' href='//dist/Isabelle/doc/sugar.pdf'>LaTeX sugar for proof documents</a></li>
   10.38 +  <li><a target='_blank' href='//dist/Isabelle/doc/axclass.pdf'>Tutorial on Axiomatic Type Classes</a></li>
   10.39 +  <li><a target='_blank' href='//dist/Isabelle/doc/ind-defs.pdf'>(Co)Inductive Definitions in ZF</a></li>
   10.40  </ul>
   10.41  </dummy:wrapper>
    11.1 --- a/Admin/website/include/downloadtable.include.html	Tue Sep 27 14:41:41 2005 +0200
    11.2 +++ b/Admin/website/include/downloadtable.include.html	Tue Sep 27 15:30:37 2005 +0200
    11.3 @@ -7,104 +7,104 @@
    11.4      <td>
    11.5        Sources and documentation
    11.6      </td>
    11.7 -    <?downloadCells target="//dist/packages/Isabelle2005.tar.gz" title="Isabelle2005.tar.gz"?>
    11.8 +    <?downloadCells target="//dist/Isabelle2005.tar.gz" title="Isabelle2005.tar.gz"?>
    11.9    </tr>
   11.10    <tr>
   11.11      <td>
   11.12        Documentation in PDF
   11.13      </td>
   11.14 -    <?downloadCells target="//dist/packages/Isabelle2005_pdf.tar.gz" title="Isabelle2005_pdf.tar.gz"?>
   11.15 +    <?downloadCells target="//dist/Isabelle2005_pdf.tar.gz" title="Isabelle2005_pdf.tar.gz"?>
   11.16    </tr>
   11.17    <tr>
   11.18      <td>
   11.19        Theory library in PDF and HTML
   11.20      </td>
   11.21 -    <?downloadCells target="//dist/packages/Isabelle2005_library.tar.gz" title="Isabelle2005_library.tar.gz"?>
   11.22 +    <?downloadCells target="//dist/Isabelle2005_library.tar.gz" title="Isabelle2005_library.tar.gz"?>
   11.23    </tr>
   11.24    <tr><td colspan="3" class="downloadheader">Proof General</td></tr>
   11.25    <tr>
   11.26      <td>
   11.27        Proof General
   11.28      </td>
   11.29 -    <?downloadCells target="//dist/packages/contrib/ProofGeneral.tar.gz" title="ProofGeneral.tar.gz"?>
   11.30 +    <?downloadCells target="//dist/contrib/ProofGeneral.tar.gz" title="ProofGeneral.tar.gz"?>
   11.31    </tr>
   11.32    <tr><td colspan="3" class="downloadheader">Poly/ML compiler and runtime system</td></tr>
   11.33    <tr>
   11.34      <td rowspan="3">
   11.35        Poly/ML
   11.36      </td>
   11.37 -    <?downloadCells target="//dist/packages/contrib/polyml_x86-linux.tar.gz" title="polyml_x86-linux.tar.gz"?>
   11.38 +    <?downloadCells target="//dist/contrib/polyml_x86-linux.tar.gz" title="polyml_x86-linux.tar.gz"?>
   11.39    </tr>
   11.40    <tr>
   11.41      <td style="display: none"></td>
   11.42 -    <?downloadCells target="//dist/packages/contrib/polyml_sparc-solaris.tar.gz" title="polyml_sparc-solaris.tar.gz"?>
   11.43 +    <?downloadCells target="//dist/contrib/polyml_sparc-solaris.tar.gz" title="polyml_sparc-solaris.tar.gz"?>
   11.44    </tr>
   11.45    <tr>
   11.46      <td style="display: none"></td>
   11.47 -    <?downloadCells target="//dist/packages/contrib/polyml_ppc-darwin.tar.gz" title="polyml_ppc-darwin.tar.gz"?>
   11.48 +    <?downloadCells target="//dist/contrib/polyml_ppc-darwin.tar.gz" title="polyml_ppc-darwin.tar.gz"?>
   11.49    </tr>
   11.50    <tr><td colspan="3" class="downloadheader">Precompiled logics</td></tr>
   11.51    <tr>
   11.52      <td rowspan="3">
   11.53        HOL
   11.54      </td>
   11.55 -    <?downloadCells target="//dist/packages/HOL_x86-linux.tar.gz" title="HOL_x86-linux.tar.gz"?>
   11.56 +    <?downloadCells target="//dist/HOL_x86-linux.tar.gz" title="HOL_x86-linux.tar.gz"?>
   11.57    </tr>
   11.58    <tr>
   11.59      <td style="display: none"></td>
   11.60 -    <?downloadCells target="//dist/packages/HOL_sparc-solaris.tar.gz" title="HOL_sparc-solaris.tar.gz"?>
   11.61 +    <?downloadCells target="//dist/HOL_sparc-solaris.tar.gz" title="HOL_sparc-solaris.tar.gz"?>
   11.62    </tr>
   11.63    <tr>
   11.64      <td style="display: none"></td>
   11.65 -    <?downloadCells target="//dist/packages/HOL_ppc-darwin.tar.gz" title="HOL_ppc-darwin.tar.gz"?>
   11.66 +    <?downloadCells target="//dist/HOL_ppc-darwin.tar.gz" title="HOL_ppc-darwin.tar.gz"?>
   11.67    </tr>
   11.68    <tr>
   11.69      <td rowspan="3">
   11.70        HOL-Complex
   11.71      </td>
   11.72 -    <?downloadCells target="//dist/packages/HOL-Complex_x86-linux.tar.gz" title="HOL-Complex_x86-linux.tar.gz"?>
   11.73 +    <?downloadCells target="//dist/HOL-Complex_x86-linux.tar.gz" title="HOL-Complex_x86-linux.tar.gz"?>
   11.74    </tr>
   11.75    <tr>
   11.76      <td style="display: none"></td>
   11.77 -    <?downloadCells target="//dist/packages/HOL-Complex_sparc-solaris.tar.gz" title="HOL-Complex_sparc-solaris.tar.gz"?>
   11.78 +    <?downloadCells target="//dist/HOL-Complex_sparc-solaris.tar.gz" title="HOL-Complex_sparc-solaris.tar.gz"?>
   11.79    </tr>
   11.80    <tr>
   11.81      <td style="display: none"></td>
   11.82 -    <?downloadCells target="//dist/packages/HOL-Complex_ppc-darwin.tar.gz" title="HOL-Complex_ppc-darwin.tar.gz"?>
   11.83 +    <?downloadCells target="//dist/HOL-Complex_ppc-darwin.tar.gz" title="HOL-Complex_ppc-darwin.tar.gz"?>
   11.84    </tr>
   11.85    <tr>
   11.86      <td rowspan="3">
   11.87        HOL4
   11.88      </td>
   11.89 -    <?downloadCells target="//dist/packages/HOL4_x86-linux.tar.gz" title="HOL4_x86-linux.tar.gz"?>
   11.90 +    <?downloadCells target="//dist/HOL4_x86-linux.tar.gz" title="HOL4_x86-linux.tar.gz"?>
   11.91    </tr>
   11.92    <tr>
   11.93      <td style="display: none"></td>
   11.94 -    <?downloadCells target="//dist/packages/HOL4_sparc-solaris.tar.gz" title="HOL4_sparc-solaris.tar.gz"?>
   11.95 +    <?downloadCells target="//dist/HOL4_sparc-solaris.tar.gz" title="HOL4_sparc-solaris.tar.gz"?>
   11.96    </tr>
   11.97    <tr>
   11.98      <td style="display: none"></td>
   11.99 -    <?downloadCells target="//dist/packages/HOL4_ppc-darwin.tar.gz" title="HOL4_ppc-darwin.tar.gz"?>
  11.100 +    <?downloadCells target="//dist/HOL4_ppc-darwin.tar.gz" title="HOL4_ppc-darwin.tar.gz"?>
  11.101    </tr>
  11.102    <tr>
  11.103      <td rowspan="3">
  11.104        ZF
  11.105      </td>
  11.106 -    <?downloadCells target="//dist/packages/ZF_x86-linux.tar.gz" title="ZF_x86-linux.tar.gz"?>
  11.107 +    <?downloadCells target="//dist/ZF_x86-linux.tar.gz" title="ZF_x86-linux.tar.gz"?>
  11.108    </tr>
  11.109    <tr>
  11.110      <td style="display: none"></td>
  11.111 -    <?downloadCells target="//dist/packages/ZF_sparc-solaris.tar.gz" title="ZF_sparc-solaris.tar.gz"?>
  11.112 +    <?downloadCells target="//dist/ZF_sparc-solaris.tar.gz" title="ZF_sparc-solaris.tar.gz"?>
  11.113    </tr>
  11.114    <tr>
  11.115      <td style="display: none"></td>
  11.116 -    <?downloadCells target="//dist/packages/ZF_ppc-darwin.tar.gz" title="ZF_ppc-darwin.tar.gz"?>
  11.117 +    <?downloadCells target="//dist/ZF_ppc-darwin.tar.gz" title="ZF_ppc-darwin.tar.gz"?>
  11.118    </tr>
  11.119    <tr><td colspan="3" class="downloadheader">HOL4 proof terms</td></tr>
  11.120    <tr>
  11.121      <td>
  11.122        HOL4 proof terms
  11.123      </td>
  11.124 -    <?downloadCells target="//dist/packages/contrib/HOL4-proofs.tar.gz" title="HOL4-proofs.tar.gz"?>
  11.125 +    <?downloadCells target="//dist/contrib/HOL4-proofs.tar.gz" title="HOL4-proofs.tar.gz"?>
  11.126  </tr>
  11.127  </table>
    12.1 --- a/Admin/website/index.html	Tue Sep 27 14:41:41 2005 +0200
    12.2 +++ b/Admin/website/index.html	Tue Sep 27 15:30:37 2005 +0200
    12.3 @@ -56,7 +56,7 @@
    12.4  	      <li>Major internal reorganizations and performance improvements.</li>
    12.5  	      </ul>
    12.6  
    12.7 -<p><a href="//dist/packages/Isabelle/NEWS">[Cumulative NEWS]</a></p>
    12.8 +<p><a href="//dist/Isabelle/NEWS">[Cumulative NEWS]</a></p>
    12.9  
   12.10  <h2>Download</h2>
   12.11  
    13.1 --- a/Admin/website/installation.html	Tue Sep 27 14:41:41 2005 +0200
    13.2 +++ b/Admin/website/installation.html	Tue Sep 27 15:30:37 2005 +0200
    13.3 @@ -23,7 +23,7 @@
    13.4              ready-to-use binary packages for Linux/x86, MaxOS X /
    13.5              Darwin, and Solaris.  For other platforms, Isabelle logics
    13.6              need to be compiled separately (see also <a
    13.7 -            href="//dist/packages/Isabelle/INSTALL">INSTALL</a>).
    13.8 +            href="//dist/Isabelle/INSTALL">INSTALL</a>).
    13.9          </p>
   13.10          
   13.11          <p>
   13.12 @@ -76,10 +76,10 @@
   13.13              <li>Unpack the archives to an appropriate location, e.&nbsp;g.
   13.14                  <tt class="shellcmd">/usr/local</tt>:
   13.15                  <ul class="shellcmd">
   13.16 -		<li>tar -C /usr/local -xzf <?downloadLink target="//dist/packages/Isabelle2005.tar.gz"?></li>
   13.17 -                <li>tar -C /usr/local -xzf <?downloadLink target="//dist/packages/contrib/polyml_x86-linux.tar.gz"?></li>
   13.18 -                <li>tar -C /usr/local -xzf <?downloadLink target="//dist/packages/HOL_x86-linux.tar.gz"?></li>
   13.19 -                <li>tar -C /usr/local -xzf <?downloadLink target="//dist/packages/contrib/ProofGeneral.tar.gz"?></li>
   13.20 +		<li>tar -C /usr/local -xzf <?downloadLink target="//dist/Isabelle2005.tar.gz"?></li>
   13.21 +                <li>tar -C /usr/local -xzf <?downloadLink target="//dist/contrib/polyml_x86-linux.tar.gz"?></li>
   13.22 +                <li>tar -C /usr/local -xzf <?downloadLink target="//dist/HOL_x86-linux.tar.gz"?></li>
   13.23 +                <li>tar -C /usr/local -xzf <?downloadLink target="//dist/contrib/ProofGeneral.tar.gz"?></li>
   13.24                  </ul>
   13.25              </li>
   13.26  
   13.27 @@ -122,10 +122,10 @@
   13.28              <li>Unpack the archives to an appropriate location, e.&nbsp;g.
   13.29                  <tt class="shellcmd">/usr/local</tt>:
   13.30                  <ul class="shellcmd">
   13.31 -                    <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/packages/Isabelle2005.tar.gz"?></li>
   13.32 -                    <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/packages/contrib/ProofGeneral.tar.gz"?></li>
   13.33 -                    <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/packages/contrib/polyml_ppc-darwin.tar.gz"?></li>
   13.34 -                    <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/packages/HOL_ppc-darwin.tar.gz"?></li>
   13.35 +                    <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/Isabelle2005.tar.gz"?></li>
   13.36 +                    <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/contrib/ProofGeneral.tar.gz"?></li>
   13.37 +                    <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/contrib/polyml_ppc-darwin.tar.gz"?></li>
   13.38 +                    <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/HOL_ppc-darwin.tar.gz"?></li>
   13.39                  </ul>
   13.40              </li>
   13.41  
   13.42 @@ -155,10 +155,10 @@
   13.43              <li>Unpack the archives to an appropriate location, e.&nbsp;g.
   13.44                  <tt class="shellcmd">/usr/local</tt>:
   13.45                  <ul class="shellcmd">
   13.46 -                    <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/packages/Isabelle2005.tar.gz"?></li>
   13.47 -                    <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/packages/contrib/ProofGeneral.tar.gz"?></li>
   13.48 -                    <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/packages/contrib/polyml_sparc-solaris.tar.gz"?></li>
   13.49 -                    <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/packages/HOL_sparc-solaris.tar.gz"?></li>
   13.50 +                    <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/Isabelle2005.tar.gz"?></li>
   13.51 +                    <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/contrib/ProofGeneral.tar.gz"?></li>
   13.52 +                    <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/contrib/polyml_sparc-solaris.tar.gz"?></li>
   13.53 +                    <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/HOL_sparc-solaris.tar.gz"?></li>
   13.54                  </ul>
   13.55              </li>
   13.56  
    14.1 --- a/Admin/website/overview.html	Tue Sep 27 14:41:41 2005 +0200
    14.2 +++ b/Admin/website/overview.html	Tue Sep 27 15:30:37 2005 +0200
    14.3 @@ -37,7 +37,7 @@
    14.4        University of Munich, Germany).</p>
    14.5  
    14.6        <p>Isabelle is distributed <em>freely</em> as Open Source
    14.7 -      Software <!--a href="//dist/packages/Isabelle/COPYRIGHT"-->BSD
    14.8 +      Software <!--a href="//dist/Isabelle/COPYRIGHT"-->BSD
    14.9        license<!--/a-->; see the <a
   14.10        href="installation.html">installation instructions</a>.</p>
   14.11