diff options
Diffstat (limited to 'pkgs/development/compilers/ats/default.nix')
-rw-r--r-- | pkgs/development/compilers/ats/default.nix | 41 |
1 files changed, 41 insertions, 0 deletions
diff --git a/pkgs/development/compilers/ats/default.nix b/pkgs/development/compilers/ats/default.nix new file mode 100644 index 0000000000000..a5ed478a879f3 --- /dev/null +++ b/pkgs/development/compilers/ats/default.nix @@ -0,0 +1,41 @@ +{ stdenv, fetchurl, gmp }: + +let version = "0.2.11"; in stdenv.mkDerivation { + name = "ats-anairiats-${version}"; + + src = fetchurl { + url = "mirror://sourceforge/ats-lang/ats-lang-anairiats-${version}.tgz"; + sha256 = "0rqykyx5whichx85jr4l4c9fdan0qsdd4kwd7a81k3l07zbd9fc6"; + }; + # this is necessary because atxt files usually include some .hats files + patches = [ ./install-atsdoc-hats-files.patch ]; + + buildInputs = [ gmp ]; + + meta = { + description = "A statically typed programming language that unifies implementation with formal specification"; + homepage = http://www.ats-lang.org/; + license = stdenv.lib.licenses.gpl3Plus; + longDescription = + '' + ATS is a programming language with a highly expressive type system + rooted in the framework Applied Type System. In particular, both + dependent types and linear types are available in ATS. The current + implementation of ATS (ATS/Anairiats) is written in ATS itself. It can + be as efficient as C/C++ and supports a variety of programming + paradigms. + + In addition, ATS contains a component ATS/LF that supports a form of + (interactive) theorem proving, where proofs are constructed as total + functions. With this component, ATS advocates a programming style that + combines programming with theorem proving. Furthermore, this component + may be used as a logical framework to encode various deduction systems + and their (meta-)properties. + + This package contains the compiler atsopt, the frontend atscc, + and the lexer atslex. + ''; + }; + + platforms = stdenv.lib.platforms.all; +} |