Wikibooks

ATS: Programming with Theorem-Proving/Installing and operating the ATS compiler

< ATS: Programming with Theorem-Proving

Installing ATS

edit

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/

edit

Open a terminal and invoke 

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

Now add this to the environment: 

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

Installing into home directory

edit

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: 

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

An explanation of the meaning of the two environment variables is in order. Both are assumed to be non-empty.

  • ATSHOME is an absolute path to the ATS installation directory
  • ATSHOMERELOC is a version of the installed ATS compiler, and is used for name mangling in the generated code

The first program

edit

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 extensions

edit

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

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

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

Retrieved from "https://en.wikibooks.org/w/index.php?title=ATS:_Programming_with_Theorem-Proving/Installing_and_operating_the_ATS_compiler&oldid=2433536"