42 lines
1.5 KiB
Nix
42 lines
1.5 KiB
Nix
|
{ 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;
|
||
|
|
}
|