summaryrefslogtreecommitdiff
path: root/lang/maude
diff options
context:
space:
mode:
authorasau <asau>2010-05-19 11:55:43 +0000
committerasau <asau>2010-05-19 11:55:43 +0000
commit1dbbc8b23308adf9bbcc3e43e9b7f507b29e38ac (patch)
tree60aaef2f92cc3c939bd85660c39f483ec4680296 /lang/maude
parent516c082a70ef870d6c133d59467a365b9885809a (diff)
downloadpkgsrc-1dbbc8b23308adf9bbcc3e43e9b7f507b29e38ac.tar.gz
Update to Maude 2.4
================================== New features and changes since 2.3 ================================== (1) Maude 2.4 provides an order-sorted Ax-unification algorithm for all order-sorted theories (CSigma, E U Ax) such that: - the signature Sigma is preregular modulo Ax; - the axioms Ax associated to function symbols are as follows: - there can be arbitrary function symbols and constants with no equational attributes; - the iter equational attribute can be declared for some unary symbols; - the comm or assoc comm attributes can be declared for some binary function symbols, but then no other equational attributes must be given for such symbols. Explicitly excluded are theories with binary function symbols having either: (i) the id:, left id:, or right id: attributes; or (ii) the assoc attribute without the comm one; or (iii) a combination of (i) and (ii). (2) Unification is reflected in the META-LEVEL module by two descent functions: op metaUnify : Module UnificationProblem Nat Nat ~> UnificationPair? [special (...)]. op metaDisjointUnify : Module UnificationProblem Nat Nat ~> UnificationTriple? [special (...)]. (3) Statements (rule, equations and membership axioms) can now take a print attribute. In print attribute mode, when a statement is executed the items in its print attribute are printed, with variables taking their value in the current substitution. (4) Parsing of file names in the commands load, in, cd and pushd now allows spaces using either of two syntactic conventions: If the file name starts with " then all following characters will be taken literally up to the terminating ", line feed or form feed. If a file name starts with other than ", the following escape sequences are recognized \\ becomes \ \<space> becomes <space> \" becomes " (5) For operators in the C, CU, CI and CUI theories, if both arguments are the same, the rewrite, srewrite and search commands and the model checker will only consider one of the arguments for that step since only one rewriting step is made per pass, the choice of argument is irrelevant. This already happened for operators in the AC and ACU theories. The frewrite command still always considers all arguments even if they are identical since multiple rewriting steps can happen in each pass. (6) The GNU libsigsegv library is used to distinguigh between true segmentation faults and stack overflows and so stack overflows are now reported with an informative message. (7) Several optimizations, bug fixes and improvements.
Diffstat (limited to 'lang/maude')
-rw-r--r--lang/maude/Makefile11
-rw-r--r--lang/maude/PLIST4
-rw-r--r--lang/maude/distinfo8
3 files changed, 12 insertions, 11 deletions
diff --git a/lang/maude/Makefile b/lang/maude/Makefile
index d641078c17b..c55a5c3f1e2 100644
--- a/lang/maude/Makefile
+++ b/lang/maude/Makefile
@@ -1,9 +1,9 @@
-# $NetBSD: Makefile,v 1.22 2010/03/24 19:43:25 asau Exp $
+# $NetBSD: Makefile,v 1.23 2010/05/19 11:55:43 asau Exp $
#
-DISTNAME= Maude-2.3
-PKGNAME= maude-2.3
-PKGREVISION= 1
+DISTNAME= Maude-2.4
+PKGNAME= maude-2.4
+#PKGREVISION= 1
CATEGORIES= lang
MASTER_SITES= http://maude.cs.uiuc.edu/download/ \
http://maude.cs.uiuc.edu/download/current/
@@ -11,11 +11,13 @@ MASTER_SITES= http://maude.cs.uiuc.edu/download/ \
MAINTAINER= kristerw@NetBSD.org
HOMEPAGE= http://maude.cs.uiuc.edu/
COMMENT= System for equational and rewriting logic specification/programming
+LICENSE= gnu-gpl-v2
PKG_DESTDIR_SUPPORT= user-destdir
MAKE_JOBS_SAFE= no
GNU_CONFIGURE= YES
+CONFIGURE_ARGS= --datadir=$(PREFIX)/share/$(PKGBASE)
USE_LANGUAGES= c c++
USE_TOOLS+= flex bison
AUTO_MKDIRS= yes
@@ -26,5 +28,6 @@ post-install:
.include "../../devel/buddy/buildlink3.mk"
.include "../../devel/gmp/buildlink3.mk"
+.include "../../devel/libsigsegv/buildlink3.mk"
.include "../../devel/libtecla/buildlink3.mk"
.include "../../mk/bsd.pkg.mk"
diff --git a/lang/maude/PLIST b/lang/maude/PLIST
index 32223ac0b87..dc84786818f 100644
--- a/lang/maude/PLIST
+++ b/lang/maude/PLIST
@@ -1,10 +1,8 @@
-@comment $NetBSD: PLIST,v 1.6 2009/06/14 18:03:36 joerg Exp $
+@comment $NetBSD: PLIST,v 1.7 2010/05/19 11:55:43 asau Exp $
bin/maude
share/maude/linear.maude
share/maude/machine-int.maude
share/maude/model-checker.maude
-share/maude/model-checker.maude
-share/maude/prelude.maude
share/maude/prelude.maude
share/maude/socket.maude
share/maude/term-order.maude
diff --git a/lang/maude/distinfo b/lang/maude/distinfo
index 5ee8b3cfaf8..4ff270147ae 100644
--- a/lang/maude/distinfo
+++ b/lang/maude/distinfo
@@ -1,7 +1,7 @@
-$NetBSD: distinfo,v 1.7 2007/12/01 13:15:55 rillig Exp $
+$NetBSD: distinfo,v 1.8 2010/05/19 11:55:43 asau Exp $
-SHA1 (Maude-2.3.tar.gz) = 68fbe7f76db1a5a5bb748cb751c5015d60c476d0
-RMD160 (Maude-2.3.tar.gz) = 8c6b67d257468b4910631f4d6d0f2c3a0ff8d995
-Size (Maude-2.3.tar.gz) = 1441239 bytes
+SHA1 (Maude-2.4.tar.gz) = fe6c11a9ba370175eb477aad4042f2f0ef8cce7e
+RMD160 (Maude-2.4.tar.gz) = dae6357386cb4f4a683fd23aa32580f29a013f82
+Size (Maude-2.4.tar.gz) = 1528771 bytes
SHA1 (patch-ab) = ff1caa60e4b57dd6a847e28d25efa9be8474f15a
SHA1 (patch-ac) = d77e8e817cb33c2594eacfa0cb44b20b63e71b8f