- 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>
This commit is contained in:
Li-Wen Hsu 2018-12-12 05:30:24 +00:00
parent 4029496b46
commit c07192f844
Notes: svn2git 2021-03-31 03:12:20 +00:00
svn path=/head/; revision=487278
21 changed files with 61 additions and 248 deletions

View file

@ -2,13 +2,12 @@
# $FreeBSD$ # $FreeBSD$
PORTNAME= maude PORTNAME= maude
PORTVERSION= 2.6 PORTVERSION= 2.7.1
PORTREVISION= 1
CATEGORIES= lang 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} DISTNAME= Maude-${PORTVERSION}
MAINTAINER= ports@FreeBSD.org MAINTAINER= greg@unrelenting.technology
COMMENT= High-performance reflective language COMMENT= High-performance reflective language
LICENSE= GPLv2 LICENSE= GPLv2
@ -21,28 +20,32 @@ LIB_DEPENDS= libbdd.so:science/buddy \
libsigsegv.so:devel/libsigsegv libsigsegv.so:devel/libsigsegv
USES= alias autoreconf bison ncurses USES= alias autoreconf bison ncurses
WRKSRC= ${WRKDIR}/maude-${PORTVERSION}
GNU_CONFIGURE= yes GNU_CONFIGURE= yes
CPPFLAGS+= -I${NCURSESINC} -I${LOCALBASE}/include CPPFLAGS+= -I${NCURSESINC} -I${LOCALBASE}/include
LDFLAGS+= -L${NCURSESLIB} -L${LOCALBASE}/lib LDFLAGS+= -L${NCURSESLIB} -L${LOCALBASE}/lib
CONFIGURE_ARGS= --datadir=${DATADIR} CONFIGURE_ARGS= --datadir=${DATADIR}
MAKE_JOBS_UNSAFE= yes 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 CVC4_LIB_DEPENDS= libcvc4.so:math/cvc4
OPTIONS_DEFAULT= FULL_MAUDE CVC4_CONFIGURE_WITH= cvc4
FULL_MAUDE_DESC= Install full-maude${FULL_MAUDE_VER}
PORTDOCS= AUTHORS COPYING ChangeLog INSTALL NEWS README PORTDOCS= AUTHORS COPYING ChangeLog INSTALL NEWS README
BROKEN_aarch64= Fails to link: missing sbrk
.include <bsd.port.options.mk> .include <bsd.port.options.mk>
.if ${PORT_OPTIONS:MFULL_MAUDE} .if ${PORT_OPTIONS:MFULL_MAUDE}
MASTER_SITES+= http://maude.lcc.uma.es/FullMaude/FM${FULL_MAUDE_VER}/:fm MASTER_SITES+= http://maude.cs.illinois.edu/w/images/c/ca/:fm
FULL_MAUDE= full-maude${FULL_MAUDE_VER}.maude FULL_MAUDE= full-maude.maude
FULL_MAUDE_DIST= full-maude.maude.zip FULL_MAUDE_DIST= Full-Maude-${PORTVERSION}.zip
DISTFILES= ${DISTNAME}${EXTRACT_SUFX} ${FULL_MAUDE_DIST}:fm DISTFILES= ${DISTNAME}${EXTRACT_SUFX} ${FULL_MAUDE_DIST}:fm
EXTRACT_ONLY= ${DISTNAME}${EXTRACT_SUFX} EXTRACT_ONLY= ${DISTNAME}${EXTRACT_SUFX}
EXTRACT_DEPENDS+= ${LOCALBASE}/bin/unzip:archivers/unzip EXTRACT_DEPENDS+= ${LOCALBASE}/bin/unzip:archivers/unzip

View file

@ -1,5 +1,5 @@
TIMESTAMP = 1478641858 TIMESTAMP = 1537177216
SHA256 (Maude-2.6.tar.gz) = a5ba79bf3d30565c874e80b3531b51a7e835b600e86cac82508a6eb9e15f4aa0 SHA256 (Maude-2.7.1.tar.gz) = b1887c7fa75e85a1526467727242f77b5ec7cd6a5dfa4ceb686b6f545bb1534b
SIZE (Maude-2.6.tar.gz) = 1600026 SIZE (Maude-2.7.1.tar.gz) = 1853963
SHA256 (full-maude.maude.zip) = 57ebfc41056b7afc2be48983f6a1311e817d23eeaaed71023471bc4edaf6b128 SHA256 (Full-Maude-2.7.1.zip) = 4c3a11b053ea92df4cfe89939a97c6b02c68489b174eb689c844c08decb18f78
SIZE (full-maude.maude.zip) = 154881 SIZE (Full-Maude-2.7.1.zip) = 156771

View file

@ -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();

View file

@ -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:

View file

@ -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;

View file

@ -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

View file

@ -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);
}

View file

@ -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:
{

View file

@ -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 +++ 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_family = AF_INET;
sockName.sin_port = htons(port); sockName.sin_port = htons(port);
sockName.sin_addr.s_addr = htonl(INADDR_ANY); // HACK - what is the portable way to set this? sockName.sin_addr.s_addr = htonl(INADDR_ANY); // HACK - what is the portable way to set this?

View file

@ -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));
}
}

View file

@ -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);

View file

@ -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))

View file

@ -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();

View file

@ -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
{

View file

@ -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");

View file

@ -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

View file

@ -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;
}

View file

@ -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;
}

View file

@ -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;
}

View file

@ -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

View file

@ -1,9 +1,10 @@
bin/maude bin/maude
%%FULL_MAUDE%%%%DATADIR%%/full-maude%%FULL_MAUDE_VER%%.maude %%FULL_MAUDE%%%%DATADIR%%/full-maude.maude
%%DATADIR%%/linear.maude %%DATADIR%%/linear.maude
%%DATADIR%%/machine-int.maude %%DATADIR%%/machine-int.maude
%%DATADIR%%/metaInterpreter.maude %%DATADIR%%/metaInterpreter.maude
%%DATADIR%%/model-checker.maude %%DATADIR%%/model-checker.maude
%%DATADIR%%/prelude.maude %%DATADIR%%/prelude.maude
%%CVC4%%%%DATADIR%%/smt.maude
%%DATADIR%%/socket.maude %%DATADIR%%/socket.maude
%%DATADIR%%/term-order.maude %%DATADIR%%/term-order.maude