- Update to 2.7.1

- Add CVC4 support option and enabled by default
- Unbreak on aarch64, sbrk is not used anymore
- Remove build date to make the build reproducible
- Pass maintainership to submitter
- Pet `portlint -abct`

PR:		231443
Submitted by:	Greg V <greg@unrelenting.technology>

21 files changed, 61 insertions, 248 deletions

diff --git a/lang/maude/Makefile b/lang/maude/Makefile
index ff59506a7b4e..0bc46c0eeb0b 100644
--- a/lang/maude/Makefile
+++ b/lang/maude/Makefile
@@ -2,13 +2,12 @@
 # $FreeBSD$
 
 PORTNAME=	maude
-PORTVERSION=	2.6
-PORTREVISION=	1
+PORTVERSION=	2.7.1
 CATEGORIES=	lang
-MASTER_SITES=	http://maude.cs.illinois.edu/versions/${PORTVERSION}/
+MASTER_SITES=	http://maude.cs.illinois.edu/w/images/d/d8/
 DISTNAME=	Maude-${PORTVERSION}
 
-MAINTAINER=	ports@FreeBSD.org
+MAINTAINER=	greg@unrelenting.technology
 COMMENT=	High-performance reflective language
 
 LICENSE=	GPLv2
@@ -21,28 +20,32 @@ LIB_DEPENDS=	libbdd.so:science/buddy \
 		libsigsegv.so:devel/libsigsegv
 
 USES=		alias autoreconf bison ncurses
+
+WRKSRC=		${WRKDIR}/maude-${PORTVERSION}
+
 GNU_CONFIGURE=	yes
 CPPFLAGS+=	-I${NCURSESINC} -I${LOCALBASE}/include
 LDFLAGS+=	-L${NCURSESLIB} -L${LOCALBASE}/lib
 CONFIGURE_ARGS=	--datadir=${DATADIR}
 MAKE_JOBS_UNSAFE=	yes
 
-FULL_MAUDE_VER=	26b
+OPTIONS_SUB=		yes
+OPTIONS_DEFINE=		DOCS FULL_MAUDE CVC4
+OPTIONS_DEFAULT=	FULL_MAUDE CVC4
+FULL_MAUDE_DESC=	Install full-maude
+CVC4_DESC=		Enable SMT support via CVC4
 
-OPTIONS_DEFINE=	DOCS FULL_MAUDE
-OPTIONS_DEFAULT=	FULL_MAUDE
-FULL_MAUDE_DESC=	Install full-maude${FULL_MAUDE_VER}
+CVC4_LIB_DEPENDS=	libcvc4.so:math/cvc4
+CVC4_CONFIGURE_WITH=	cvc4
 
 PORTDOCS=	AUTHORS COPYING ChangeLog INSTALL NEWS README
 
-BROKEN_aarch64=		Fails to link: missing sbrk
-
 .include <bsd.port.options.mk>
 
 .if ${PORT_OPTIONS:MFULL_MAUDE}
-MASTER_SITES+=	http://maude.lcc.uma.es/FullMaude/FM${FULL_MAUDE_VER}/:fm
-FULL_MAUDE=	full-maude${FULL_MAUDE_VER}.maude
-FULL_MAUDE_DIST=	full-maude.maude.zip
+MASTER_SITES+=	http://maude.cs.illinois.edu/w/images/c/ca/:fm
+FULL_MAUDE=	full-maude.maude
+FULL_MAUDE_DIST=	Full-Maude-${PORTVERSION}.zip
 DISTFILES=	${DISTNAME}${EXTRACT_SUFX} ${FULL_MAUDE_DIST}:fm
 EXTRACT_ONLY=	${DISTNAME}${EXTRACT_SUFX}
 EXTRACT_DEPENDS+=	${LOCALBASE}/bin/unzip:archivers/unzip
diff --git a/lang/maude/distinfo b/lang/maude/distinfo
index 03390fa2dc52..2092fd7230b4 100644
--- a/lang/maude/distinfo
+++ b/lang/maude/distinfo
@@ -1,5 +1,5 @@
-TIMESTAMP = 1478641858
-SHA256 (Maude-2.6.tar.gz) = a5ba79bf3d30565c874e80b3531b51a7e835b600e86cac82508a6eb9e15f4aa0
-SIZE (Maude-2.6.tar.gz) = 1600026
-SHA256 (full-maude.maude.zip) = 57ebfc41056b7afc2be48983f6a1311e817d23eeaaed71023471bc4edaf6b128
-SIZE (full-maude.maude.zip) = 154881
+TIMESTAMP = 1537177216
+SHA256 (Maude-2.7.1.tar.gz) = b1887c7fa75e85a1526467727242f77b5ec7cd6a5dfa4ceb686b6f545bb1534b
+SIZE (Maude-2.7.1.tar.gz) = 1853963
+SHA256 (Full-Maude-2.7.1.zip) = 4c3a11b053ea92df4cfe89939a97c6b02c68489b174eb689c844c08decb18f78
+SIZE (Full-Maude-2.7.1.zip) = 156771
diff --git a/lang/maude/files/patch-Mixfix-lexerAux b/lang/maude/files/patch-Mixfix-lexerAux
deleted file mode 100644
index f37b92b29821..000000000000
--- a/lang/maude/files/patch-Mixfix-lexerAux
+++ /dev/null
@@ -1,22 +0,0 @@
---- ./src/Mixfix/lexerAux.cc.orig	2014-09-03 02:54:57.000000000 +0200
-+++ ./src/Mixfix/lexerAux.cc	2014-09-03 02:55:40.000000000 +0200
-@@ -35,7 +35,7 @@
- bool fakeNewlineStack[MAX_IN_DEPTH];
- 
- void
--getInput(char* buf, int& result, int max_size)
-+getInput(char* buf, size_t& result, size_t max_size)
- {
-   result = YY_NULL;
-   if (UserLevelRewritingContext::interrupted())
---- ./src/Mixfix/lexerAux.hh.orig	2014-09-03 02:56:33.000000000 +0200
-+++ ./src/Mixfix/lexerAux.hh	2014-09-03 02:57:05.000000000 +0200
-@@ -27,7 +27,7 @@
- //extern int inStackPtr;
- //extern YY_BUFFER_STATE inStack[];
- 
--void getInput(char* buf, int& result, int max_size);
-+void getInput(char* buf, size_t& result, size_t max_size);
- void lexerIdMode();
- void lexerTokenTreeMode(int terminatingTokens);
- void lexerCmdMode();
diff --git a/lang/maude/files/patch-src_Core_dagNodeSet.hh b/lang/maude/files/patch-src_Core_dagNodeSet.hh
deleted file mode 100644
index 1967c371a489..000000000000
--- a/lang/maude/files/patch-src_Core_dagNodeSet.hh
+++ /dev/null
@@ -1,18 +0,0 @@
-./dagNodeSet.hh:35:15: error: ISO C++11 does not allow access declarations; use using
-      declarations instead
-  PointerSet::cardinality;
-              ^
-
---- src/Core/dagNodeSet.hh.orig	2018-08-27 20:49:56 UTC
-+++ src/Core/dagNodeSet.hh
-@@ -32,8 +32,8 @@ class DagNodeSet : private PointerSet
- public:
-   int insert(DagNode* d);
-   int dagNode2Index(DagNode* d) const;
--  PointerSet::cardinality;
--  PointerSet::makeEmpty;
-+  using PointerSet::cardinality;
-+  using PointerSet::makeEmpty;
-   DagNode* index2DagNode(int i) const;
- 
- private:
diff --git a/lang/maude/files/patch-src_Core_termSet.hh b/lang/maude/files/patch-src_Core_termSet.hh
deleted file mode 100644
index cbc6bbd1ab94..000000000000
--- a/lang/maude/files/patch-src_Core_termSet.hh
+++ /dev/null
@@ -1,19 +0,0 @@
-In file included from symbol.cc:41:
-In file included from ./term.hh:34:
-../../src/Core/termSet.hh:35:15: error: ISO C++11 does not allow access declarations; use using declarations instead
-  PointerSet::cardinality;
-              ^
-
---- src/Core/termSet.hh.orig	2018-08-27 20:47:58 UTC
-+++ src/Core/termSet.hh
-@@ -32,8 +32,8 @@ class TermSet : private PointerSet
- public:
-   void insert(Term* t);
-   int term2Index(Term* t) const;
--  PointerSet::cardinality;
--  PointerSet::makeEmpty;
-+  using PointerSet::cardinality;
-+  using PointerSet::makeEmpty;
- 
- private:
-   unsigned int hash(void* pointer) const;
diff --git a/lang/maude/files/patch-src_Meta_metaMatch.cc b/lang/maude/files/patch-src_Meta_metaMatch.cc
deleted file mode 100644
index 2b015926f455..000000000000
--- a/lang/maude/files/patch-src_Meta_metaMatch.cc
+++ /dev/null
@@ -1,11 +0,0 @@
---- src/Meta/metaMatch.cc.orig	2018-08-27 20:58:55 UTC
-+++ src/Meta/metaMatch.cc
-@@ -172,7 +172,7 @@ MetaLevelOpSymbol::makeMatchSearchState2(MetaModule* m
- 	    }
- 	}
-     }
--  return false;
-+  return NULL;
- }
- 
- bool
diff --git a/lang/maude/files/patch-src_Mixfix_banner.cc b/lang/maude/files/patch-src_Mixfix_banner.cc
new file mode 100644
index 000000000000..6de6794f32d3
--- /dev/null
+++ b/lang/maude/files/patch-src_Mixfix_banner.cc
@@ -0,0 +1,13 @@
+Make the build reproducible
+--- src/Mixfix/banner.cc.orig	2018-09-17 10:53:25 UTC
++++ src/Mixfix/banner.cc
+@@ -53,8 +53,7 @@ printBanner(std::ostream& s)
+     Tty(Tty::GREEN) << 'e' <<
+     Tty(Tty::RESET) << " ---\n";
+   s << "\t\t     /||||||||||||||||||\\\n";
+-  s << "\t   " << PACKAGE_STRING << " built: " <<
+-    __DATE__ << ' ' << __TIME__ << '\n';
++  s << "\t   " << PACKAGE_STRING << " built by FreeBSD ports\n";
+   s << "\t    Copyright 1997-2016 SRI International\n";
+   s << "\t\t   " << ctime(&secs);
+ }
diff --git a/lang/maude/files/patch-src_Mixfix_variableGenerator.cc b/lang/maude/files/patch-src_Mixfix_variableGenerator.cc
new file mode 100644
index 000000000000..a00361608c5e
--- /dev/null
+++ b/lang/maude/files/patch-src_Mixfix_variableGenerator.cc
@@ -0,0 +1,23 @@
+kind::IFF was removed in CVC4 1.6 
+--- src/Mixfix/variableGenerator.cc.orig	2018-09-17 10:44:35 UTC
++++ src/Mixfix/variableGenerator.cc
+@@ -312,18 +312,7 @@ VariableGenerator::dagToCVC4(DagNode* dag)
+ 	  //
+ 	case SMT_Symbol::EQUALS:
+ 	  {
+-	    //
+-	    //	Bizarrely CVC4 requires the IFF be used for Boolean equality so we need to
+-	    //	check the SMT type associated with our first argument sort to catch this case.
+-	    //
+-	    Sort* domainSort = s->getOpDeclarations()[0].getDomainAndRange()[0];
+-	    SMT_Info::SMT_Type smtType = smtInfo.getType(domainSort);
+-	    if (smtType == SMT_Info::NOT_SMT)
+-	      {
+-		IssueWarning("term " << QUOTE(dag) << " does not belong to an SMT sort.");
+-		goto fail;
+-	      }
+-	    return exprManager->mkExpr(((smtType == SMT_Info::BOOLEAN) ? kind::IFF : kind::EQUAL), exprs[0], exprs[1]);
++	    return exprManager->mkExpr(kind::EQUAL, exprs[0], exprs[1]);
+ 	  }
+ 	case SMT_Symbol::NOT_EQUALS:
+ 	  {
diff --git a/lang/maude/files/patch-src_ObjectSystem_socketStuff.cc b/lang/maude/files/patch-src_ObjectSystem_socketStuff.cc
index 4e930fe49627..fee0dab0be51 100644
--- a/lang/maude/files/patch-src_ObjectSystem_socketStuff.cc
+++ b/lang/maude/files/patch-src_ObjectSystem_socketStuff.cc
@@ -1,6 +1,6 @@
---- src/ObjectSystem/socketStuff.cc.orig	2018-08-27 20:56:09 UTC
+--- src/ObjectSystem/socketStuff.cc.orig	2018-09-17 10:38:45 UTC
 +++ src/ObjectSystem/socketStuff.cc
-@@ -219,7 +219,7 @@ SocketManagerSymbol::createServerTcpSocket(FreeDagNode
+@@ -230,7 +230,7 @@ SocketManagerSymbol::createServerTcpSocket(FreeDagNode
  	sockName.sin_family = AF_INET;
  	sockName.sin_port = htons(port);
  	sockName.sin_addr.s_addr = htonl(INADDR_ANY);  // HACK - what is the portable way to set this?
diff --git a/lang/maude/files/patch-src__BuiltIn__stringOpSymbol.cc b/lang/maude/files/patch-src__BuiltIn__stringOpSymbol.cc
deleted file mode 100644
index 252a2884f2e8..000000000000
--- a/lang/maude/files/patch-src__BuiltIn__stringOpSymbol.cc
+++ /dev/null
@@ -1,11 +0,0 @@
---- src/BuiltIn/stringOpSymbol.cc.orig	2008-09-12 01:03:36 UTC
-+++ src/BuiltIn/stringOpSymbol.cc
-@@ -472,7 +472,7 @@ StringOpSymbol::eqRewrite(DagNode* subject, RewritingC
- 		const mpz_class& n0 = succSymbol->getNat(a0);
- 		if (n0 <= 255)
- 		  {
--		    char c = n0.get_si();
-+		    char c[2] = { static_cast<char>(n0.get_si()), 0 };
- 		    return rewriteToString(subject, context, crope(c));
- 		  }
- 	      }
diff --git a/lang/maude/files/patch-src__Mixfix__bottom.yy b/lang/maude/files/patch-src__Mixfix__bottom.yy
deleted file mode 100644
index 5da5f16bd82f..000000000000
--- a/lang/maude/files/patch-src__Mixfix__bottom.yy
+++ /dev/null
@@ -1,11 +0,0 @@
---- ./src/Mixfix/bottom.yy.orig	2014-09-03 02:49:14.000000000 +0200
-+++ ./src/Mixfix/bottom.yy	2014-09-03 02:50:56.000000000 +0200
-@@ -23,7 +23,7 @@
- %%
- 
- static void
--yyerror(char *s)
-+yyerror(UserLevelRewritingContext::ParseResult *parseResult, char *s)
- {
-   if (!(UserLevelRewritingContext::interrupted()))
-     IssueWarning(LineNumber(lineNumber) << ": " << s);
diff --git a/lang/maude/files/patch-src__Mixfix__commands.yy b/lang/maude/files/patch-src__Mixfix__commands.yy
deleted file mode 100644
index c5ee2ba8312b..000000000000
--- a/lang/maude/files/patch-src__Mixfix__commands.yy
+++ /dev/null
@@ -1,17 +0,0 @@
---- ./src/Mixfix/commands.yy.orig	2014-09-03 02:51:54.000000000 +0200
-+++ ./src/Mixfix/commands.yy	2014-09-03 02:53:05.000000000 +0200
-@@ -23,12 +23,12 @@
- /*
-  *	Commands.
-  */
--command		:	KW_SELECT		{ lexBubble(END_COMMAND, 1) }
-+command		:	KW_SELECT		{ lexBubble(END_COMMAND, 1); }
- 			endBubble
- 			{
- 			  interpreter.setCurrentModule(lexerBubble);
- 			}
--		|	KW_DUMP			{ lexBubble(END_COMMAND, 1) }
-+		|	KW_DUMP			{ lexBubble(END_COMMAND, 1); }
- 			endBubble
- 			{
- 			  if (interpreter.setCurrentModule(lexerBubble))
diff --git a/lang/maude/files/patch-src__Mixfix__interact.cc b/lang/maude/files/patch-src__Mixfix__interact.cc
deleted file mode 100644
index e1b4925ceba5..000000000000
--- a/lang/maude/files/patch-src__Mixfix__interact.cc
+++ /dev/null
@@ -1,18 +0,0 @@
---- ./src/Mixfix/interact.cc.orig	2014-09-03 02:53:35.000000000 +0200
-+++ ./src/Mixfix/interact.cc	2014-09-03 02:54:14.000000000 +0200
-@@ -25,13 +25,14 @@
- //
- #include <signal.h>
- 
-+#include "surface.h"
-+
- bool UserLevelRewritingContext::interactiveFlag = true;
- bool UserLevelRewritingContext::ctrlC_Flag = false;
- bool UserLevelRewritingContext::stepFlag = false;
- bool UserLevelRewritingContext::abortFlag = false;
- int UserLevelRewritingContext::debugLevel = 0;
- 
--int yyparse(void*);
- void cleanUpParser();
- void cleanUpLexer();
- 
diff --git a/lang/maude/files/patch-src__Mixfix__modules.yy b/lang/maude/files/patch-src__Mixfix__modules.yy
deleted file mode 100644
index 370f3194d30a..000000000000
--- a/lang/maude/files/patch-src__Mixfix__modules.yy
+++ /dev/null
@@ -1,11 +0,0 @@
---- ./src/Mixfix/modules.yy.orig	2014-09-03 02:57:44.000000000 +0200
-+++ ./src/Mixfix/modules.yy	2014-09-03 02:58:03.000000000 +0200
-@@ -247,7 +247,7 @@
- 			  //	press on.
- 			  //
- 			  opDescription = lexerBubble;
--			  lexBubble(END_STATEMENT, 1)
-+			  lexBubble(END_STATEMENT, 1);
- 			}
- 			endBubble
- 			{
diff --git a/lang/maude/files/patch-src__Mixfix__token.cc b/lang/maude/files/patch-src__Mixfix__token.cc
deleted file mode 100644
index b32f6565b47f..000000000000
--- a/lang/maude/files/patch-src__Mixfix__token.cc
+++ /dev/null
@@ -1,11 +0,0 @@
---- ./src/Mixfix/token.cc.orig	2014-09-03 02:58:50.000000000 +0200
-+++ ./src/Mixfix/token.cc	2014-09-03 02:59:18.000000000 +0200
-@@ -632,7 +632,7 @@
- 	      }
- 	  }
- 	}
--      result.append(c);
-+      result.push_back(c);
-       seenBackslash = false;
-     }
-   CantHappen("bad end to string");
diff --git a/lang/maude/files/patch-src__Mixfix__top.yy b/lang/maude/files/patch-src__Mixfix__top.yy
deleted file mode 100644
index f95be50776fe..000000000000
--- a/lang/maude/files/patch-src__Mixfix__top.yy
+++ /dev/null
@@ -1,25 +0,0 @@
---- ./src/Mixfix/top.yy.orig	2014-09-03 03:00:02.000000000 +0200
-+++ ./src/Mixfix/top.yy	2014-09-03 03:02:15.000000000 +0200
-@@ -59,7 +59,6 @@
- #define store(token)		tokenSequence.append(token)
- #define fragClear()		fragments.contractTo(0);
- #define fragStore(token)	fragments.append(token)
--#define YYPARSE_PARAM	parseResult
- #define PARSE_RESULT	(*((UserLevelRewritingContext::ParseResult*) parseResult))
- 
- #define CM		interpreter.getCurrentModule()
-@@ -91,12 +90,13 @@
- Int64 number;
- Int64 number2;
- 
--static void yyerror(char *s);
-+static void yyerror(UserLevelRewritingContext::ParseResult *parseResult, char *s);
- 
- void cleanUpModuleExpression();
- void cleanUpParser();
- void missingSpace(const Token& token);
- %}
-+%parse-param { UserLevelRewritingContext::ParseResult *parseResult }
- %pure_parser
- 
- %union
diff --git a/lang/maude/files/patch-src__ObjectSystem__configSymbol.hh b/lang/maude/files/patch-src__ObjectSystem__configSymbol.hh
deleted file mode 100644
index 43d8a90e1774..000000000000
--- a/lang/maude/files/patch-src__ObjectSystem__configSymbol.hh
+++ /dev/null
@@ -1,11 +0,0 @@
---- ./src/ObjectSystem/configSymbol.hh.orig	2014-09-03 02:37:37.000000000 +0200
-+++ ./src/ObjectSystem/configSymbol.hh	2014-09-03 02:38:05.000000000 +0200
-@@ -50,7 +50,7 @@
- private:
-   struct symbolLt
-   {
--    bool operator()(const Symbol* d1, const Symbol* d2)
-+    bool operator()(const Symbol* d1, const Symbol* d2) const
-     {
-       return d1->compare(d2) < 0;
-     }
diff --git a/lang/maude/files/patch-src__ObjectSystem__objectMap.cc b/lang/maude/files/patch-src__ObjectSystem__objectMap.cc
deleted file mode 100644
index 29d4faa153d4..000000000000
--- a/lang/maude/files/patch-src__ObjectSystem__objectMap.cc
+++ /dev/null
@@ -1,11 +0,0 @@
---- ./src/ObjectSystem/objectMap.cc.orig	2014-09-03 02:39:09.000000000 +0200
-+++ ./src/ObjectSystem/objectMap.cc	2014-09-03 02:39:20.000000000 +0200
-@@ -50,7 +50,7 @@
- 
- struct ConfigSymbol::dagNodeLt
- {
--  bool operator()(const DagNode* d1, const DagNode* d2)
-+  bool operator()(const DagNode* d1, const DagNode* d2) const
-     {
-       return d1->compare(d2) < 0;
-     }
diff --git a/lang/maude/files/patch-src__ObjectSystem__objectSystemRewritingContext.hh b/lang/maude/files/patch-src__ObjectSystem__objectSystemRewritingContext.hh
deleted file mode 100644
index 84652ced73f4..000000000000
--- a/lang/maude/files/patch-src__ObjectSystem__objectSystemRewritingContext.hh
+++ /dev/null
@@ -1,11 +0,0 @@
---- ./src/ObjectSystem/objectSystemRewritingContext.hh.orig	2014-09-03 02:40:31.000000000 +0200
-+++ ./src/ObjectSystem/objectSystemRewritingContext.hh	2014-09-03 02:40:48.000000000 +0200
-@@ -62,7 +62,7 @@
- private:
-   struct dagNodeLt
-   {
--    bool operator()(const DagNode* d1, const DagNode* d2)
-+    bool operator()(const DagNode* d1, const DagNode* d2) const
-     {
-       return d1->compare(d2) < 0;
-     }
diff --git a/lang/maude/files/patch-src__Utility__ropeStuff.hh b/lang/maude/files/patch-src__Utility__ropeStuff.hh
deleted file mode 100644
index 5ba62e4d60a0..000000000000
--- a/lang/maude/files/patch-src__Utility__ropeStuff.hh
+++ /dev/null
@@ -1,20 +0,0 @@
---- ./src/Utility/ropeStuff.hh.orig	2014-09-03 02:27:15.000000000 +0200
-+++ ./src/Utility/ropeStuff.hh	2014-09-03 02:28:58.000000000 +0200
-@@ -25,6 +25,11 @@
- //
- #ifndef _ropeStuff_hh_
- #define _ropeStuff_hh_
-+#include <cstddef>
-+#ifdef _LIBCPP_VERSION
-+#include <string>
-+typedef std::string crope;
-+#else
- #ifdef __GNUC__
-   #if __GNUC__ < 3
-     #include <rope.h>
-@@ -50,3 +55,5 @@
- #include <rope>
- #endif
- #endif
-+
-+#endif
diff --git a/lang/maude/pkg-plist b/lang/maude/pkg-plist
index da6bfef82282..0c485f54844f 100644
--- a/lang/maude/pkg-plist
+++ b/lang/maude/pkg-plist
@@ -1,9 +1,10 @@
 bin/maude
-%%FULL_MAUDE%%%%DATADIR%%/full-maude%%FULL_MAUDE_VER%%.maude
+%%FULL_MAUDE%%%%DATADIR%%/full-maude.maude
 %%DATADIR%%/linear.maude
 %%DATADIR%%/machine-int.maude
 %%DATADIR%%/metaInterpreter.maude
 %%DATADIR%%/model-checker.maude
 %%DATADIR%%/prelude.maude
+%%CVC4%%%%DATADIR%%/smt.maude
 %%DATADIR%%/socket.maude
 %%DATADIR%%/term-order.maude