--- a/Admin/website/installation_notes_cygwin.html Wed Jul 12 17:00:33 2006 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,211 +0,0 @@
-<?xml version='1.0' encoding='iso-8859-1' ?>
-<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
-<!-- $Id$ -->
-<html xmlns="http://www.w3.org/1999/xhtml">
-
-<head>
- <title>Installation notes for Windows/Cygwin</title>
- <?include file="//include/htmlheader.include.html"?>
-</head>
-
-<body class="dist">
- <?include file="//include/header.include.html"?>
- <div class="hr"><hr/></div>
- <?include file="//include/navigation.include.html"?>
- <div class="hr"><hr/></div>
-
- <div id="content">
-
- <h2>Preconditions and restrictions</h2>
-
- <p>Please notice before you go ahead:</p>
-
- <ul>
- <li>The ML system these notes apply to is <a href=
- "http://www.smlnj.org/">Standard ML of New Jersey</a>, which
- provides explicit Cygwin support. Poly/ML is not covered
- here.</li>
-
- <li>It is assumed you have some experience with an Unix
- operating system (e.g. what a shell is for and how to use
- it).</li>
- </ul>
-
- <p>Any suggestions and improvements concerning this hints are welcomed!</p>
-
- <h2>Acknowlegements</h2>
-
- <p>Thanks to <a href=
- "http://cswww.essex.ac.uk/Research/FSS/projects/isawin/">Norbert
- Völker</a> and <a href=
- "http://www.abo.fi/~viorel.preoteasa/isabelle/">Viorel Preoteasa</a> whose
- efforts helped a lot to get Isabelle run this way.</p>
-
- <h2>Installing Cygwin</h2>
-
- <p>Cygwin is a POSIX emulation layer for Windows; it contains ports of a
- large collection of common Unix software (shells, perl, gcc, X11, latex,
- ImageMagick, …).</p>
-
- <p>To install it, get the installer from the <a href=
- "http://www.cygwin.com">Cygwin website</a> and run it. It will ask you which
- packages to install, and then downloads and installs them. Please make sure
- you install everything needed by Isabelle; it is hard to give a concise list
- of packages here since the bundling of Cygwin packages may vary over time,
- but installing the base packages, perl, make, xemacs and x-server should be a
- good choice for the beginning.</p>
-
- <p>By default, cygwin installs to <tt class="shellcmd">c:\cygwin</tt>; you may choose an
- arbitrary location, but it is recommended that it does not include any space
- or exotic characters. This directory will then become the root directory of
- the Cygwin filesystem tree, i.e. the Cygwin path <tt class="shellcmd">/opt/smlnj</tt> will be
- mapped to Windows path <tt class="shellcmd">c:\cygwin\opt\smlnj</tt>.</p>
-
- <p>After installation, open a Cygwin shell window (normally the installer
- makes a shortcut for you).</p>
-
- <h2>Getting and building SML/NJ</h2>
-
- <p>Now we are ready to get and build <a href=
- "http://www.smlnj.org/">SML/NJ</a>; before this, set the environment variable
- SMLNJ_CYGWIN_RUNTIME to 1:</p>
-
- <ul class="shellcmd">
- <li>export SMLNJ_CYGWIN_RUNTIME=1</li>
- </ul>
-
- <p>This setting will tell the build process that it should
- <em>not</em> attempt to build SML/NJ natively for Win32 but for Cygwin
- instead (see further <a href=
- "http://smlnj.cs.uchicago.edu/dist/working/110.53/CYGWININSTALL">CYGWININSTALL</a>).</p>
-
- <p>So far, this setup was tested using the working version 110.53 of SML/NJ
- from <a href=
- "http://smlnj.cs.uchicago.edu/dist/working/110.53/">http://smlnj.cs.uchicago.edu/dist/working/110.53/</a>.
- SML/NJ provides a nice installer enabling you to download and build it. Read
- <a href=
- "http://smlnj.cs.uchicago.edu/dist/working/110.53/INSTALL">INSTALL</a> to
- learn about the different possibilites to do this. The default packages
- should be sufficient.</p>
-
- <p>In the following, it is assumed that you install SML/NJ to Cygwin path
- <tt class="shellcmd">/opt/smlnj</tt>; if you choose an other location, some tweaking in the
- <a href="#config"><tt class="shellcmd">etc/settings</tt> file</a> may be neccessary later.</p>
-
- <p>Whenever SMLNJ is used, the SMLNJ_CYGWIN_RUNTIME environment variable must
- be set to 1 (later on a convenient mechanism to make this the default is
- proposed).</p>
-
- <h2>Installing Isabelle</h2>
-
- <p><a href="download.html">Download</a> the latest Isabelle and
- ProofGeneral release packages. Assuming that you are in the
- directory where you downloaded the files, install them into <tt
- class="shellcmd">/opt</tt> by typing into the bash shell:</p>
-
- <ul class="shellcmd">
- <li>tar -C /usr/opt -xvzf <?value key="distname"?>.tar.gz</li>
- <li>tar -C /usr/opt -xvzf ProofGeneral.tar.gz</li>
- </ul>
-
- <p>The location <tt class="shellcmd">/opt</tt> again is just a proposal; if you choose other
- locations, some tweaking in the <a href="#config"><tt class="shellcmd">etc/settings</tt>
- file</a> may be neccessary later.</p>
-
- <h2 id="config">Configuring Isabelle</h2>
-
- <p>Edit the file <tt class="shellcmd">/opt/Isabelle/etc/settings</tt>; first, uncomment the
- lines about SMLNJ. Also set the variable SMLNJ_CYGWIN_RUNTIME to 1, in order
- the cygwin version of SMLNJ is used. As mentioned above, the path variables
- for the ML system and ProofGeneral may need adjustions, depending on your
- different installation locations.</p>
-
- <p>Take heed of the setting of ISABELLE_HOME_USER; by default, this is
- <tt class="shellcmd">~/isabelle</tt>. To detect which Windows path this will be mapped to,
- type into the Cygwin bash shell:</p>
-
- <ul class="shellcmd">
- <li>cygpath --windows ~/isabelle</li>
- </ul>
-
- <p>If you don't like this location to be the isabelle home
- directory, consider setting of ISABELLE_HOME_USER to another value; use
- <tt class="shellcmd">cygpath --unix <winpath></tt> to detect which Cygwin path a given
- Windows path is mapped to.</p>
-
- <p>A typical change could look like this:</p>
-
- <blockquote>
- from<br />
- <tt># Standard ML of New Jersey 110 or later<br />
- #ML_SYSTEM=smlnj-110<br />
- #ML_HOME="$ISABELLE_HOME/../smlnj/bin"<br />
- #ML_OPTIONS="@SMLdebug=/dev/null"<br />
- #ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo
- "$HEAP_SUFFIX")<br /></tt>
- </blockquote>
-
- <blockquote>
- to<br />
- <tt># Standard ML of New Jersey 110 or later<br />
- SMLNJ_CYGWIN_RUNTIME=1<br />
- ML_SYSTEM=smlnj-110<br />
- ML_HOME="$ISABELLE_HOME/../smlnj/bin"<br />
- ML_OPTIONS="@SMLdebug=/dev/null"<br />
- ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo
- "$HEAP_SUFFIX")</tt>
- </blockquote>
-
- <h2>Building logics</h2>
-
- <p>Now we can compile some logics. Start the cygwin shell (if not still
- running) and type:</p>
-
- <ul class="shellcmd">
- <li>cd /opt/Isabelle</li>
- <li>build FOL</li>
- <li>build ZF</li>
- <li>build HOL</li>
- </ul>
-
- <p>The compilation process may take some time (depending on how fast the
- computer is). Before building a logic image the build program shows some
- variables and expects user input – just hit enter.</p>
-
- <h2>Running Isabelle with ProofGeneral</h2>
-
- <p>Now everything should be ready. To test, start the cygwin shell and
- type</p>
-
- <ul class="shellcmd">
- <li>startx &</li>
- </ul>
-
- <p>This will start the cygwin X server and an X shell window. In
- the X shell window, type</p>
-
- <ul class="shellcmd">
- <li>/opt/Isabelle/bin/Isabelle &</li>.
- </ul>
-
- <p>This will start the ProofGeneral interface for Isabelle. After a
- while an empty buffer <tt>Scratch.thy</tt> is created. You can turn on
- X-Symbol from the menu Proof-General, item Options.</p>
-
- <p>Load one of your favorite theories and test your Isabelle installation by
- proving something.</p>
-
- <p>To simplify starting ProofGeneral, consider writing a Windows command
- script, e. g.</p>
-
- <blockquote>
- <tt>@bash startx -geometry 30x4 -iconic -e Isabelle</tt>
- </blockquote>
-
- <p>and assigning a shortcut in the start menu to it.</p>
- </div>
- <div class="hr"><hr/></div>
- <?include file="//include/footer.include.html"?>
-</body>
-
-</html>