Adding ATS1, updating ATS2 package.

2 files changed, 79 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;
+}
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 0000000000000..93c6fa07d8a69
--- /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
+