General

This repository holds the sources for the Albatross compiler.

The language Albatross allows static verification (i.e. correctness proofs) of programs.

The albatross compiler is a proof assistant and a compiler for the Albatross language.

Installation

Prerequisites: In order to compile the Albatross compiler you need the OCaml compiler. The OCaml compiler is available at no cost through caml.inria.fr and installs easily on a variety of platforms.

Compile the Albatross compiler with the commands:

cd path/to/albatross/ocaml

ocamlbuild -lib unix alba.native

Now you have the file alba.native in the directory albatross/ocaml/_build which is the executable albatross compiler. Copy (or link) it under the name alba to any location which is in the search path for programs.

The basic libary is in albatross/library/alba.base. In order to use it you have to compile it.

cd path/to/albatross/library/alba.base

alba init

alba compile

Set the environment variable ALBA_LIB_PATH to path/to/albatross/library (e.g. in the bash shell export ALBA_LIB_PATH=/path/to/albatross/library) and the compiler will find the libraries automatically.

For the emacs editor there is an albatross mode which does syntax highlighting. The file albatross-mode.el can be found in the directory misc. The file contains instructions to activate the mode in emacs.