Admin/website/installation_notes_cygwin.html
author wenzelm
Fri, 30 Sep 2005 15:28:43 +0200
changeset 17734 fb2fd74358e1
parent 17683 d7f78036546b
child 17780 274eaa114c6d
permissions -rw-r--r--
pruned notes about Poly/ML; removed unnecessary rename of Isabelle executable;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
16674
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
     1
<?xml version='1.0' encoding='iso-8859-1' ?>
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
     2
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
     3
<!-- $Id$ -->
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
     4
<html xmlns="http://www.w3.org/1999/xhtml">
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
     5
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
     6
<head>
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
     7
    <title>Installation notes for Windows/Cygwin</title>
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
     8
    <?include file="//include/htmlheader.include.html"?>
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
     9
</head>
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    10
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    11
<body class="dist">
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    12
    <?include file="//include/header.include.html"?>
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    13
    <div class="hr"><hr/></div>
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    14
    <?include file="//include/navigation.include.html"?>
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    15
    <div class="hr"><hr/></div>
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    16
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    17
    <div id="content">
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    18
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    19
      <h2>Preconditions and restrictions</h2>
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    20
    
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    21
      <p>Please notice before you go ahead:</p>
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    22
    
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    23
      <ul>
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    24
        <li>The ML system these notes apply to is <a href=
17734
fb2fd74358e1 pruned notes about Poly/ML;
wenzelm
parents: 17683
diff changeset
    25
        "http://www.smlnj.org/">Standard ML of New Jersey</a>, which
fb2fd74358e1 pruned notes about Poly/ML;
wenzelm
parents: 17683
diff changeset
    26
        provides explicit Cygwin support.  Poly/ML is not covered
fb2fd74358e1 pruned notes about Poly/ML;
wenzelm
parents: 17683
diff changeset
    27
        here.</li>
16674
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    28
    
17734
fb2fd74358e1 pruned notes about Poly/ML;
wenzelm
parents: 17683
diff changeset
    29
        <li>It is assumed you have some experience with an Unix
fb2fd74358e1 pruned notes about Poly/ML;
wenzelm
parents: 17683
diff changeset
    30
        operating system (e.g. what a shell is for and how to use
fb2fd74358e1 pruned notes about Poly/ML;
wenzelm
parents: 17683
diff changeset
    31
        it).</li>
16674
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    32
      </ul>
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    33
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    34
      <p>Any suggestions and improvements concerning this hints are welcomed!</p>
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    35
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    36
      <h2>Acknowlegements</h2>
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    37
    
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    38
      <p>Thanks to <a href=
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    39
      "http://cswww.essex.ac.uk/Research/FSS/projects/isawin/">Norbert
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    40
      Völker</a> and <a href=
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    41
      "http://www.abo.fi/~viorel.preoteasa/isabelle/">Viorel Preoteasa</a> whose
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    42
      efforts helped a lot to get Isabelle run this way.</p>
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    43
    
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    44
      <h2>Installing Cygwin</h2>
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    45
    
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    46
      <p>Cygwin is a POSIX emulation layer for Windows; it contains ports of a
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    47
      large collection of common Unix software (shells, perl, gcc, X11, latex,
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    48
      ImageMagick, &hellip;).</p>
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    49
    
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    50
      <p>To install it, get the installer from the <a href=
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    51
      "http://www.cygwin.com">Cygwin website</a> and run it. It will ask you which
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    52
      packages to install, and then downloads and installs them. Please make sure
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    53
      you install everything needed by Isabelle; it is hard to give a concise list
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    54
      of packages here since the bundling of Cygwin packages may vary over time,
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    55
      but installing the base packages, perl, make, xemacs and x-server should be a
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    56
      good choice for the beginning.</p>
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    57
    
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    58
      <p>By default, cygwin installs to <tt class="shellcmd">c:\cygwin</tt>; you may choose an
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    59
      arbitrary location, but it is recommended that it does not include any space
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    60
      or exotic characters. This directory will then become the root directory of
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    61
      the Cygwin filesystem tree, i.e. the Cygwin path <tt class="shellcmd">/opt/smlnj</tt> will be
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    62
      mapped to Windows path <tt class="shellcmd">c:\cygwin\opt\smlnj</tt>.</p>
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    63
    
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    64
      <p>After installation, open a Cygwin shell window (normally the installer
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    65
      makes a shortcut for you).</p>
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    66
    
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    67
      <h2>Getting and building SML/NJ</h2>
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    68
    
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    69
      <p>Now we are ready to get and build <a href=
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    70
      "http://www.smlnj.org/">SML/NJ</a>; before this, set the environment variable
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    71
      SMLNJ_CYGWIN_RUNTIME to 1:</p>
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    72
    
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    73
      <ul class="shellcmd">
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    74
        <li>export SMLNJ_CYGWIN_RUNTIME=1</li>
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    75
      </ul>
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    76
    
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    77
      <p>This setting will tell the build process that it should
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    78
      <em>not</em> attempt to build SML/NJ natively for Win32 but for Cygwin
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    79
      instead (see further <a href=
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    80
      "http://smlnj.cs.uchicago.edu/dist/working/110.53/CYGWININSTALL">CYGWININSTALL</a>).</p>
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    81
    
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    82
      <p>So far, this setup was tested using the working version 110.53 of SML/NJ
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    83
      from <a href=
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    84
      "http://smlnj.cs.uchicago.edu/dist/working/110.53/">http://smlnj.cs.uchicago.edu/dist/working/110.53/</a>.
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    85
      SML/NJ provides a nice installer enabling you to download and build it. Read
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    86
      <a href=
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    87
      "http://smlnj.cs.uchicago.edu/dist/working/110.53/INSTALL">INSTALL</a> to
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    88
      learn about the different possibilites to do this. The default packages
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    89
      should be sufficient.</p>
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    90
    
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    91
      <p>In the following, it is assumed that you install SML/NJ to Cygwin path
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    92
      <tt class="shellcmd">/opt/smlnj</tt>; if you choose an other location, some tweaking in the
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    93
      <a href="#config"><tt class="shellcmd">etc/settings</tt> file</a> may be neccessary later.</p>
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    94
    
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    95
      <p>Whenever SMLNJ is used, the SMLNJ_CYGWIN_RUNTIME environment variable must
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    96
      be set to 1 (later on a convenient mechanism to make this the default is
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    97
      proposed).</p>
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    98
    
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
    99
      <h2>Installing Isabelle</h2>
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   100
    
17683
d7f78036546b renamed "Packages" to "Download";
wenzelm
parents: 17676
diff changeset
   101
      <p><a href="download.html">Download</a> the latest Isabelle and
d7f78036546b renamed "Packages" to "Download";
wenzelm
parents: 17676
diff changeset
   102
      ProofGeneral release packages. Assuming that you are in the
d7f78036546b renamed "Packages" to "Download";
wenzelm
parents: 17676
diff changeset
   103
      directory where you downloaded the files, install them into <tt
d7f78036546b renamed "Packages" to "Download";
wenzelm
parents: 17676
diff changeset
   104
      class="shellcmd">/opt</tt> by typing into the bash shell:</p>
16674
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   105
    
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   106
      <ul class="shellcmd">
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   107
        <li>tar -C /usr/opt -xvzf <?value key="distname"?>.tar.gz</li>
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   108
        <li>tar -C /usr/opt -xvzf ProofGeneral.tar.gz</li>
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   109
      </ul>
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   110
      
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   111
      <p>The location <tt class="shellcmd">/opt</tt> again is just a proposal; if you choose other
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   112
      locations, some tweaking in the <a href="#config"><tt class="shellcmd">etc/settings</tt>
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   113
      file</a> may be neccessary later.</p>
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   114
    
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   115
      <h2 id="config">Configuring Isabelle</h2>
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   116
    
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   117
      <p>Edit the file <tt class="shellcmd">/opt/Isabelle/etc/settings</tt>; first, uncomment the
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   118
      lines about SMLNJ. Also set the variable SMLNJ_CYGWIN_RUNTIME to 1, in order
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   119
      the cygwin version of SMLNJ is used. As mentioned above, the path variables
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   120
      for the ML system and ProofGeneral may need adjustions, depending on your
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   121
      different installation locations.</p>
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   122
    
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   123
      <p>Take heed of the setting of ISABELLE_HOME_USER; by default, this is
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   124
      <tt class="shellcmd">~/isabelle</tt>. To detect which Windows path this will be mapped to,
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   125
      type into the Cygwin bash shell:</p>
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   126
    
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   127
      <ul class="shellcmd">
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   128
        <li>cygpath --windows ~/isabelle</li>
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   129
      </ul>
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   130
      
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   131
      <p>If you don't like this location to be the isabelle home
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   132
      directory, consider setting of ISABELLE_HOME_USER to another value; use
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   133
      <tt class="shellcmd">cygpath --unix &lt;winpath&gt;</tt> to detect which Cygwin path a given
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   134
      Windows path is mapped to.</p>
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   135
    
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   136
      <p>A typical change could look like this:</p>
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   137
    
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   138
      <blockquote>
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   139
        from<br />
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   140
        <tt># Standard ML of New Jersey 110 or later<br />
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   141
        #ML_SYSTEM=smlnj-110<br />
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   142
        #ML_HOME="$ISABELLE_HOME/../smlnj/bin"<br />
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   143
        #ML_OPTIONS="@SMLdebug=/dev/null"<br />
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   144
        #ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2&gt;/dev/null); echo
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   145
        "$HEAP_SUFFIX")<br /></tt>
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   146
      </blockquote>
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   147
    
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   148
      <blockquote>
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   149
        to<br />
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   150
        <tt># Standard ML of New Jersey 110 or later<br />
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   151
        SMLNJ_CYGWIN_RUNTIME=1<br />
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   152
        ML_SYSTEM=smlnj-110<br />
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   153
        ML_HOME="$ISABELLE_HOME/../smlnj/bin"<br />
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   154
        ML_OPTIONS="@SMLdebug=/dev/null"<br />
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   155
        ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2&gt;/dev/null); echo
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   156
        "$HEAP_SUFFIX")</tt>
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   157
      </blockquote>
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   158
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   159
      <h2>Building logics</h2>
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   160
    
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   161
      <p>Now we can compile some logics. Start the cygwin shell (if not still
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   162
      running) and type:</p>
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   163
    
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   164
      <ul class="shellcmd">
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   165
        <li>cd /opt/Isabelle</li>
17563
abb280dd3431 unify dist and main
haftmann
parents: 16674
diff changeset
   166
        <li>build FOL</li>
abb280dd3431 unify dist and main
haftmann
parents: 16674
diff changeset
   167
        <li>build ZF</li>
16674
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   168
        <li>build HOL</li>
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   169
      </ul>
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   170
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   171
      <p>The compilation process may take some time (depending on how fast the
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   172
      computer is). Before building a logic image the build program shows some
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   173
      variables and expects user input &ndash; just hit enter.</p>
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   174
    
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   175
      <h2>Running Isabelle with ProofGeneral</h2>
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   176
    
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   177
      <p>Now everything should be ready. To test, start the cygwin shell and
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   178
      type</p>
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   179
    
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   180
      <ul class="shellcmd">
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   181
        <li>startx &amp;</li>
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   182
      </ul>
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   183
      
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   184
      <p>This will start the cygwin X server and an X shell window. In
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   185
      the X shell window, type</p>
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   186
    
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   187
      <ul class="shellcmd">
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   188
        <li>/opt/Isabelle/bin/Isabelle &amp;</li>.
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   189
      </ul>
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   190
      
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   191
      <p>This will start the ProofGeneral interface for Isabelle. After a
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   192
      while an empty buffer <tt>Scratch.thy</tt> is created. You can turn on
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   193
      X-Symbol from the menu Proof-General, item Options.</p>
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   194
    
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   195
      <p>Load one of your favorite theories and test your Isabelle installation by
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   196
      proving something.</p>
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   197
    
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   198
      <p>To simplify starting ProofGeneral, consider writing a Windows command
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   199
      script, e.&nbsp;g.</p>
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   200
    
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   201
      <blockquote>
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   202
        <tt>@bash startx -geometry 30x4 -iconic -e Isabell</tt>
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   203
      </blockquote>
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   204
      
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   205
      <p>and assigning a shortcut in the start menu to it.</p>
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   206
    </div>
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   207
    <div class="hr"><hr/></div>
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   208
    <?include file="//include/footer.include.html"?>
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   209
</body>
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   210
bf2cd93cc245 unified main and dist
haftmann
parents:
diff changeset
   211
</html>