diff --git a/lang/maude/Makefile b/lang/maude/Makefile index ff59506a7b4e..735d0c7b6972 100644 --- a/lang/maude/Makefile +++ b/lang/maude/Makefile @@ -2,13 +2,13 @@ # $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} +WRKSRC= ${WRKDIR}/maude-${PORTVERSION} -MAINTAINER= ports@FreeBSD.org +MAINTAINER= greg@unrelenting.technology COMMENT= High-performance reflective language LICENSE= GPLv2 @@ -27,22 +27,23 @@ 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 .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(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 - -+#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 -+#ifdef _LIBCPP_VERSION -+#include -+typedef std::string crope; -+#else - #ifdef __GNUC__ - #if __GNUC__ < 3 - #include -@@ -50,3 +55,5 @@ - #include - #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