10 files changed, 68 insertions, 96 deletions

diff --git a/math/hs-Agda/Makefile b/math/hs-Agda/Makefile
index a323aeef942a..d86e179601d9 100644
--- a/math/hs-Agda/Makefile
+++ b/math/hs-Agda/Makefile
@@ -2,42 +2,33 @@
 # $FreeBSD$
 
 PORTNAME=	Agda
-PORTVERSION=	2.3.0.1
-PORTREVISION=	3
+PORTVERSION=	2.3.2
 CATEGORIES=	math haskell
 
 MAINTAINER=	haskell@FreeBSD.org
-COMMENT=	A dependently typed functional programming language and proof assistant
+COMMENT=	Dependently typed functional programming language and proof assistant
 
 CABAL_SETUP=	Setup.hs
 
-USE_CABAL=	hashable>=1.2 hashtables haskeline>=0.6.3.2 \
-		haskell-src-exts>=1.9.6 mtl QuickCheck>=2.3 syb>=0.1 \
+USE_CABAL=	geniplate>=0.6.0.3 hashable>=1.2 hashtables \
+		haskeline>=0.6.3.2 haskell-src-exts>=1.9.6 mtl \
+		QuickCheck>=2.3 parallel syb>=0.1 unordered-containers>=0.2 \
 		xhtml zlib>=0.4.0.1
 USE_ALEX=	yes
 USE_HAPPY=	yes
 USE_ICONV=	yes
 
-EXECUTABLE=	agda-mode
+EXECUTABLE=	agda-mode agda
 
 INSTALL_PORTDATA=	(cd ${WRKSRC} && ${INSTALL_DATA} README ${DATADIR}; \
 			 cd ${WRKSRC}/doc && ${COPYTREE_SHARE} \* ${DATADIR})
 
-SHOW_PKGMSG=	yes
+OPTIONS_DEFINE=		EPIC
 
-OPTIONS_DEFINE=		USE_LOCALE EPIC
-
-USE_LOCALE_DESC=	Use encoding specified by the locale
 EPIC_DESC=		Install the Epic compiler
 
 .include "${.CURDIR}/../../lang/ghc/bsd.cabal.options.mk"
 
-.if ${PORT_OPTIONS:MUSE_LOCALE}
-CONFIGURE_ARGS+=	--flags="use-locale"
-.else
-CONFIGURE_ARGS+=	--flags="-use-locale"
-.endif
-
 .if ${PORT_OPTIONS:MEPIC}
 CONFIGURE_ARGS+=	--flags="epic"
 USE_CABAL+=		epic>=0.1.13
diff --git a/math/hs-Agda/distinfo b/math/hs-Agda/distinfo
index 5ed05c7e5708..485c853062a9 100644
--- a/math/hs-Agda/distinfo
+++ b/math/hs-Agda/distinfo
@@ -1,2 +1,2 @@
-SHA256 (cabal/Agda-2.3.0.1.tar.gz) = 5cc016a6cf113979d92af05c10b1e92dead4bf87861086177a017ce1d7605338
-SIZE (cabal/Agda-2.3.0.1.tar.gz) = 612342
+SHA256 (cabal/Agda-2.3.2.tar.gz) = d47a0b2a0806ea5c109b59280211a47b980b47a8f6ac0ab9fca673f3d4c6e0f6
+SIZE (cabal/Agda-2.3.2.tar.gz) = 726462
diff --git a/math/hs-Agda/files/patch-Agda.cabal b/math/hs-Agda/files/patch-Agda.cabal
index ad9b3b70f9a2..208d469dd4d5 100644
--- a/math/hs-Agda/files/patch-Agda.cabal
+++ b/math/hs-Agda/files/patch-Agda.cabal
@@ -1,38 +1,13 @@
---- ./Agda.cabal.orig	2012-03-12 11:09:34.000000000 +0100
-+++ ./Agda.cabal	2013-02-05 04:15:30.000000000 +0100
-@@ -71,13 +71,13 @@
-   if flag(use-locale)
-     build-depends:  base >= 4.2 && < 4.6
-   else
--    build-depends:  base == 4.1.*,
-+    build-depends:  base >= 4.1,
-                     utf8-string == 0.3.*
-   if flag(epic)
-     build-depends:  epic >= 0.1.13 && < 0.10
--  build-depends:    mtl == 2.0.*,
--                    QuickCheck >= 2.3 && < 2.5,
--                    haskell-src-exts >= 1.9.6 && < 1.12,
-+  build-depends:    mtl >= 2.0,
-+                    QuickCheck >= 2.3 && < 2.6,
-+                    haskell-src-exts >= 1.9.6,
-                     containers >= 0.1 && < 0.5,
-                     pretty >= 1.0 && < 1.2,
-                     directory >= 1.0 && < 1.2,
-@@ -90,7 +90,7 @@
+--- ./Agda.cabal.orig	2012-11-12 01:25:25.000000000 +0100
++++ ./Agda.cabal	2013-03-09 17:44:08.000000000 +0100
+@@ -82,8 +82,8 @@
                      process >= 1.0.1.0 && < 1.2,
-                     haskeline >= 0.6.3.2 && < 0.7,
+                     haskeline >= 0.6.3.2 && < 0.8,
                      xhtml == 3000.2.*,
--                    hashable == 1.1.*,
-+                    hashable == 1.2.*,
-                     hashtables == 1.0.*,
-                     syb >= 0.1 && < 0.4
-   build-tools:      happy >= 1.15 && < 2,
-@@ -334,7 +334,7 @@
-   if flag(use-locale)
-     build-depends:  base >= 4.2 && < 4.6
-   else
--    build-depends:  base == 4.1.*,
-+    build-depends:  base >= 4.1,
-                     utf8-string == 0.3.*
-   build-depends:    filepath >= 1.1 && < 1.4,
-                     process >= 1.0.1.0 && < 1.2,
+-                    hashable >= 1.1.2.3 && < 1.2,
+-                    hashtables == 1.0.*,
++                    hashable >= 1.1.2.3 && < 1.3,
++                    hashtables == 1.1.*,
+                     geniplate >= 0.6.0.3 && < 0.7,
+                     parallel < 3.3,
+                     deepseq == 1.3.*,
diff --git a/math/hs-Agda/files/patch-src__full__Agda__Compiler__MAlonzo__Compiler.hs b/math/hs-Agda/files/patch-src__full__Agda__Compiler__MAlonzo__Compiler.hs
deleted file mode 100644
index bae4ce30dd13..000000000000
--- a/math/hs-Agda/files/patch-src__full__Agda__Compiler__MAlonzo__Compiler.hs
+++ /dev/null
@@ -1,11 +0,0 @@
---- ./src/full/Agda/Compiler/MAlonzo/Compiler.hs.orig	2012-03-12 11:09:33.000000000 +0100
-+++ ./src/full/Agda/Compiler/MAlonzo/Compiler.hs	2012-04-08 22:51:55.000000000 +0200
-@@ -466,7 +466,7 @@
-   ]
-   where
-     parse = HS.parseWithMode
--              HS.defaultParseMode{HS.extensions = [HS.ExplicitForall]}
-+              HS.defaultParseMode{HS.extensions = [HS.ExplicitForAll]}
- 
-     ok (HS.ParseOk d)   = d
-     ok HS.ParseFailed{} = __IMPOSSIBLE__
diff --git a/math/hs-Agda/files/patch-src__full__Agda__Syntax__Abstract__Name.hs b/math/hs-Agda/files/patch-src__full__Agda__Syntax__Abstract__Name.hs
new file mode 100644
index 000000000000..5108666a5839
--- /dev/null
+++ b/math/hs-Agda/files/patch-src__full__Agda__Syntax__Abstract__Name.hs
@@ -0,0 +1,24 @@
+--- ./src/full/Agda/Syntax/Abstract/Name.hs.orig	2012-11-12 01:25:21.000000000 +0100
++++ ./src/full/Agda/Syntax/Abstract/Name.hs	2013-02-10 15:14:44.000000000 +0100
+@@ -239,8 +239,8 @@
+   show x = show (nameConcrete x) -- ++ "|" ++ show (nameId x)
+ 
+ instance Hashable Name where
+-  {-# INLINE hash #-}
+-  hash = hash . nameId
++  {-# INLINE hashWithSalt #-}
++  hashWithSalt salt = hashWithSalt salt . nameId
+ 
+ instance Show QName where
+   show q = concat $ intersperse "." $ map show $ qnameToList q
+@@ -255,8 +255,8 @@
+   compare = compare `on` qnameName
+ 
+ instance Hashable QName where
+-  {-# INLINE hash #-}
+-  hash = hash . qnameName
++  {-# INLINE hashWithSalt #-}
++  hashWithSalt salt = hashWithSalt salt . qnameName
+ 
+ instance HasRange Name where
+   getRange = getRange . nameConcrete
diff --git a/math/hs-Agda/files/patch-src__full__Agda__Syntax__Common.hs b/math/hs-Agda/files/patch-src__full__Agda__Syntax__Common.hs
new file mode 100644
index 000000000000..b071c8448e13
--- /dev/null
+++ b/math/hs-Agda/files/patch-src__full__Agda__Syntax__Common.hs
@@ -0,0 +1,13 @@
+--- ./src/full/Agda/Syntax/Common.hs.orig	2012-11-12 01:25:21.000000000 +0100
++++ ./src/full/Agda/Syntax/Common.hs	2013-02-10 15:12:42.000000000 +0100
+@@ -272,8 +272,8 @@
+   fromEnum (NameId n _) = fromIntegral n
+ 
+ instance Hashable NameId where
+-  {-# INLINE hash #-}
+-  hash (NameId n m) = hash (n, m)
++  {-# INLINE hashWithSalt #-}
++  hashWithSalt salt (NameId n m) = hashWithSalt salt (n, m)
+ 
+ newtype Constr a = Constr a
+ 
diff --git a/math/hs-Agda/files/patch-src__full__Agda__Termination__Lexicographic.hs b/math/hs-Agda/files/patch-src__full__Agda__Termination__Lexicographic.hs
deleted file mode 100644
index 907f0bed5274..000000000000
--- a/math/hs-Agda/files/patch-src__full__Agda__Termination__Lexicographic.hs
+++ /dev/null
@@ -1,11 +0,0 @@
---- ./src/full/Agda/Termination/Lexicographic.hs.orig	2012-03-12 11:09:33.000000000 +0100
-+++ ./src/full/Agda/Termination/Lexicographic.hs	2012-10-03 23:48:30.000000000 +0200
-@@ -230,7 +230,7 @@
-   , quickCheck' prop_fromDiagonals
-   , quickCheck' prop_newBehaviour
-   , quickCheckWith' stdArgs{ maxSuccess = 50
--                           , maxDiscard = 200
-+                           , maxDiscardRatio = 200
-                            , maxSize    = 20
-                            }
-                     prop_lexOrder
diff --git a/math/hs-Agda/files/patch-src__full__Agda__TypeChecking__Serialise.hs b/math/hs-Agda/files/patch-src__full__Agda__TypeChecking__Serialise.hs
deleted file mode 100644
index ef6fa31298eb..000000000000
--- a/math/hs-Agda/files/patch-src__full__Agda__TypeChecking__Serialise.hs
+++ /dev/null
@@ -1,11 +0,0 @@
---- ./src/full/Agda/TypeChecking/Serialise.hs.orig	2012-03-12 11:09:33.000000000 +0100
-+++ ./src/full/Agda/TypeChecking/Serialise.hs	2013-02-05 04:30:03.000000000 +0100
-@@ -119,7 +119,7 @@
- -- | With direct access to the internals of 'TypeRep' this instance
- -- could presumably be improved.
- instance Hashable TypeRep' where
--  hash = hash . show . unTypeRep'
-+  hashWithSalt n = hashWithSalt n . show . unTypeRep'
- 
- data St = St
-   { nodeE     :: !(Array Int32 Node)
diff --git a/math/hs-Agda/files/patch-src__full__Agda__Utils__Pointer.hs b/math/hs-Agda/files/patch-src__full__Agda__Utils__Pointer.hs
new file mode 100644
index 000000000000..1d480e01d10b
--- /dev/null
+++ b/math/hs-Agda/files/patch-src__full__Agda__Utils__Pointer.hs
@@ -0,0 +1,11 @@
+--- ./src/full/Agda/Utils/Pointer.hs.orig	2012-11-12 01:25:22.000000000 +0100
++++ ./src/full/Agda/Utils/Pointer.hs	2013-02-10 15:11:53.000000000 +0100
+@@ -71,7 +71,7 @@
+   compare = compare `on` ptrTag
+ 
+ instance Hashable (Ptr a) where
+-  hash = hash . ptrTag
++  hashWithSalt salt = hashWithSalt salt . ptrTag
+ 
+ instance NFData (Ptr a) where
+ 
diff --git a/math/hs-Agda/pkg-message b/math/hs-Agda/pkg-message
deleted file mode 100644
index 10d2fc595c34..000000000000
--- a/math/hs-Agda/pkg-message
+++ /dev/null
@@ -1,9 +0,0 @@
-Note that if you want to use the command-line program (agda), then
-you should also install the Agda-executable package. The Agda
-package includes an Emacs mode for Agda, but you need to set up the
-Emacs mode yourself (for instance by running agda-mode setup; see
-the README).
-
-Note also that this library does not follow the package versioning
-policy, because the library is only intended to be used by the Emacs
-mode and the Agda-executable package.