ATS: Programming with Theorem-Proving/Installing the ATS programming language system

In this article we provide instructions on installing the ATS compiler on your system. At the end, a very simple program is provided to help you test your installation.

Installing ATS

NOTE: these instructions have been tested on Ubuntu Linux, and may need to be changed for other distributions.

On Linux, the first step is to download the stable version of the current ATS compiler, ATS/Anairiats. The filename should be along the lines of "ats-lang-anairiats-x.x.x.tar.gz", where "x.x.x" stands for version. Then you can install either into /usr/share/atshome/ or into some directory under your home directory.

Installing into /usr/share/atshome/

Open a terminal and invoke

sudo tar xvzf ats-lang-anairiats-x.x.x.tar.gz /

Now add this to the environment:

export ATSHOME=/usr/share/atshome
export ATSHOMERELOC=ATS-x.x.x
export PATH=$ATSHOME/bin:$PATH

Installing into home directory

If you choose to install in a different directory, say ~/FOO, untar into some temporary directory first:

tar xvzf ats-lang-anairiats-x.x.x.tar.gz /tmp

Then move /tmp/usr/share/atshome to ~/FOO:

mv /tmp/usr/share/atshome ~/FOO

And then add the following to ~/.bashrc:

export ATSHOME=~/FOO/atshome
export ATSHOMERELOC=ATS-x.x.x
export PATH=$ATSHOME/bin:$PATH

The first program

For testing, please write the following in your favorite text editor:

implement main () = print "hello, world!\n"

and save it into a file named hello.dats. Then please issue the following command-line:

atscc -o hello hello.dats

If everything goes fine, then ./hello is a newly generated executable, which should print the string "Hello, world!" and a newline onto the console when executed.

File name extensions

There are two major types of files you'll be interested in:

• the extension .sats (the first letter comes from "statics") is for files containing module interface, and
• the extension .dats (the first letter comes from "dynamics") is for files containing implementation of interface.

The meaning of "statics" and "dynamics" will be explained later.