There will be wireless network access for the registered participants, and for people with chalmers accounts (cid). If you bring your own laptop, make sure you have a working wireless connection in your computer. We will also provide a CD and USB memory with the base software, in case of network problems.
[To TYPES School Main Page]Agda
- General info: Agda Homepage
In the above link you can (among other things) find information about how to get the latest sources from CVS. If you choose to do so, please look at the file README-SummerSchool.- Installation specific to the summer school:
We have prepared a version of Agda that will be used in the summer school.
To install this version of Agda, you need a recent version of the Haskell compiler ghc . Download the following file:
Agda-TYPES-2005.tgz
Unpack it and enter the Agda directory. Look at the Agda-part of the following installation log ( install.log ) in which you can see what commands are issued to compile and install Agda and its emacs-mode. The emacs-mode installation should work on most unix-systems, but the path to the emacs mode probably have to be changed according to the system you have.
The emacs-mode is important, since the interface we will use for Agda is solely implemented as an emacs-mode.
Replace "/usr/share/locale/summerschool/agda" above with the location were you prefer to put the Agda libraries (see next bullet).
- An Agda Library.
Download the following file: AgdaLib-TYPES-2005.tgz
Coq
The version used will be Coq-8.0pl2. The binary installation will serve most purposes,
but you can also install it from the sources, and then you can try some of Bertot's extensions.
- General info: Coq Homepage
- Binary installation: (Linux Redhat on PC)
Download the files: coq-8.0pl2-1.i386.rpm , and coqide-8.0pl2-1.i386.rpm.
Install: rpm -i file.rpm
- From source:
Download the following file: coq-8.0pl2.tar.gz
Look at the installation log for details: install.log .
Note that it might be difficult to install coqide from sources.
Note also: To compile Coq you need the ocaml compiler, version 3.06 or later,
and the parser library ocamlp4, recent version. To compile coqide you need lablGtk, an ocaml-interface to gtk.
Warning ! It might be difficult to compile coqide from source. An alternative could be to compile coq, and then install the coqide binary.
Coq can also be run from the command-line using coqtop (built-in in coq), and with Proof General, a mode in XEmacs.
Isabelle
The version of Isabelle used will be Isabelle 2004.
The user-interface for Isabelle will be Proof General run in XEmacs.
- General info: Isabelle Homepage
- Installation, see installation.html
- For various installation issues, it might help to look how we did (on a RedHat Linux PC):
again, the log... install.log .- Testing successful installation:
Citing Nipkow:
Start Isabelle (with command Isabelle). That should launch xemacs and Proof General. Load isabelle/src/HOL/Library/Primes.thy. This should activate Proof General. Now activate xsymbols by setting Proof-General > Options > X-Symbol. This should turn \forall etc into nice mathematical symbols (maybe after reloading the file). If you click on the Use icon, the whole buffer should be processed by Isabelle: first it turns pink, later blue. If all of this works, you have correctly installed Isabelle.
Other systems
The following systems will also be discussed, but as far as we know now they will not be part of the practical sessions:
Pre-installed software
As additional help for installing the software we provide the installation log from an IBM T40 1500MHz laptop running RedHat Enterprise Linux, kernel 2.6. See the following file: install.log .
Resource directory
Here is a directory with the various resource files mentioned in the above text. We might add things here later. Feel free to browse: resources/