pkgsrc-Changes-HG archive

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index][Old Index]

[pkgsrc/trunk]: pkgsrc/lang/maude Update to Maude 2.4



details:   https://anonhg.NetBSD.org/pkgsrc/rev/4d7cc2dd4381
branches:  trunk
changeset: 575650:4d7cc2dd4381
user:      asau <asau%pkgsrc.org@localhost>
date:      Wed May 19 11:55:43 2010 +0000

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

 lang/maude/Makefile |  11 +++++++----
 lang/maude/PLIST    |   4 +---
 lang/maude/distinfo |   8 ++++----
 3 files changed, 12 insertions(+), 11 deletions(-)

diffs (68 lines):

diff -r 306b1a7d0d8f -r 4d7cc2dd4381 lang/maude/Makefile
--- a/lang/maude/Makefile       Wed May 19 11:48:39 2010 +0000
+++ b/lang/maude/Makefile       Wed May 19 11:55:43 2010 +0000
@@ -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 @@
 MAINTAINER=    kristerw%NetBSD.org@localhost
 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 @@
 
 .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 -r 306b1a7d0d8f -r 4d7cc2dd4381 lang/maude/PLIST
--- a/lang/maude/PLIST  Wed May 19 11:48:39 2010 +0000
+++ b/lang/maude/PLIST  Wed May 19 11:55:43 2010 +0000
@@ -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 -r 306b1a7d0d8f -r 4d7cc2dd4381 lang/maude/distinfo
--- a/lang/maude/distinfo       Wed May 19 11:48:39 2010 +0000
+++ b/lang/maude/distinfo       Wed May 19 11:55:43 2010 +0000
@@ -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



Home | Main Index | Thread Index | Old Index