# HG changeset patch # User wenzelm # Date 969980848 -7200 # Node ID a9704bf900312f292fe94d0f3f7db51a83dda445 # Parent ede64d0782e5aaf012637dc7530357f1c7d0f53c simplified; got rid of rpm; diff -r ede64d0782e5 -r a9704bf90031 Admin/page/common/functions.pl --- a/Admin/page/common/functions.pl Tue Sep 26 17:06:16 2000 +0200 +++ b/Admin/page/common/functions.pl Tue Sep 26 17:07:28 2000 +0200 @@ -14,6 +14,7 @@ if (defined(&setnavcolor)) { undef &setnavcolor; } if (defined(&twodig)) { undef &twodig; } if (defined(&setdowncolor)) { undef &setdowncolor; } + if (defined(&downloadhead)) { undef &downloadhead; } if (defined(&download)) { undef &download; } --> @@ -92,9 +93,9 @@ return $retval; } - # size(filename) sub size { my $filename = $_[0]; + my @s = stat $filename; my $size = defined $s[7] ? $s[7]/1024 : 0; @@ -106,12 +107,19 @@ return ""; } - # download(description, url, prefix) - sub download { + sub downloadhead { + my $text = $_[0]; - my $descr = $_[0]; - my $url = $_[1]; - my $prefix = $_[2]; + return <$text +EOF + } + + sub download { + my $rowspan = $_[0]; + my $descr = $_[1]; + my $url = $_[2]; + my $prefix = $_[3]; my $size = size("$prefix/$url"); $size = "$size K"; @@ -124,11 +132,17 @@ my $td = "nowrap bgcolor=$downcolor"; - my $retval = < - + my $descr_text = ""; + if ($descr ne "") { + $descr_text = <   $descr +EOF + } + + my $retval = <$descr_text   $filename diff -r ede64d0782e5 -r a9704bf90031 Admin/page/dist-content/packages.content --- a/Admin/page/dist-content/packages.content Tue Sep 26 17:06:16 2000 +0200 +++ b/Admin/page/dist-content/packages.content Tue Sep 26 17:07:28 2000 +0200 @@ -16,109 +16,105 @@ suitable implementation of Standard ML (e.g. Poly/ML as provided below). A comfortable Isabelle working environment demands further user interface support, as provided by Proof General -together with the (optional) Proof General together with the +(optional) X-Symbol package. Both of these should be used with a recent version of XEmacs (e.g. version 21.1). +href="http://www.xemacs.org">XEmacs-21.

-We provide ready-to-go packages for Isabelle, Proof General and + +

Packages

+ +We provide a complete set of packages for Isabelle, Proof General and X-Symbol. While XEmacs-21 is not included here, most operating system -distributions already provide suitable packages, although not +distributions already provide a suitable package, although not installed by default.

-Following the example installation procedures below, there is -no separate configuration required of any of these -components. After installation, users may invoke the Isabelle -executables without further ado. - -

- - -

(1) Linux/x86 systems with RPM

- -This version of the distribution is for generic -Linux/x86 systems with RPM package management, as used by most Linux -distributions. Note that rpm requires root user access for -installation. +Some packages are platform dependent. Everything is included below +for Linux/x86 and Solaris/Sparc systems. Other Unix platforms work as +well, but require manual compilation of Isabelle logic images using a +suitable Standard ML system.

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

-Example installation procedure (the location of --prefix -/usr/share may be changed): +

Installation

-
-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
-rpm -i --prefix /usr/share xsymbol.rpm
-
- -Note that installed RPMs may be removed like this: - -
-rpm -e xsymbol proofgeneral isabelle-HOL isabelle polyml
-
+Installation is very easy. Basically, just unpack all required +packages within the same directory. There is no manual +configuration required of any of these components, if used according +the default settings of Isabelle.

- -

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

- -The following distribution works for any -Linux/x86 or Solaris/Sparc system. Installation does not rely on -package management at all. +A typical Linux/x86 site installation of Isabelle/HOL works as follows +(the location /usr/local may be changed):

- -

- - - - - - - -
-
+ +   tar -C /usr/local -xzf +
+   tar -C /usr/local -xzf +
+   tar -C /usr/local -xzf +
+   tar -C /usr/local -xzf +
+   tar -C /usr/local -xzf +
+   tar -C /usr/local -xzf +
+

-Example installation in /usr/local for Linux/x86: - -

-tar -C /usr/local -x -z -f polyml_base.tar.gz
-tar -C /usr/local -x -z -f polyml_x86-linux.tar.gz
-tar -C /usr/local -x -z -f 
-tar -C /usr/local -x -z -f ProofGeneral.tar.gz
-tar -C /usr/local -x -z -f x-symbol.tar.gz
-
-cd 
-./configure
-./build
-./bin/isatool install -p /usr/local/bin
-
+The installation may be finished as follows:

+ + +  
+   ./configure
+   ./bin/isatool install -p /usr/local/bin
+
+ +

+ +Users can now invoke the Isabelle executables without further ado. + +