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.