pruned notes about Poly/ML;
authorwenzelm
Fri Sep 30 15:28:43 2005 +0200 (2005-09-30)
changeset 17734fb2fd74358e1
parent 17733 25ffdae37db1
child 17735 e6948d8f5f73
pruned notes about Poly/ML;
removed unnecessary rename of Isabelle executable;
Admin/website/installation_notes_cygwin.html
     1.1 --- a/Admin/website/installation_notes_cygwin.html	Fri Sep 30 15:17:04 2005 +0200
     1.2 +++ b/Admin/website/installation_notes_cygwin.html	Fri Sep 30 15:28:43 2005 +0200
     1.3 @@ -22,13 +22,13 @@
     1.4      
     1.5        <ul>
     1.6          <li>The ML system these notes apply to is <a href=
     1.7 -        "http://www.smlnj.org/">Standard ML of New Jersey</a>; it is <em>not</em>
     1.8 -        known yet how to get Isabelle run completely with <a href=
     1.9 -        "http://www.polyml.org/">Poly/ML</a>. See <a href="#polyml">a note on Poly/ML</a>
    1.10 -        down this page.</li>
    1.11 +        "http://www.smlnj.org/">Standard ML of New Jersey</a>, which
    1.12 +        provides explicit Cygwin support.  Poly/ML is not covered
    1.13 +        here.</li>
    1.14      
    1.15 -        <li>It is assumed you have some experience with an Unix operating system
    1.16 -        (e.g. what a shell is for and how to use it).</li>
    1.17 +        <li>It is assumed you have some experience with an Unix
    1.18 +        operating system (e.g. what a shell is for and how to use
    1.19 +        it).</li>
    1.20        </ul>
    1.21  
    1.22        <p>Any suggestions and improvements concerning this hints are welcomed!</p>
    1.23 @@ -174,15 +174,6 @@
    1.24      
    1.25        <h2>Running Isabelle with ProofGeneral</h2>
    1.26      
    1.27 -      <p>On Linux, Isabelle can be started by two scripts located in
    1.28 -      <tt class="shellcmd">Isabelle/bin</tt>: <tt class="shellcmd">Isabelle</tt> and <tt class="shellcmd">isabelle</tt>.
    1.29 -      <tt class="shellcmd">Isabelle</tt> attempts to start ProofGeneral with XEmacs, and isabelle
    1.30 -      starts it in an SML shell session. However Windows treats the two names as
    1.31 -      one. To get around this, just rename <tt class="shellcmd">/opt/Isabelle/bin/isabelle</tt> to
    1.32 -      <tt class="shellcmd">/opt/Isabelle/bin/Isabelle</tt>. This script
    1.33 -      will start Isabelle with ProofGeneral; the <tt class="shellcmd">isabelle</tt>
    1.34 -      script in any case is available as <tt class="shellcmd">isabelle-process</tt>.</p>
    1.35 -    
    1.36        <p>Now everything should be ready. To test, start the cygwin shell and
    1.37        type</p>
    1.38      
    1.39 @@ -212,17 +203,6 @@
    1.40        </blockquote>
    1.41        
    1.42        <p>and assigning a shortcut in the start menu to it.</p>
    1.43 -    
    1.44 -      <h2 id="polyml">A note on Poly/ML</h2>
    1.45 -    
    1.46 -      <p>As indicated above, Isabelle does <em>not</em> run neatly with <a href=
    1.47 -      "http://www.polyml.org/">Poly/ML</a> on Windows, since it is not clear
    1.48 -      how Poly/ML has to be compiled for Cygwin, and the native Windows port
    1.49 -      of PolyML does not provide some Posix signals Isabelle/ProofGeneral relies on.</p>
    1.50 -    
    1.51 -      <p>If you know how to circumvent (fully or partially) any of these problems,
    1.52 -      please let us know.</p>
    1.53 -
    1.54      </div>
    1.55      <div class="hr"><hr/></div>
    1.56      <?include file="//include/footer.include.html"?>