Documentation

- -

General

- -

- Isabelle runs on common Unix platforms. - For Linux, Solaris and MaxOS / Darwin, we provide ready-to-install bundles; - for other Unices, Isabelle has to be built from scratch. -

- -

- A usable Isabelle system consists of the following components: -

- -

a suitable ML environment for Standard ML
the Isabelle system itself, including the desired object logic(s) - (e. g. HOL)
the ProofGeneral user interface

- -

Optionally, theory graph browsing may be used if a Java JRE 1.1 or above - is installed.

- -

For operating-system-specific instructions:

- -

Linux (x86)
Solaris (sparc)
MacOS X / Darwin
Windows

- -

Linux

- -

Commonly, an installation of Isabelle could work as follows:

- -

Ensure that your system has a running XEmacs 21 or Emacs 21 - with mule support (for ProofGeneral)
Get the packages for Poly/ML, - ProofGeneral (including - the Emacs X-Symbol package) - and Isabelle, - either from our package page or from the - links below. When you download ProofGeneral, please - register
Likewise download the compiled image(s) of your desired object logic(s)
Unpack the archives to an appropriate location, e. g. - /usr/local: -
- tar -C /usr/local -xzf
- tar -C /usr/local -xzf
- tar -C /usr/local -xzf
- tar -C /usr/local -xzf
- tar -C /usr/local -xzf
-
Under most circumstances, the default settings of Isabelle should be reasonable for - invoking Isabelle/ProofGeneral without further ado: -
- /usr/local/Isabelle/bin/Isabelle
- Note that there is a separate option in - the Proof General Options menu to enable X-Symbol. -
If Emacs appears to hang when the prover process is started, see the - ProofGeneral FAQ for - advice. -

- -

For more information, see the file INSTALL.

- -

Solaris

- -

Before you start, ensure the following for your system:

GNU bash 2.x
perl 5.x
GNU tar 1.13 or higher
GNU gzip 1.3 or higher
running XEmacs 21 or Emacs 21 - with mule support (for ProofGeneral)

- -

Then, an installation on Solaris is analogous to Linux:

- -

Get the packages for Poly/ML, - ProofGeneral (including - the Emacs X-Symbol package) - and Isabelle, - either from our package page or from the - links below. When you download ProofGeneral, please - register
Likewise download the compiled image(s) of your desired object logic(s)
Unpack the archives to an appropriate location, e. g. - /usr/local: -
- gtar -C /usr/local -xzf
- gtar -C /usr/local -xzf
- gtar -C /usr/local -xzf
- gtar -C /usr/local -xzf
- gtar -C /usr/local -xzf
-
Under most circumstances, the default settings of Isabelle should be reasonable for - invoking Isabelle/ProofGeneral without further ado: -
- /usr/local/Isabelle/bin/Isabelle
- Note that there is a separate option in - the Proof General Options menu to enable X-Symbol. -
If Emacs appears to hang when the prover process is started, see the - ProofGeneral FAQ for - advice. -

- -

For more information, see the file INSTALL.

- -

MaxOS X / Darwin

- -

Before you start, ensure the following for your system:

running MacOS X 10.2.2 or higher
running XEmacs 21 or Emacs 21 with mule support (for ProofGeneral) - – for further reference, see the - MacOS X Emacs hints -

- -

Then, an installation on Darwin is analogous to Linux:

- -

Get the packages for Poly/ML, - ProofGeneral (including - the Emacs X-Symbol package) - and Isabelle, - either from our package page or from the - links below. When you download ProofGeneral, please - register
Likewise download the compiled image(s) of your desired object logic(s)
Unpack the archives to an appropriate location, e. g. - /usr/local: -
- gtar -C /usr/local -xzf
- gtar -C /usr/local -xzf
- gtar -C /usr/local -xzf
- gtar -C /usr/local -xzf
- gtar -C /usr/local -xzf
-
Under most circumstances, the default settings of Isabelle should be reasonable for - invoking Isabelle/ProofGeneral without further ado: -
- /usr/local/Isabelle/bin/Isabelle
- Note that there is a separate option in - the Proof General Options menu to enable X-Symbol. -
If Emacs appears to hang when the prover process is started, see the - ProofGeneral FAQ for - advice. -

- -

Windows

- -

Isabelle does not run nativly on Windows; in a restricted fashion, - you may run Isabelle on Windows using the Cygwin environment. - See Installation notes for - Cygwin/Windows.

- -

For a serious apporach, you should consider a Windows/Linux dualboot - installation.

- -

MacOS X Emacs hints

- -

Assuming you have an installation of Isabelle on your Mac, - there are various possibilites for running ProofGeneral:

- -

You should also be able to launch Proof General by typing - Isabelle at the Unix command line. This will invoke the - Apple-supplied version of Emacs in a terminal window, providing a primitive - environment.
Somewhat better is to run Proof General from within a version - of Emacs ported as a native Mac OS X application, such as MacEmacs JP or - mindlube's or Enhanced Carbon Emacs. - Visiting a theory file from Emacs will automatically launch Proof General - provided isabelle is on the search path. None of these options - support the X-Symbol package, unfortunately.
In order to get the full benefit of Proof General, you must install the X - Window System (X11) and XEmacs or - GNU Emacs.

- apple's version of X11 - is included with the Panther (MacOS X 10.3) installation discs, though it is - not installed by default. The Command key serves as Meta, but it is - reserved for standard Apple shortcuts such as C, V and X, so you must use - Esc-C, Esc-V and Esc-X in Emacs or else deselect »Enable key equivalents« - in the X11 preferences.
The easiest way to install XEmacs or GNU Emacs is via the package manager - Fink. Install the Fink package - xemacs-sumo-pkg to get the XEmacs libraries that Proof General needs - to run. To install GNU Emacs, install the package emacs21. Fink can - compile from sources, but this takes hours, so it is better to request binary - installations.
To use GNU - Emacs instead of XEmacs, you must - recompile Proof General and X-Symbol following the instructions here. Note that Proof General - incorporates its own copy of X-Symbol.

- -

You may want to install this drag-and-drop Isabelle launcher. It is a simple hack that - invokes XEmacs on any files dropped on it.

- -

Here is a screenshot showing Proof General running - in GNU Emacs.

- -

Preconditions and restrictions

- -

Please notice before you go ahead:

- -

The ML system these notes apply to is Standard ML of New Jersey; it is not - known yet how to get Isabelle run completely with 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).

- -

Any suggestions and improvements concerning this hints are welcomed!

- -

Acknowlegements

- -

Thanks to Norbert - Völker and Viorel Preoteasa whose - efforts helped a lot to get Isabelle run this way.

- -

Installing Cygwin

- -

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

- -

To install it, get the installer from the Cygwin website and run it. It will ask you which - packages to install, and then downloads and installs them. Please make sure - you install everything needed by Isabelle; it is hard to give a concise list - of packages here since the bundling of Cygwin packages may vary over time, - but installing the base packages, perl, make, xemacs and x-server should be a - good choice for the beginning.

- -

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 will be - mapped to Windows path c:\cygwin\opt\smlnj.

- -

After installation, open a Cygwin shell window (normally the installer - makes a shortcut for you).

- -

Getting and building SML/NJ

- -

Now we are ready to get and build SML/NJ; before this, set the environment variable - SMLNJ_CYGWIN_RUNTIME to 1:

- -

export SMLNJ_CYGWIN_RUNTIME=1

- -

This setting will tell the build process that it should - not attempt to build SML/NJ natively for Win32 but for Cygwin - instead (see further CYGWININSTALL).

- -

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 to - learn about the different possibilites to do this. The default packages - should be sufficient.

- -

In the following, it is assumed that you install SML/NJ to Cygwin path - /opt/smlnj; if you choose an other location, some tweaking in the - etc/settings file may be neccessary later.

- -

Whenever SMLNJ is used, the SMLNJ_CYGWIN_RUNTIME environment variable 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. 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 .tar.gz
tar -C /usr/opt -xvzf ProofGeneral.tar.gz

- -

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 may be neccessary later.

- -

Configuring Isabelle

- -

Edit the file /opt/Isabelle/etc/settings; first, uncomment the - lines about SMLNJ. Also set the variable SMLNJ_CYGWIN_RUNTIME to 1, in order - the cygwin version of SMLNJ is used. As mentioned above, the path variables - for the ML system and ProofGeneral may need adjustions, depending on your - different installation locations.

- -

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

- -

cygpath --windows ~/isabelle

- -

If you don't like this location to be the isabelle home - directory, consider setting of ISABELLE_HOME_USER to another value; use - cygpath --unix <winpath> to detect which Cygwin path a given - Windows path is mapped to.

- -

A typical change could look like this:

- -

- from
- # Standard ML of New Jersey 110 or later - #ML_SYSTEM=smlnj-110 - #ML_HOME="$ISABELLE_HOME/../smlnj/bin" - #ML_OPTIONS="@SMLdebug=/dev/null" - #ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo - "$HEAP_SUFFIX") -

- -

- to
- # Standard ML of New Jersey 110 or later - SMLNJ_CYGWIN_RUNTIME=1 - ML_SYSTEM=smlnj-110 - ML_HOME="$ISABELLE_HOME/../smlnj/bin" - ML_OPTIONS="@SMLdebug=/dev/null" - ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo - "$HEAP_SUFFIX") -

- -

Building logics

- -

Now we can compile some logics. Start the cygwin shell (if not still - running) and type:

- -

cd /opt/Isabelle
build HOL
build ZF

- -

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: 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 rename /opt/Isabelle/bin/isabelle to - /opt/Isabelle/bin/Isabelle. This script - will start Isabelle with ProofGeneral; the isabelle - script in any case is available as isabelle-process.

- -

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

- -

startx &

- -

This will start the cygwin X server and an X shell window. In - the X shell window, type

- -

/opt/Isabelle/bin/Isabelle &

- -

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, item Options.

- -

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.

- -

- @bash startx -geometry 30x4 -iconic -e Isabell -

- -

and assigning a shortcut in the start menu to it.

- -

Inconveniencies with the current version of - Isabelle

- -

With the current Isabelle release (Isabelle 2004), there are two - inconveniencies:

- -

During extraction you will get a warning that file - Real/HahnBanach/Aux.thy can not be created. This is because - Aux is not allowed as a filename under Windows. If you do not want - to run the HahnBanach example, you might simply want to ignore this - warning.
The tool isatool mkdir tries to detect the name of the current - user, to put it into the generated root.tex. Alas, on Windows, - this leads to an unquoted \ in the TeX file. So you either must - edit your root.tex manually to fix this, or directly patch - /opt/Isabelle/lib/Tools/mkdir by replacing - -
- AUTHOR=$("$AUTO_PERL" -e "@pw = getpwnam(\"$USER\"); print @pw[6]" | tr _ -) -
with - -
- AUTHOR="default author name" -
-

- -

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 neatly with Poly/ML on Windows, since it is not clear - how Poly/ML has to be compiled for Cygwin, and the native Windows port - of PolyML does not provide some Posix signals Isabelle/ProofGeneral relies on.

- -

If you know how to circumvent (fully or partially) any of these problems, - please let us know.

- -

Installing on Mac OS X

Mac OS X is the current version - of the Macintosh operating system, installed on all new Apple computers. Because it is based on Unix, it - can run Isabelle. The new - Power Mac G5 is an excellent - Isabelle machine. Here is a screenshot showing Proof General running - in GNU Emacs.

- -

This page gives advice on building Isabelle for Mac OS X. It assumes that - you are familiar with both Mac OS X and Unix. You must have installed the Mac - OS X developer tools.

- -

Download Isabelle to a suitable directory, as described on the - download page. Be sure to get the following - files - -
- .tar.gz
- ProofGeneral.tar.gz
- polyml_base.tar.gz
- polyml_ppc-darwin.tar.gz
- HOL_ppc-darwin.tar.gz
-
You may have to install the bash shell. Versions of Mac OS X prior to - 10.2.2 did not provide it. If /bin/bash does not exist, you can install it - using the package manager Fink.
At this point, you should be able to run Isabelle with the command line - interface. You can also build Isabelle from the Unix command line, - following the instructions for "Compiling Logics" in file - Isabelle/INSTALL.
You should also be able to launch Proof General by typing - Isabelle at the Unix command line. This will invoke the - Apple-supplied version of Emacs in a terminal window, providing a primitive - environment. Somewhat better is to run Proof General from within a version - of Emacs ported as a native Mac OS X application, such as MacEmacs JP or - mindlube's or Enhanced Carbon Emacs. - Visiting a theory file from Emacs will automatically launch Proof General - provided isabelle is on the search path. None of these options - support the X-Symbol package, unfortunately.

- -

In order to get the full benefit of Proof General, you must install the X - Window System (X11) and XEmacs or - GNU Emacs.

- -

Apple's version of X11 - is included with the Panther (MacOS 10.3) installation discs, though it is - not installed by default. The Command key serves as Meta, but it is - reserved for standard Apple shortcuts such as C, V and X, so you must use - Esc-C, Esc-V and Esc-X in Emacs or else deselect "Enable key equivalents" - in the X11 preferences.
Some people prefer the OroborOSX - window manager. It must be used in conjunction with XFree86, which is easy to install if you use the - installer provided by the XonX project.

- -

The easiest way to install XEmacs or GNU Emacs is via the package manager - Fink. Install the Fink package - xemacs-sumo-pkg to get the XEmacs libraries that Proof General needs - to run. To install GNU Emacs, install the package emacs21. Fink can - compile from sources, but this takes hours, so it is better to request binary - installations.

- -

To use GNU - Emacs instead of XEmacs, you must - recompile Proof General and X-Symbol following the instructions here. Note that Proof General - incorporates its own copy of X-Symbol.

- -

Install X11 or OroborOSX.
Install XEmacs (and its libraries), or install GNU Emacs and recompile - Proof General.
You may want to install this drag-and-drop Isabelle launcher. It is a simple hack that - invokes xemacs on any files dropped on it.

- -

Getting started

diff -r 6b14aba5ddaa -r bf2cd93cc245 Admin/website/download_past.html --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Admin/website/download_past.html Mon Jul 04 15:15:55 2005 +0200 @@ -0,0 +1,43 @@ + + + + + + + Older Isabelle Releases + + + + + +

+ +

MacOS X Emacs hints

+ +

Assuming you have an installation of Isabelle on your Mac, + there are various possibilites for running ProofGeneral:

+ +

You should also be able to launch Proof General by typing + Isabelle at the Unix command line. This will invoke the + Apple-supplied version of Emacs in a terminal window, providing a primitive + environment.
Somewhat better is to run Proof General from within a version + of Emacs ported as a native Mac OS X application, such as MacEmacs JP or + mindlube's or Enhanced Carbon Emacs. + Visiting a theory file from Emacs will automatically launch Proof General + provided isabelle is on the search path. None of these options + support the X-Symbol package, unfortunately.
In order to get the full benefit of Proof General, you must install the X + Window System (X11) and XEmacs or + GNU Emacs.

+ apple's version of X11 + is included with the Panther (MacOS X 10.3) installation discs, though it is + not installed by default. The Command key serves as Meta, but it is + reserved for standard Apple shortcuts such as C, V and X, so you must use + Esc-C, Esc-V and Esc-X in Emacs or else deselect »Enable key equivalents« + in the X11 preferences.
The easiest way to install XEmacs or GNU Emacs is via the package manager + Fink. Install the Fink package + xemacs-sumo-pkg to get the XEmacs libraries that Proof General needs + to run. To install GNU Emacs, install the package emacs21. Fink can + compile from sources, but this takes hours, so it is better to request binary + installations.
To use GNU + Emacs instead of XEmacs, you must + recompile Proof General and X-Symbol following the instructions here. Note that Proof General + incorporates its own copy of X-Symbol.

+ +

You may want to install this drag-and-drop Isabelle launcher. It is a simple hack that + invokes XEmacs on any files dropped on it.

+ +

Here is a screenshot showing Proof General running + in GNU Emacs.

+ +

Preconditions and restrictions

+ +

Please notice before you go ahead:

+ +

The ML system these notes apply to is Standard ML of New Jersey; it is not + known yet how to get Isabelle run completely with 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).

+ +

Any suggestions and improvements concerning this hints are welcomed!

+ +

Acknowlegements

+ +

Thanks to Norbert + Völker and Viorel Preoteasa whose + efforts helped a lot to get Isabelle run this way.

+ +

Installing Cygwin

+ +

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

+ +

To install it, get the installer from the Cygwin website and run it. It will ask you which + packages to install, and then downloads and installs them. Please make sure + you install everything needed by Isabelle; it is hard to give a concise list + of packages here since the bundling of Cygwin packages may vary over time, + but installing the base packages, perl, make, xemacs and x-server should be a + good choice for the beginning.

+ +

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 will be + mapped to Windows path c:\cygwin\opt\smlnj.

+ +

After installation, open a Cygwin shell window (normally the installer + makes a shortcut for you).

+ +

Getting and building SML/NJ

+ +

Now we are ready to get and build SML/NJ; before this, set the environment variable + SMLNJ_CYGWIN_RUNTIME to 1:

+ +

export SMLNJ_CYGWIN_RUNTIME=1

+ +

This setting will tell the build process that it should + not attempt to build SML/NJ natively for Win32 but for Cygwin + instead (see further CYGWININSTALL).

+ +

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 to + learn about the different possibilites to do this. The default packages + should be sufficient.

+ +

In the following, it is assumed that you install SML/NJ to Cygwin path + /opt/smlnj; if you choose an other location, some tweaking in the + etc/settings file may be neccessary later.

+ +

Whenever SMLNJ is used, the SMLNJ_CYGWIN_RUNTIME environment variable 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. 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 .tar.gz
tar -C /usr/opt -xvzf ProofGeneral.tar.gz

+ +

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 may be neccessary later.

+ +

Configuring Isabelle

+ +

Edit the file /opt/Isabelle/etc/settings; first, uncomment the + lines about SMLNJ. Also set the variable SMLNJ_CYGWIN_RUNTIME to 1, in order + the cygwin version of SMLNJ is used. As mentioned above, the path variables + for the ML system and ProofGeneral may need adjustions, depending on your + different installation locations.

+ +

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

+ +

cygpath --windows ~/isabelle

+ +

If you don't like this location to be the isabelle home + directory, consider setting of ISABELLE_HOME_USER to another value; use + cygpath --unix <winpath> to detect which Cygwin path a given + Windows path is mapped to.

+ +

A typical change could look like this:

+ +

+ from
+ # Standard ML of New Jersey 110 or later + #ML_SYSTEM=smlnj-110 + #ML_HOME="$ISABELLE_HOME/../smlnj/bin" + #ML_OPTIONS="@SMLdebug=/dev/null" + #ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo + "$HEAP_SUFFIX") +

+ +

+ to
+ # Standard ML of New Jersey 110 or later + SMLNJ_CYGWIN_RUNTIME=1 + ML_SYSTEM=smlnj-110 + ML_HOME="$ISABELLE_HOME/../smlnj/bin" + ML_OPTIONS="@SMLdebug=/dev/null" + ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo + "$HEAP_SUFFIX") +

+ +

Building logics

+ +

Now we can compile some logics. Start the cygwin shell (if not still + running) and type:

+ +

cd /opt/Isabelle
build HOL
build ZF

+ +

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: 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 rename /opt/Isabelle/bin/isabelle to + /opt/Isabelle/bin/Isabelle. This script + will start Isabelle with ProofGeneral; the isabelle + script in any case is available as isabelle-process.

+ +

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

+ +

startx &

+ +

This will start the cygwin X server and an X shell window. In + the X shell window, type

+ +

/opt/Isabelle/bin/Isabelle &

+ +

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, item Options.

+ +

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.

+ +

+ @bash startx -geometry 30x4 -iconic -e Isabell +

+ +

and assigning a shortcut in the start menu to it.

+ +

Inconveniencies with the current version of + Isabelle

+ +

With the current Isabelle release (Isabelle 2004), there are two + inconveniencies:

+ +

During extraction you will get a warning that file + Real/HahnBanach/Aux.thy can not be created. This is because + Aux is not allowed as a filename under Windows. If you do not want + to run the HahnBanach example, you might simply want to ignore this + warning.
The tool isatool mkdir tries to detect the name of the current + user, to put it into the generated root.tex. Alas, on Windows, + this leads to an unquoted \ in the TeX file. So you either must + edit your root.tex manually to fix this, or directly patch + /opt/Isabelle/lib/Tools/mkdir by replacing + +
+ AUTHOR=$("$AUTO_PERL" -e "@pw = getpwnam(\"$USER\"); print @pw[6]" | tr _ -) +
with + +
+ AUTHOR="default author name" +
+

+ +

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 neatly with Poly/ML on Windows, since it is not clear + how Poly/ML has to be compiled for Cygwin, and the native Windows port + of PolyML does not provide some Posix signals Isabelle/ProofGeneral relies on.

+ +

If you know how to circumvent (fully or partially) any of these problems, + please let us know.

+ +

Getting started

Mailing list and FAQ

Isabelle Documentation

Release notes

Course Material and Exercises

Development snapshot

Past releases

Archive

Welcome to the Isabelle Distribution!

General

Linux

Solaris

MaxOS X / Darwin

Windows

MacOS X Emacs hints

Preconditions and restrictions

Acknowlegements

Installing Cygwin

Getting and building SML/NJ

Installing Isabelle

Configuring Isabelle

Building logics

Running Isabelle with ProofGeneral

Inconveniencies with the current version of - Isabelle

A note on Poly/ML

Installing on Mac OS X

More about Isabelle

Getting started

Archive

Site Mirrors:

Navigation

General

MacOS X Emacs hints

Preconditions and restrictions

Acknowlegements

Installing Cygwin

Getting and building SML/NJ

Installing Isabelle

Configuring Isabelle

Building logics

Running Isabelle with ProofGeneral

Inconveniencies with the current version of + Isabelle

A note on Poly/ML

What is Isabelle?

Preview of Isabelle