Admin/website/installation_notes_cygwin.html
changeset 16674 bf2cd93cc245
child 17563 abb280dd3431
equal deleted inserted replaced
16673:6b14aba5ddaa 16674:bf2cd93cc245
       
     1 <?xml version='1.0' encoding='iso-8859-1' ?>
       
     2 <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
       
     3 <!-- $Id$ -->
       
     4 <html xmlns="http://www.w3.org/1999/xhtml">
       
     5 
       
     6 <head>
       
     7     <title>Installation notes for Windows/Cygwin</title>
       
     8     <?include file="//include/htmlheader.include.html"?>
       
     9 </head>
       
    10 
       
    11 <body class="dist">
       
    12     <?include file="//include/header.include.html"?>
       
    13     <div class="hr"><hr/></div>
       
    14     <?include file="//include/navigation.include.html"?>
       
    15     <div class="hr"><hr/></div>
       
    16 
       
    17     <div id="content">
       
    18 
       
    19       <h2>Preconditions and restrictions</h2>
       
    20     
       
    21       <p>Please notice before you go ahead:</p>
       
    22     
       
    23       <ul>
       
    24         <li>The ML system these notes apply to is <a href=
       
    25         "http://www.smlnj.org/">Standard ML of New Jersey</a>; it is <em>not</em>
       
    26         known yet how to get Isabelle run completely with <a href=
       
    27         "www.polyml.org/">Poly/ML</a>. See <a href="#polyml">a note on Poly/ML</a>
       
    28         down this page.</li>
       
    29     
       
    30         <li>It is assumed you have some experience with an Unix operating system
       
    31         (e.g. what a shell is for and how to use it).</li>
       
    32       </ul>
       
    33 
       
    34       <p>Any suggestions and improvements concerning this hints are welcomed!</p>
       
    35 
       
    36       <h2>Acknowlegements</h2>
       
    37     
       
    38       <p>Thanks to <a href=
       
    39       "http://cswww.essex.ac.uk/Research/FSS/projects/isawin/">Norbert
       
    40       Völker</a> and <a href=
       
    41       "http://www.abo.fi/~viorel.preoteasa/isabelle/">Viorel Preoteasa</a> whose
       
    42       efforts helped a lot to get Isabelle run this way.</p>
       
    43     
       
    44       <h2>Installing Cygwin</h2>
       
    45     
       
    46       <p>Cygwin is a POSIX emulation layer for Windows; it contains ports of a
       
    47       large collection of common Unix software (shells, perl, gcc, X11, latex,
       
    48       ImageMagick, &hellip;).</p>
       
    49     
       
    50       <p>To install it, get the installer from the <a href=
       
    51       "http://www.cygwin.com">Cygwin website</a> and run it. It will ask you which
       
    52       packages to install, and then downloads and installs them. Please make sure
       
    53       you install everything needed by Isabelle; it is hard to give a concise list
       
    54       of packages here since the bundling of Cygwin packages may vary over time,
       
    55       but installing the base packages, perl, make, xemacs and x-server should be a
       
    56       good choice for the beginning.</p>
       
    57     
       
    58       <p>By default, cygwin installs to <tt class="shellcmd">c:\cygwin</tt>; you may choose an
       
    59       arbitrary location, but it is recommended that it does not include any space
       
    60       or exotic characters. This directory will then become the root directory of
       
    61       the Cygwin filesystem tree, i.e. the Cygwin path <tt class="shellcmd">/opt/smlnj</tt> will be
       
    62       mapped to Windows path <tt class="shellcmd">c:\cygwin\opt\smlnj</tt>.</p>
       
    63     
       
    64       <p>After installation, open a Cygwin shell window (normally the installer
       
    65       makes a shortcut for you).</p>
       
    66     
       
    67       <h2>Getting and building SML/NJ</h2>
       
    68     
       
    69       <p>Now we are ready to get and build <a href=
       
    70       "http://www.smlnj.org/">SML/NJ</a>; before this, set the environment variable
       
    71       SMLNJ_CYGWIN_RUNTIME to 1:</p>
       
    72     
       
    73       <ul class="shellcmd">
       
    74         <li>export SMLNJ_CYGWIN_RUNTIME=1</li>
       
    75       </ul>
       
    76     
       
    77       <p>This setting will tell the build process that it should
       
    78       <em>not</em> attempt to build SML/NJ natively for Win32 but for Cygwin
       
    79       instead (see further <a href=
       
    80       "http://smlnj.cs.uchicago.edu/dist/working/110.53/CYGWININSTALL">CYGWININSTALL</a>).</p>
       
    81     
       
    82       <p>So far, this setup was tested using the working version 110.53 of SML/NJ
       
    83       from <a href=
       
    84       "http://smlnj.cs.uchicago.edu/dist/working/110.53/">http://smlnj.cs.uchicago.edu/dist/working/110.53/</a>.
       
    85       SML/NJ provides a nice installer enabling you to download and build it. Read
       
    86       <a href=
       
    87       "http://smlnj.cs.uchicago.edu/dist/working/110.53/INSTALL">INSTALL</a> to
       
    88       learn about the different possibilites to do this. The default packages
       
    89       should be sufficient.</p>
       
    90     
       
    91       <p>In the following, it is assumed that you install SML/NJ to Cygwin path
       
    92       <tt class="shellcmd">/opt/smlnj</tt>; if you choose an other location, some tweaking in the
       
    93       <a href="#config"><tt class="shellcmd">etc/settings</tt> file</a> may be neccessary later.</p>
       
    94     
       
    95       <p>Whenever SMLNJ is used, the SMLNJ_CYGWIN_RUNTIME environment variable must
       
    96       be set to 1 (later on a convenient mechanism to make this the default is
       
    97       proposed).</p>
       
    98     
       
    99       <h2>Installing Isabelle</h2>
       
   100     
       
   101       <p>Download the latest Isabelle and ProofGeneral <a href=
       
   102       "download.html">release packages</a>. Assuming that you are in the directory
       
   103       where you downloaded the files, install them into <tt class="shellcmd">/opt</tt> by typing
       
   104       into the bash shell:</p>
       
   105     
       
   106       <ul class="shellcmd">
       
   107         <li>tar -C /usr/opt -xvzf <?value key="distname"?>.tar.gz</li>
       
   108         <li>tar -C /usr/opt -xvzf ProofGeneral.tar.gz</li>
       
   109       </ul>
       
   110       
       
   111       <p>During extraction, one inconvenience may occur, see <a href=
       
   112       "#inconvenience">below</a>.</p>
       
   113     
       
   114       <p>The location <tt class="shellcmd">/opt</tt> again is just a proposal; if you choose other
       
   115       locations, some tweaking in the <a href="#config"><tt class="shellcmd">etc/settings</tt>
       
   116       file</a> may be neccessary later.</p>
       
   117     
       
   118       <h2 id="config">Configuring Isabelle</h2>
       
   119     
       
   120       <p>Edit the file <tt class="shellcmd">/opt/Isabelle/etc/settings</tt>; first, uncomment the
       
   121       lines about SMLNJ. Also set the variable SMLNJ_CYGWIN_RUNTIME to 1, in order
       
   122       the cygwin version of SMLNJ is used. As mentioned above, the path variables
       
   123       for the ML system and ProofGeneral may need adjustions, depending on your
       
   124       different installation locations.</p>
       
   125     
       
   126       <p>Take heed of the setting of ISABELLE_HOME_USER; by default, this is
       
   127       <tt class="shellcmd">~/isabelle</tt>. To detect which Windows path this will be mapped to,
       
   128       type into the Cygwin bash shell:</p>
       
   129     
       
   130       <ul class="shellcmd">
       
   131         <li>cygpath --windows ~/isabelle</li>
       
   132       </ul>
       
   133       
       
   134       <p>If you don't like this location to be the isabelle home
       
   135       directory, consider setting of ISABELLE_HOME_USER to another value; use
       
   136       <tt class="shellcmd">cygpath --unix &lt;winpath&gt;</tt> to detect which Cygwin path a given
       
   137       Windows path is mapped to.</p>
       
   138     
       
   139       <p>A typical change could look like this:</p>
       
   140     
       
   141       <blockquote>
       
   142         from<br />
       
   143         <tt># Standard ML of New Jersey 110 or later<br />
       
   144         #ML_SYSTEM=smlnj-110<br />
       
   145         #ML_HOME="$ISABELLE_HOME/../smlnj/bin"<br />
       
   146         #ML_OPTIONS="@SMLdebug=/dev/null"<br />
       
   147         #ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2&gt;/dev/null); echo
       
   148         "$HEAP_SUFFIX")<br /></tt>
       
   149       </blockquote>
       
   150     
       
   151       <blockquote>
       
   152         to<br />
       
   153         <tt># Standard ML of New Jersey 110 or later<br />
       
   154         SMLNJ_CYGWIN_RUNTIME=1<br />
       
   155         ML_SYSTEM=smlnj-110<br />
       
   156         ML_HOME="$ISABELLE_HOME/../smlnj/bin"<br />
       
   157         ML_OPTIONS="@SMLdebug=/dev/null"<br />
       
   158         ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2&gt;/dev/null); echo
       
   159         "$HEAP_SUFFIX")</tt>
       
   160       </blockquote>
       
   161 
       
   162       <h2>Building logics</h2>
       
   163     
       
   164       <p>Now we can compile some logics. Start the cygwin shell (if not still
       
   165       running) and type:</p>
       
   166     
       
   167       <ul class="shellcmd">
       
   168         <li>cd /opt/Isabelle</li>
       
   169         <li>build HOL</li>
       
   170         <li>build ZF</li>
       
   171       </ul>
       
   172 
       
   173       <p>The compilation process may take some time (depending on how fast the
       
   174       computer is). Before building a logic image the build program shows some
       
   175       variables and expects user input &ndash; just hit enter.</p>
       
   176     
       
   177       <h2>Running Isabelle with ProofGeneral</h2>
       
   178     
       
   179       <p>On Linux, Isabelle can be started by two scripts located in
       
   180       <tt class="shellcmd">Isabelle/bin</tt>: <tt class="shellcmd">Isabelle</tt> and <tt class="shellcmd">isabelle</tt>.
       
   181       <tt class="shellcmd">Isabelle</tt> attempts to start ProofGeneral with XEmacs, and isabelle
       
   182       starts it in an SML shell session. However Windows treats the two names as
       
   183       one. To get around this, just rename <tt class="shellcmd">/opt/Isabelle/bin/isabelle</tt> to
       
   184       <tt class="shellcmd">/opt/Isabelle/bin/Isabelle</tt>. This script
       
   185       will start Isabelle with ProofGeneral; the <tt class="shellcmd">isabelle</tt>
       
   186       script in any case is available as <tt class="shellcmd">isabelle-process</tt>.</p>
       
   187     
       
   188       <p>Now everything should be ready. To test, start the cygwin shell and
       
   189       type</p>
       
   190     
       
   191       <ul class="shellcmd">
       
   192         <li>startx &amp;</li>
       
   193       </ul>
       
   194       
       
   195       <p>This will start the cygwin X server and an X shell window. In
       
   196       the X shell window, type</p>
       
   197     
       
   198       <ul class="shellcmd">
       
   199         <li>/opt/Isabelle/bin/Isabelle &amp;</li>.
       
   200       </ul>
       
   201       
       
   202       <p>This will start the ProofGeneral interface for Isabelle. After a
       
   203       while an empty buffer <tt>Scratch.thy</tt> is created. You can turn on
       
   204       X-Symbol from the menu Proof-General, item Options.</p>
       
   205     
       
   206       <p>Load one of your favorite theories and test your Isabelle installation by
       
   207       proving something.</p>
       
   208     
       
   209       <p>To simplify starting ProofGeneral, consider writing a Windows command
       
   210       script, e.&nbsp;g.</p>
       
   211     
       
   212       <blockquote>
       
   213         <tt>@bash startx -geometry 30x4 -iconic -e Isabell</tt>
       
   214       </blockquote>
       
   215       
       
   216       <p>and assigning a shortcut in the start menu to it.</p>
       
   217     
       
   218       <h2 id="inconvenience">Inconveniencies with the current version of
       
   219       Isabelle</h2>
       
   220     
       
   221       <p>With the current Isabelle release (Isabelle 2004), there are two
       
   222       inconveniencies:</p>
       
   223     
       
   224       <ul>
       
   225         <li>During extraction you will get a warning that file
       
   226         <tt class="shellcmd">Real/HahnBanach/Aux.thy</tt> can not be created. This is because
       
   227         <tt class="shellcmd">Aux</tt> is not allowed as a filename under Windows. If you do not want
       
   228         to run the HahnBanach example, you might simply want to ignore this
       
   229         warning.</li>
       
   230     
       
   231         <li>The tool <tt class="shellcmd">isatool mkdir</tt> tries to detect the name of the current
       
   232         user, to put it into the generated <tt class="shellcmd">root.tex</tt>. Alas, on Windows,
       
   233         this leads to an unquoted <tt>\</tt> in the TeX file. So you either must
       
   234         edit your <tt class="shellcmd">root.tex</tt> manually to fix this, or directly patch
       
   235         <tt class="shellcmd">/opt/Isabelle/lib/Tools/mkdir</tt> by replacing
       
   236     
       
   237           <blockquote>
       
   238             <tt>AUTHOR=$("$AUTO_PERL" -e "@pw = getpwnam(\"$USER\"); print @pw[6]" | tr _ -)</tt>
       
   239           </blockquote>with
       
   240     
       
   241           <blockquote>
       
   242             <tt>AUTHOR="default author name"</tt>
       
   243           </blockquote>
       
   244         </li>
       
   245       </ul>
       
   246     
       
   247       <p>To get around these inconveniencies, consider using a recent developer
       
   248       snapshot of Isabelle; both will be fixed in the next Isabelle release.</p>
       
   249     
       
   250       <h2 id="polyml">A note on Poly/ML</h2>
       
   251     
       
   252       <p>As indicated above, Isabelle does <em>not</em> run neatly with <a href=
       
   253       "http://www.polyml.org/">Poly/ML</a> on Windows, since it is not clear
       
   254       how Poly/ML has to be compiled for Cygwin, and the native Windows port
       
   255       of PolyML does not provide some Posix signals Isabelle/ProofGeneral relies on.</p>
       
   256     
       
   257       <p>If you know how to circumvent (fully or partially) any of these problems,
       
   258       please let us know.</p>
       
   259 
       
   260     </div>
       
   261     <div class="hr"><hr/></div>
       
   262     <?include file="//include/footer.include.html"?>
       
   263 </body>
       
   264 
       
   265 </html>