Admin/website/installation_notes_cygwin.html
changeset 16674 bf2cd93cc245
child 17563 abb280dd3431
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/website/installation_notes_cygwin.html	Mon Jul 04 15:15:55 2005 +0200
@@ -0,0 +1,265 @@
+<?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>; it is <em>not</em>
+        known yet how to get Isabelle run completely with <a href=
+        "www.polyml.org/">Poly/ML</a>. See <a href="#polyml">a note on Poly/ML</a>
+        down this page.</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, &hellip;).</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>Download the latest Isabelle and ProofGeneral <a href=
+      "download.html">release packages</a>. 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>During extraction, one inconvenience may occur, see <a href=
+      "#inconvenience">below</a>.</p>
+    
+      <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 &lt;winpath&gt;</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&gt;/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&gt;/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 HOL</li>
+        <li>build ZF</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 &ndash; just hit enter.</p>
+    
+      <h2>Running Isabelle with ProofGeneral</h2>
+    
+      <p>On Linux, Isabelle can be started by two scripts located in
+      <tt class="shellcmd">Isabelle/bin</tt>: <tt class="shellcmd">Isabelle</tt> and <tt class="shellcmd">isabelle</tt>.
+      <tt class="shellcmd">Isabelle</tt> attempts to start ProofGeneral with XEmacs, and isabelle
+      starts it in an SML shell session. However Windows treats the two names as
+      one. To get around this, just rename <tt class="shellcmd">/opt/Isabelle/bin/isabelle</tt> to
+      <tt class="shellcmd">/opt/Isabelle/bin/Isabelle</tt>. This script
+      will start Isabelle with ProofGeneral; the <tt class="shellcmd">isabelle</tt>
+      script in any case is available as <tt class="shellcmd">isabelle-process</tt>.</p>
+    
+      <p>Now everything should be ready. To test, start the cygwin shell and
+      type</p>
+    
+      <ul class="shellcmd">
+        <li>startx &amp;</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 &amp;</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.&nbsp;g.</p>
+    
+      <blockquote>
+        <tt>@bash startx -geometry 30x4 -iconic -e Isabell</tt>
+      </blockquote>
+      
+      <p>and assigning a shortcut in the start menu to it.</p>
+    
+      <h2 id="inconvenience">Inconveniencies with the current version of
+      Isabelle</h2>
+    
+      <p>With the current Isabelle release (Isabelle 2004), there are two
+      inconveniencies:</p>
+    
+      <ul>
+        <li>During extraction you will get a warning that file
+        <tt class="shellcmd">Real/HahnBanach/Aux.thy</tt> can not be created. This is because
+        <tt class="shellcmd">Aux</tt> is not allowed as a filename under Windows. If you do not want
+        to run the HahnBanach example, you might simply want to ignore this
+        warning.</li>
+    
+        <li>The tool <tt class="shellcmd">isatool mkdir</tt> tries to detect the name of the current
+        user, to put it into the generated <tt class="shellcmd">root.tex</tt>. Alas, on Windows,
+        this leads to an unquoted <tt>\</tt> in the TeX file. So you either must
+        edit your <tt class="shellcmd">root.tex</tt> manually to fix this, or directly patch
+        <tt class="shellcmd">/opt/Isabelle/lib/Tools/mkdir</tt> by replacing
+    
+          <blockquote>
+            <tt>AUTHOR=$("$AUTO_PERL" -e "@pw = getpwnam(\"$USER\"); print @pw[6]" | tr _ -)</tt>
+          </blockquote>with
+    
+          <blockquote>
+            <tt>AUTHOR="default author name"</tt>
+          </blockquote>
+        </li>
+      </ul>
+    
+      <p>To get around these inconveniencies, consider using a recent developer
+      snapshot of Isabelle; both will be fixed in the next Isabelle release.</p>
+    
+      <h2 id="polyml">A note on Poly/ML</h2>
+    
+      <p>As indicated above, Isabelle does <em>not</em> run neatly with <a href=
+      "http://www.polyml.org/">Poly/ML</a> on Windows, since it is not clear
+      how Poly/ML has to be compiled for Cygwin, and the native Windows port
+      of PolyML does not provide some Posix signals Isabelle/ProofGeneral relies on.</p>
+    
+      <p>If you know how to circumvent (fully or partially) any of these problems,
+      please let us know.</p>
+
+    </div>
+    <div class="hr"><hr/></div>
+    <?include file="//include/footer.include.html"?>
+</body>
+
+</html>