[arch-commits] Commit in maude/trunk (PKGBUILD maude-cvc4-1.5.patch)

[Felix Yan via arch-commits]

Date: Saturday, February 29, 2020 @ 08:53:47
  Author: felixonmars
Revision: 586806

upgpkg: maude 3.0-1

Modified:
  maude/trunk/PKGBUILD
Deleted:
  maude/trunk/maude-cvc4-1.5.patch

--+
 PKGBUILD |   25 +++--
 maude-cvc4-1.5.patch |   24 
 2 files changed, 11 insertions(+), 38 deletions(-)

Modified: PKGBUILD
===
--- PKGBUILD2020-02-29 08:34:37 UTC (rev 586805)
+++ PKGBUILD2020-02-29 08:53:47 UTC (rev 586806)
@@ -4,32 +4,29 @@
 # Contributor: Stefan Husmann 
 
 pkgname=maude
-pkgver=2.7.1
-pkgrel=3
+pkgver=3.0
+pkgrel=1
 pkgdesc="High-level Specification Language"
 arch=('x86_64')
-url="http://maude.cs.uiuc.edu;
+url="http://maude.cs.illinois.edu;
 license=('GPL')
 depends=('buddy' 'cvc4' 'libtecla' 'gmp' 'libsigsegv')
 makedepends=('flex' 'bison')
-source=("http://maude.cs.illinois.edu/w/images/d/d8/Maude-$pkgver.tar.gz;
-"http://maude.cs.illinois.edu/w/images/c/ca/Full-Maude-$pkgver.zip;
-maude.sh maude-cvc4-1.5.patch)
-sha512sums=('b4f172c679959a4c3386003f174a5938690926accd750ae2f5dcf945321a359d0428cf78d66ced9a560610a9cff5dae51f938542049e106c5f8bcba55c10f1a9'
-
'19a665408db13ee60ffdd47d156ba8572a7f23fd51efac5b6dbc2922d022dd4c687541e59c94eb6ec6b27eb7e7b5ef5245409ae50775a15dfd663d98e106f805'
-
'f62e1709d035e996c9f9a887840492527415f157990cc2d52355d8a7fe9382a757c06bed95f97e298f8eea0dd2a846bf7efb8fb84987784a4a797820807be12e'
-
'87c50ee550bb5e8644dbc8b6b598bab1c74fa4f65d29b23b1d073b0844f879e1e314a8f2e7e72f1b8138f41c07ac92b0e98b50396909f77620987daaccb898a7')
+source=("http://maude.cs.illinois.edu/w/images/9/92/Maude-$pkgver.tar.gz;
+"http://maude.cs.illinois.edu/w/images/0/04/Full-Maude-$pkgver.zip;
+maude.sh)
+sha512sums=('9f27a045da931c38536e27e7f046a518714fe80b4cb37749c9a4e6a5c5c7b94d111398037c03a50953294762360219d23e96f34e0e6c904bf0e5aff3b3473324'
+
'10b9b8085ac2f40f2ce9a1430ff93d2e4454e82c1fec8857ca10108da4705929b17da557db9ea3afbfd88c05a9f7bd89a79490988fa03c132aa79e4f5dc8f431'
+
'f62e1709d035e996c9f9a887840492527415f157990cc2d52355d8a7fe9382a757c06bed95f97e298f8eea0dd2a846bf7efb8fb84987784a4a797820807be12e')
 
 prepare() {
   cd "$srcdir/maude-$pkgver"
   autoreconf -i
-
-  patch -p1 -i ../maude-cvc4-1.5.patch # Fix build with CVC4 1.5
 }
 
 build() {
   cd "$srcdir/maude-$pkgver"
-  ./configure --prefix=/usr --datadir=/usr/share/maude
+  ./configure --with-cvc4=yes --with-yices2=no --prefix=/usr 
--datadir=/usr/share/maude
   make -j1 all CVC4_LIB="-lcvc4 -lcln"
 }
 
@@ -41,7 +38,7 @@
 package() {
   cd "$srcdir/maude-$pkgver"
   make DESTDIR="$pkgdir/" install
-  install -D -m 444 "$srcdir/full-maude.maude" \
+  install -D -m 444 "$srcdir/full-maude3.maude" \
 "$pkgdir/usr/share/maude/full-maude.maude"
 
   install -D -m 555 "$srcdir/maude.sh" "$pkgdir/etc/profile.d/maude.sh"

Deleted: maude-cvc4-1.5.patch
===
--- maude-cvc4-1.5.patch2020-02-29 08:34:37 UTC (rev 586805)
+++ maude-cvc4-1.5.patch2020-02-29 08:53:47 UTC (rev 586806)
@@ -1,24 +0,0 @@
-diff --git a/src/Mixfix/variableGenerator.cc b/src/Mixfix/variableGenerator.cc
-index 4761dfc..086b4ee 100755
 a/src/Mixfix/variableGenerator.cc
-+++ b/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:
- {

[arch-commits] Commit in maude/trunk (PKGBUILD maude-cvc4-1.5.patch)

[Antonio Rojas via arch-commits]

Date: Friday, January 12, 2018 @ 19:28:57
  Author: arojas
Revision: 281691

Rebuild with CVC4 1.5 (FS#57069)

Added:
  maude/trunk/maude-cvc4-1.5.patch
Modified:
  maude/trunk/PKGBUILD

--+
 PKGBUILD |9 ++---
 maude-cvc4-1.5.patch |   24 
 2 files changed, 30 insertions(+), 3 deletions(-)

Modified: PKGBUILD
===
--- PKGBUILD2018-01-12 18:58:06 UTC (rev 281690)
+++ PKGBUILD2018-01-12 19:28:57 UTC (rev 281691)
@@ -6,7 +6,7 @@
 
 pkgname=maude
 pkgver=2.7.1
-pkgrel=1
+pkgrel=2
 pkgdesc="High-level Specification Language"
 arch=('x86_64')
 url="http://maude.cs.uiuc.edu;
@@ -15,14 +15,17 @@
 makedepends=('flex' 'bison')
 source=("http://maude.cs.illinois.edu/w/images/d/d8/Maude-$pkgver.tar.gz;
 "http://maude.cs.illinois.edu/w/images/c/ca/Full-Maude-$pkgver.zip;
-maude.sh)
+maude.sh maude-cvc4-1.5.patch)
 md5sums=('aa31753f742f976940c69aa699c3d0ec'
  'b365fe0fdd161880e95aeb089f166657'
- '0a51738365579574b40a3d32da6f3291')
+ '0a51738365579574b40a3d32da6f3291'
+ '9e759db427d9d6e77d35cc56b7690e0b')
 
 prepare() {
   cd "$srcdir/maude-$pkgver"
   autoreconf -i
+
+  patch -p1 -i ../maude-cvc4-1.5.patch # Fix build with CVC4 1.5
 }
 
 build() {

Added: maude-cvc4-1.5.patch
===
--- maude-cvc4-1.5.patch(rev 0)
+++ maude-cvc4-1.5.patch2018-01-12 19:28:57 UTC (rev 281691)
@@ -0,0 +1,24 @@
+diff --git a/src/Mixfix/variableGenerator.cc b/src/Mixfix/variableGenerator.cc
+index 4761dfc..086b4ee 100755
+--- a/src/Mixfix/variableGenerator.cc
 b/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:
+ {