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