ATS：带定理证明的编程/安装 ATS 编程语言系统

本文提供了在系统上安装 ATS 编译器的说明。最后，提供了一个非常简单的程序来帮助您测试安装。

安装 ATS

注意：这些说明已在 Ubuntu Linux 上测试过，可能需要针对其他发行版进行更改。

在 Linux 上，第一步是下载当前 ATS 编译器 ATS/Anairiats 的稳定版本。文件名应类似于 "ats-lang-anairiats-x.x.x.tar.gz"，其中 "x.x.x" 代表版本。然后，您可以将其安装到/usr/share/atshome/ 或主目录下的某个目录中。

安装到 /usr/share/atshome/

打开终端并调用

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

现在将此添加到环境中

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

安装到主目录

如果您选择安装到其他目录，例如 ~/FOO，请先解压到某个临时目录

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

然后将 /tmp/usr/share/atshome 移动到 ~/FOO

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

然后将以下内容添加到 ~/.bashrc

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

第一个程序

为了测试，请在您喜欢的文本编辑器中编写以下内容

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

并将它保存到名为 hello.dats 的文件中。然后请执行以下命令行

atscc -o hello hello.dats

如果一切顺利，./hello 将是一个新生成的执行文件，它应该在执行时将字符串 "Hello, world!" 和一个换行符打印到控制台。

文件名扩展名

您将感兴趣的两种主要类型的文件

• 扩展名 .sats（第一个字母来自“statics”）用于包含模块接口的文件，以及
• 扩展名 .dats（第一个字母来自“dynamics”）用于包含接口实现的文件。

“statics” 和“dynamics” 的含义将在后面解释。