# HG changeset patch # User kleing # Date 1115597028 -7200 # Node ID 55c3932335b9826b55f07dc0425e8a8c74d97c6c # Parent 292a9de8abe93418ce4ee1e071d74d6fcf1fc7f9 made file links local, smoothed text over in some places diff -r 292a9de8abe9 -r 55c3932335b9 Admin/page/dist-content/notes_win_cygwin.content --- a/Admin/page/dist-content/notes_win_cygwin.content Mon May 09 02:03:01 2005 +0200 +++ b/Admin/page/dist-content/notes_win_cygwin.content Mon May 09 02:03:48 2005 +0200 @@ -13,11 +13,12 @@ Poly/ML. See a note on Poly/ML down this page.
  • It is assumed you have some experience with an Unix operating - system (e. g. what a shell is for and how to use it basically). - This is neccessary since the ML system has to be compiled from scratch.
  • + system (e.g. what a shell is for and how to use it).

    +

    Acknowlegements

    +

    Thanks to Norbert Vöker and Viorel Preoteasa @@ -25,7 +26,7 @@

    Installing Cygwin

    -

    Cygwin is a POSIX emulation layer for windows; it contains ports of a large +

    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, …).

    @@ -40,7 +41,7 @@

    By default, cygwin installs to c:\cygwin; 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 /opt/smlnj +filesystem tree, i.e. the Cygwin path /opt/smlnj will be mapped to Windows path c:\cygwin\opt\smlnj.

    After installation, open a Cygwin shell window (normally the installer @@ -69,7 +70,7 @@ to build SML/NJ natively for Win32 but for Cygwin instead (see further CYGWININSTALL).

    -

    So far, this whole setup was tested using the latest working version (110.53) +

    So far, this setup was tested using the working version 110.53 of SML/NJ from http://smlnj.cs.uchicago.edu/dist/working/110.53/. SML/NJ provides a nice installer enabling you to download and build it. Read INSTALL @@ -82,25 +83,24 @@ may be neccessary later.

    Whenever SMLNJ is used, the SMLNJ_CYGWIN_RUNTIME environment variable -must be set to 1 (lateron a convenient mechanism to make this the default +must be set to 1 (later on a convenient mechanism to make this the default is proposed).

    Installing Isabelle

    -

    Download the latest Isabelle and ProofGeneral release packages from -http://isabelle.in.tum.de/dist/packages.html. +

    Download the latest Isabelle and ProofGeneral release packages. Assuming that you are in the directory where you downloaded the files, install them into /opt by typing into the bash shell:

    - tar -C /usr/opt -xvzf Isabelle2004.tar.gz
    - tar -C /usr/opt -xvzf ProofGeneral-3.5.tar.gz + tar -C /usr/opt -xvzf
    + tar -C /usr/opt -xvzf
    -During extracting, one inconvenience may occur, see below.

    +During extraction, one inconvenience may occur, see below.

    The location /opt again is just a proposal; if you choose other locations, some tweaking in the etc/settings file @@ -115,7 +115,7 @@ installation locations.

    Take heed of the setting of ISABELLE_HOME_USER; by default, this is -~/isabelle. To detect to which Windows path this will be mapped, +~/isabelle. To detect which Windows path this will be mapped to, type into the Cygwin bash shell:

    @@ -169,21 +169,20 @@

    -

    The compilation process may take quite a lot of time (depending also on -how fast the computer is). When starting building some logic the build -program shows some variables and expects the user input – just hit enter. +

    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 – just hit enter.

    Running Isabelle with ProofGeneral

    -

    On Linux Isabelle can be started by two scripts located in Isabelle/bin: +

    On Linux, Isabelle can be started by two scripts located in Isabelle/bin: Isabelle and isabelle. Isabelle 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 copy /opt/Isabelle/bin/isabelle to /opt/Isabelle/bin/Isabell. The script /opt/Isabelle/bin/Isabell will start Isabelle with ProofGeneral.

    -

    How everything is ready to test some theory. Start the cygwin shell -(if not already running) and type +

    Now everything should be ready. To test, start the cygwin shell and type

    startx & @@ -196,15 +195,15 @@ /opt/Isabelle/bin/Isabell &.
    -This will start the ProofGeneral interface for Isabelle. After a while an empty buffer -scratch.thy is created. You can turn on X-Symbol and Electric Terminator -from the menu Proof-General &rarrow; Options.

    +This will start the ProofGeneral interface for Isabelle. After a while +an empty buffer Scratch.thy is created. You can turn on +X-Symbol from the menu Proof-General &rarrow; Options.

    -

    Load one of your favorite theory and test your Isabelle installation +

    Load one of your favorite theories and test your Isabelle installation by proving something.

    To simplify starting ProofGeneral, consider writing a Windows command script, -e. g. +e.g.

    @bash startx -geometry 30x4 -iconic -e Isabell @@ -243,18 +242,17 @@ -

    To get around both inconveniencies, consider using a recent developer snapshot -of Isabelle; either, both inconveniencies won't be alive anymore in the next -Isabelle release.

    +

    To get around these inconveniencies, consider using a recent developer snapshot +of Isabelle; both will be fixed in the next Isabelle release.

    A note on Poly/ML

    As indicated above, Isabelle does not run -neatlessly with Poly/ML on Windows, due to two +neatly with Poly/ML on Windows, for two reasons: