From 0242b3c6ac186aea0ae7bf2c7f876133325d7119 Mon Sep 17 00:00:00 2001 From: Artyom Shalkhakov Date: Tue, 25 Mar 2014 04:51:35 +0100 Subject: [PATCH] Adding ATS1, updating ATS2 package. --- pkgs/development/compilers/ats/default.nix | 41 +++++++++++++++++++ .../ats/install-atsdoc-hats-files.patch | 38 +++++++++++++++++ pkgs/development/compilers/ats2/default.nix | 6 ++- pkgs/top-level/all-packages.nix | 1 + 4 files changed, 84 insertions(+), 2 deletions(-) create mode 100644 pkgs/development/compilers/ats/default.nix create mode 100644 pkgs/development/compilers/ats/install-atsdoc-hats-files.patch diff --git a/pkgs/development/compilers/ats/default.nix b/pkgs/development/compilers/ats/default.nix new file mode 100644 index 000000000000..a5ed478a879f --- /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; +} diff --git a/pkgs/development/compilers/ats/install-atsdoc-hats-files.patch b/pkgs/development/compilers/ats/install-atsdoc-hats-files.patch new file mode 100644 index 000000000000..93c6fa07d8a6 --- /dev/null +++ b/pkgs/development/compilers/ats/install-atsdoc-hats-files.patch @@ -0,0 +1,38 @@ +--- ats-lang-anairiats-0.2.11/Makefile 2013-12-10 00:43:52.000000000 +0100 ++++ ats-lang-anairiats-0.2.11/Makefile 2014-03-02 07:49:06.985837425 +0100 +@@ -97,7 +97,7 @@ + cd $(abs_top_srcdir) + [ -d $(bindir2) ] || $(MKDIR_P) $(bindir2) + $(MKDIR_P) $(ATSLIBHOME2)/bin +- find ccomp contrib doc libats libc prelude -type d \ ++ find ccomp contrib doc libats libatsdoc libc prelude -type d \ + -exec $(MKDIR_P) $(ATSLIBHOME2)/\{} \; \ + -print + +@@ -105,7 +105,7 @@ + # + # recursively install all files in the list except .svn control files. + # +- for d in ccomp/runtime contrib doc libats libc prelude; do \ ++ for d in ccomp/runtime contrib doc libats libatsdoc libc prelude; do \ + cd $(abs_top_srcdir) && \ + $(INSTALL) -d $(ATSLIBHOME2)/"$$d" && \ + find "$$d" -name .svn -prune -o -type f \ +@@ -143,6 +143,17 @@ + $(INSTALL) -m 755 ats_env.sh $(bindir2)/"$$b" && \ + echo [ats_env.sh] is installed into $(bindir2)/"$$b"; \ + done ++# ++# install atsdoc headers ++# ++ for f in \ ++ utils/atsdoc/SATS/*.sats utils/atsdoc/DATS/*.dats utils/atsdoc/HATS/*.hats; \ ++ do \ ++ [ -f "$$f" ] || continue; \ ++ cd $(abs_top_srcdir) && \ ++ $(INSTALL) -m 644 -D "$$f" $(ATSLIBHOME2)/"$$f" && \ ++ echo "$$f"; \ ++ done + + install:: install_files + diff --git a/pkgs/development/compilers/ats2/default.nix b/pkgs/development/compilers/ats2/default.nix index ae9a202a529e..c1c71b0dfe21 100644 --- a/pkgs/development/compilers/ats2/default.nix +++ b/pkgs/development/compilers/ats2/default.nix @@ -1,11 +1,11 @@ { stdenv, fetchurl, gmp }: -let version = "0.0.5"; in stdenv.mkDerivation { +let version = "0.0.6"; in stdenv.mkDerivation { name = "ats2-postiats-${version}"; src = fetchurl { url = "mirror://sourceforge/ats2-lang/ATS2-Postiats-${version}.tgz"; - sha256 = "1rzcqc7fwqf0y4cc14lr282r25s66jygf6cxrnf5l8p5p550l0dl"; + sha256 = "110a4drzf656j9s5yfvxj1cwgh5g9ysnh40cv8y9qfjjkki8vd5b"; }; buildInputs = [ gmp ]; @@ -15,4 +15,6 @@ let version = "0.0.5"; in stdenv.mkDerivation { homepage = http://www.ats-lang.org/; license = stdenv.lib.licenses.gpl3Plus; }; + + platforms = stdenv.lib.platforms.all; } diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix index 7e81a39ec083..8e2a54b17cb2 100644 --- a/pkgs/top-level/all-packages.nix +++ b/pkgs/top-level/all-packages.nix @@ -2360,6 +2360,7 @@ let aspectj = callPackage ../development/compilers/aspectj { }; + ats = callPackage ../development/compilers/ats { }; ats2 = callPackage ../development/compilers/ats2 { }; avra = callPackage ../development/compilers/avra { };