I wanted to look at ATS again after a long gap. I've written about it many times before but haven't done much with it in recent years. Part of what prompted this was looking at Verus for verified Rust programming and thinking about how ATS compares. ATS takes a different approach to verification. It's built into the type system itself rather than added as an annotation layer. Proofs are first-class values that you construct and pass around. It compiles to C and the proofs are erased during compilation so the generated code is just plain C with no runtime overhead.

In this post I go through the steps I needed to build ATS1 and ATS2 from their GitHub repositories on Linux and macOS. I expected this to be straightforward but ended up spending a fair amount of time working through bitrot in the existing documentation and build system.

# Bitrot

The last official ATS2 release was version 0.4.2 in 2020. Development has continued on GitHub but there hasn't been a new release tarball. The ATS website still links to older releases. Most of the build instructions I found online are out of date or refer to release tarballs that aren't the best way to get started anymore. Building from the GitHub repositories requires building ATS1 (ATS-Anairiats) first since the ATS2 compiler is written in ATS1. This is where most of the problems are. The ATS1 repository has broken autotools symlinks, missing directories and issues with newer versions of macOS. I spent some time working through these and documenting the fixes here.

# Prerequisites

On Linux (Debian/Ubuntu) the dependencies are straightforward:

$ sudo apt-get install -y build-essential automake bison libgmp-dev

On macOS with Homebrew there are a few extra steps. Install the dependencies:

$ brew install automake bison gmp gcc

Homebrew's bison needs to be added to the PATH because macOS ships an older version that is too old for the ATS1 build:

$ export PATH="/opt/homebrew/opt/bison/bin:$PATH"

This is for Apple Silicon. On Intel Macs the path is /usr/local/opt/bison/bin instead.

# Cloning the repositories

Both ATS1 and ATS2 need to be cloned:

$ mkdir -p ats && cd ats
$ git clone https://github.com/githwxi/ATS-Anairiats.git
$ git clone https://github.com/githwxi/ATS-Postiats.git

# Building ATS1

The ATS1 repository has some issues that need to be fixed before building. The first is that the install-sh and missing files are symlinks pointing to an automake-1.15 installation that won't exist on your system. These need to be replaced:

$ cd ATS-Anairiats
$ rm -f install-sh missing
$ automake --add-missing --copy 2>/dev/null || true

The automake command will print warnings about missing Makefile.am files but this can be ignored. It copies the real install-sh and missing scripts from your system's automake installation into the working directory, replacing the dead symlinks.

The build also expects a bootstrap1 directory that doesn't exist in the repository. I'm not sure if this is something that used to be generated by a step that no longer works or if it was always missing:

$ mkdir -p bootstrap1

With the symlinks and directory fixed, configure the build. For Linux:

$ ./configure

On macOS, Homebrew installs GMP to a non-standard location so the paths need to be passed to configure:

$ CPPFLAGS="-I$(brew --prefix gmp)/include" LDFLAGS="-L$(brew --prefix gmp)/lib" ./configure

GMP is needed because ATS2's type checker generates integer arithmetic constraints at compile time and the patsopt compiler uses GMP for arbitrary-precision constraint solving. There is also a non-GMP variant that uses machine integers instead but it can overflow on complex constraints so GMP is what should be preferred. The rest of this post assumes the GMP build.

Check that the output includes checking for gmp.h... yes. If it says no then the ATS1 libraries will be built without GMP support and the ATS2 build will fail later with confusing linker errors. This tripped me up on my first attempt on macOS.

Pre-existing archive files in the repository are checked in as read-only which causes errors during the build:

$ chmod u+w ccomp/lib/*.a ccomp/lib64/*.a 2>/dev/null

Set the required environment variables and build:

$ export ATSHOME=$PWD
$ export ATSHOMERELOC=ATS-0.2.12

On macOS there is an additional issue that took me a while to figure out. Apple Clang treats implicit function declarations as errors whereas GCC on Linux only warns. The ATS1 codebase triggers these in several places. There are two mechanisms that invoke gcc during the build and each needs its own fix:

$ export C_INCLUDE_PATH="$(brew --prefix gmp)/include"
$ export LIBRARY_PATH="$(brew --prefix gmp)/lib"
$ export CC="gcc -Wno-error=implicit-function-declaration"

The CC variable handles Makefile $(CC) calls. The ATS1 batch compiler atscc also invokes gcc internally via execvp() and passes the ATSCCOMP variable directly as the program name without shell word splitting. I initially tried just setting ATSCCOMP="gcc -Wno-error=implicit-function-declaration" but that doesn't work because atscc doesn't split it into separate arguments. I used a wrapper script intead. I'm not sure it's the best fix but got things working:

$ mkdir -p "$ATSHOME/bin"
$ cat > "$ATSHOME/bin/atscc-gcc" <<'EOF'
#!/bin/sh
exec gcc -Wno-error=implicit-function-declaration "$@"
EOF
$ chmod +x "$ATSHOME/bin/atscc-gcc"
$ export ATSCCOMP="$ATSHOME/bin/atscc-gcc"

With the environment set, the build is the same on both platforms:

$ make all0

The all0 target builds without GC support which is fine for only using it to build ATS2. The all target links against the Boehm garbage collector which the ATS runtime can use for automatic memory management. Since we only need ATS1 to compile ATS2's source to C, the garbage collector isn't needed. The build takes a couple of minutes and produces a lot of output as it compiles the ATS1 compiler and its standard library. Verify it worked:

$ bin/atsopt --version
ATS/Anairiats version 0.2.13 with Copyright (c) 2002-2014 Hongwei Xi

The version reports 0.2.13 which is confusing because ATSHOMERELOC needs to be set to ATS-0.2.12. These are actually unrelated. The version number is just what atsopt reports. ATSHOMERELOC controls how ATS encodes module paths into C symbol names. ATS uses percent encoding to turn paths like prelude/DATS/unsafe.dats into C symbols. Without ATSHOMERELOC it uses the full absolute path from your filesystem which produces symbols that don't match anything in libats.a. The value ATS-0.2.12 is what was used when we compiled those library archives in the make all0 step. It doesn't matter that the compiler itself is version 0.2.13.

# Building ATS2

With ATS1 built, set the environment variables for the ATS2 build. Run these from the parent ats/ directory:

$ export ATSHOME=$(pwd)/ATS-Anairiats
$ export ATSHOMERELOC=ATS-0.2.12
$ export PATSHOME=$(pwd)/ATS-Postiats

The ATSHOMERELOC variable is important and I spent some time debugging what happens without it. If it's not set, ATS1 generates C code with absolute filesystem paths baked into symbol names. These won't match the symbols in libats.a and you get confusing linker errors like:

undefined reference to `_2Users_2you_2ats_2ATS_2dAnairiats_2prelude_2DATS_2unsafe_2edats__staload'

On macOS keep all the environment variables from the ATS1 build step exported as the ATS2 build uses them too. The ATS2 build itself is a single make target:

$ cd ATS-Postiats
$ make -f Makefile_devl all

This takes a few minutes. It uses atsopt (ATS1) to compile the ATS2 compiler source to C, then gcc to compile that C into the patsopt binary, then patsopt to build patscc and the standard library. The Makefile_devl is used instead of the regular Makefile because the regular one expects a pre-built patsopt to already exist. The _devl variant bootstraps everything from ATS1.

Verify the build:

$ bin/patsopt --version
ATS/Postiats version 0.4.3 with Copyright (c) 2011-2021 Hongwei Xi

# Testing with hello world

$ export PATH=$PATSHOME/bin:$PATH
$ cat > /tmp/hello.dats << 'EOF'
implement main0 () = println! ("Hello from ATS2!")
EOF
$ patscc -o /tmp/hello /tmp/hello.dats
$ /tmp/hello
Hello from ATS2!

The patscc wrapper handles calling patsopt to compile ATS to C and then invoking gcc to produce the binary. The -o flag works the same as with gcc. If you look at the generated C in /tmp/hello_dats.c you can see the output of the compilation. ATS generates readable C with comments indicating the source locations.

# Installation

When building from the GitHub source there is no make install target so ATS2 just runs from the source directory. The patsopt compiler needs PATSHOME to find the prelude, runtime headers and standard library at compile time. Without it you get errors about missing SATS and HATS files when trying to compile anything that includes the prelude. I added these to my shell profile:

export PATSHOME=/path/to/ATS-Postiats
export PATH=$PATSHOME/bin:$PATH

On macOS also add the GMP path exports:

export C_INCLUDE_PATH="$(brew --prefix gmp)/include"
export LIBRARY_PATH="$(brew --prefix gmp)/lib"

# Creating a release tarball

The GitHub build has no make install target but it is possible to produce a self-contained release tarball that can be built with just a C compiler and no ATS1. The release infrastructure lives in ATS-Postiats/doc/DISTRIB/. I went through the process of generating one to see if it still works and to document the steps.

This requires autoconf in addition to the earlier prerequisites:

$ sudo apt-get install -y autoconf

All environment variables from the ATS1 and ATS2 build steps must still be set. The first step is to generate the CBOOT files which are the pre-generated C source that allows building without ATS1:

$ cd $PATSHOME
$ make -f Makefile_devl all
$ make -C src -f Makefile CBOOTgmp

The CBOOTgmp target takes the compiled ATS2 source and generates standalone C files that can bootstrap the compiler without needing ATS1. These go into src/CBOOT/.

The distribution template directory under doc/DISTRIB/ATS-Postiats needs the env.sh templates and a generated configure script:

$ cp $PATSHOME/bin/*_env.sh.in $PATSHOME/doc/DISTRIB/ATS-Postiats/bin/
$ cd $PATSHOME/doc/DISTRIB/ATS-Postiats
$ sh ./autogen.sh
$ ./configure

Generate C for the standard library:

$ cd $PATSHOME
$ make -C src/CBOOT/prelude -f Makefile
$ make -C src/CBOOT/libc -f Makefile
$ make -C src/CBOOT/libats -f Makefile

These targets use patsopt to compile the prelude and standard library ATS files to C, placing the results alongside the compiler CBOOT files so the release tarball is fully self-contained.

Generate the distribution Makefile from Makefile.atxt using atsdoc:

$ cd $PATSHOME/doc/DISTRIB
$ make -f Makefile.gen

With everything generated, the final packaging step assembles the tarball:

$ make -f Makefile atspackaging
$ make -f Makefile atspacktarzvcf_gmp

This produces ATS2-Postiats-gmp-0.4.3.tgz in the current directory. The tarball contains all the pre-generated C source, the configure script and Makefile so that end users can build with just a C compiler.

If you'd rather not run all of these steps manually, there is a build_release.sh script in share/SCRIPT/ that automates the process. I haven't tested it thoroughly but it should be run from a clean working directory outside the source tree:

$ cd /tmp
$ sh $PATSHOME/share/SCRIPT/build_release.sh 0.4.3 gmpknd

# Installing from a release tarball

The release tarball only needs a C compiler to build. No ATS1 is required since the tarball includes the pre-generated C source for the compiler. Extract and build:

$ tar xzf ATS2-Postiats-gmp-0.4.3.tgz
$ cd ATS2-Postiats-gmp-0.4.3
$ ./configure
$ make
$ sudo make install

The configure script detects GMP and sets up the Makefile. The make step compiles patsopt from the CBOOT C source and then builds patscc and the standard library.

On macOS, GMP headers and libraries are in Homebrew's prefix rather than the default search paths, so pass them to configure:

$ CPPFLAGS="-I$(brew --prefix gmp)/include" LDFLAGS="-L$(brew --prefix gmp)/lib" ./configure

This installs to /usr/local by default. The installed wrapper scripts set PATSHOME automatically so no manual environment setup is needed after install. To install to a different location use --prefix:

$ ./configure --prefix=$HOME/.local
$ make
$ make install

After make install you should be able to run patscc directly to compile ATS programs.

# Conclusion

Getting ATS built from source in 2026 requires working around some bitrot in the build system but it is doable on both Linux and macOS. The main pain points for me were the broken autotools symlinks in the ATS1 repository, macOS Clang treating implicit function declarations as errors and getting GMP paths right on macOS.

Some further reading: