Bug 238376

Summary: math/cvc4: update to 1.7
Product: Ports & Packages Reporter: Greg V <greg>
Component: Individual Port(s)Assignee: Fernando Apesteguía <fernape>
Status: Closed FIXED    
Severity: Affects Only Me CC: fernape, greg
Priority: ---    
Version: Latest   
Hardware: Any   
OS: Any   
Attachments:
Description Flags
cvc4.patch
none
cvc4.patch v2
none
cvc4.patch v2 real
none
cvc4.patch v3
none
cvc4 patch v4
none
cvc4 patch v4
greg: maintainer-approval+
cvc4 patch v5 greg: maintainer-approval+

Description Greg V 2019-06-06 23:52:00 UTC
Created attachment 204867 [details]
cvc4.patch

New build system, new problems :)

This still needs some QA, but seems to work so far. I'm building openjdk8 on aarch64 to test this on there. Haven't tested in synth either yet.
Comment 1 Fernando Apesteguía freebsd_committer 2019-06-12 17:27:52 UTC
(In reply to Greg V from comment #0)
Hi Greg,

I can not build the port. It fails to configure:

-- Configuring with C flag '-pthread'
-- Configuring with CXX flag '-pthread'
-- Configuring with C flag '-pthread'
-- Configuring with CXX flag '-pthread'
-- Found CryptoMiniSat: /usr/local/include  
-- Found CryptoMiniSat libs: /usr/local/lib/libcryptominisat5.so
CMake Error at cmake/FindReadline.cmake:38 (message):
  Could not link against readline.  Check CMakeError.log for more details
Call Stack (most recent call first):
  CMakeLists.txt:435 (find_package)

Could you have a look?
Comment 2 Greg V 2019-07-25 14:14:23 UTC
Created attachment 206060 [details]
cvc4.patch v2

Added readline:port, added /bin/bash fix. Tested on aarch64.
Comment 3 Fernando Apesteguía freebsd_committer 2019-07-25 15:35:40 UTC
(In reply to Greg V from comment #2)
Thanks for the update, Greg

Can you try and apply it to a recent copy of the port? The patch doesn't apply cleanly to my recently updated svn checkout. It rejects many changes in the port Makefile.

Thanks!
Comment 4 Greg V 2019-07-25 20:07:48 UTC
Created attachment 206064 [details]
cvc4.patch v2 real

sorry, diffed against wrong remote
Comment 5 Fernando Apesteguía freebsd_committer 2019-07-28 17:09:55 UTC
Thanks again for the update Greg.

This one seems to build fine. I tested other ports that depend on math/cvc4, namely lang/solidity and lang/maude and sadly they don't build with this new version. For instance, solidity fails with this error:

In file included from /wrkdirs/usr/ports/lang/solidity/work/solidity_0.5.10/libsolidity/formal/SMTPortfolio.cpp:24:
In file included from /wrkdirs/usr/ports/lang/solidity/work/solidity_0.5.10/libsolidity/formal/CVC4Interface.h:30:
In file included from /usr/local/include/cvc4/cvc4.h:21:
/usr/local/include/cvc4/base/configuration.h:19:10: fatal error: 'cvc4_public.h' file not found
#include "cvc4_public.h"

Certainly, tries to include cvc4_public.h assuming it is in the same directory while it is not:

root@12_0amd64-default:~ # cd /usr/local/include/cvc4/base
root@12_0amd64-default:/usr/local/include/cvc4/base # grep cvc4_public.h configuration.h 
#include "cvc4_public.h"
root@12_0amd64-default:/usr/local/include/cvc4/base # ls cvc4_public.h
ls: cvc4_public.h: No such file or directory
root@12_0amd64-default:/usr/local/include/cvc4/base # ls ../cvc4_public.h
../cvc4_public.h
root@12_0amd64-default:/usr/local/include/cvc4/base # 

This is a change from the previous version:

root@12_0amd64-default:/usr/local/include/cvc4/base # pkg help info
root@12_0amd64-default:/usr/local/include/cvc4/base # pkg info cvc4 | grep Version
Version        : 1.6_5
root@12_0amd64-default:/usr/local/include/cvc4/base # grep cvc4_public.h configuration.h 
#include <cvc4/cvc4_public.h>
root@12_0amd64-default:/usr/local/include/cvc4/base # ls ../cvc4_public.h 
../cvc4_public.h
root@12_0amd64-default:/usr/local/include/cvc4/base # 

lang/maude fails in a similar way.

Could you have a look at this?

Thanks!
Comment 6 Greg V 2019-07-28 17:38:55 UTC
(In reply to Fernando Apesteguía from comment #5)
oops..

now building with the following added to post-patch:

	@${REINPLACE_CMD} -e "s|sed -i 's|sed -ibak 's|g" \
		${WRKSRC}/src/fix-install-headers.sh

basically, CMake is supposed to call that script when installing to fix the includes. That script is using -i without an extension like GNU sed allows. I think CMake was letting it fail silently (not aborting the build).
Comment 7 Greg V 2019-07-28 18:33:39 UTC
Created attachment 206129 [details]
cvc4.patch v3

argh, the cmake file was also not respecting DESTDIR, and the script was called on the real /usr/local instead of staging
Comment 8 Fernando Apesteguía freebsd_committer 2019-07-30 15:00:46 UTC
(In reply to Greg V from comment #7)

Issues in pkg-plist :-(

Error: Orphaned: include/cvc4/api/cvc4cpp.hbak
Error: Orphaned: include/cvc4/api/cvc4cppkind.hbak
Error: Orphaned: include/cvc4/base/configuration.hbak
Error: Orphaned: include/cvc4/base/exception.hbak
Error: Orphaned: include/cvc4/base/listener.hbak
Error: Orphaned: include/cvc4/base/modal_exception.hbak
Error: Orphaned: include/cvc4/context/cdhashmap_forward.hbak
Error: Orphaned: include/cvc4/context/cdhashset_forward.hbak
Error: Orphaned: include/cvc4/context/cdinsert_hashmap_forward.hbak
Error: Orphaned: include/cvc4/context/cdlist_forward.hbak
...
...

Will you check, please?

I assume you're not using poudriere?
Comment 9 Greg V 2019-07-30 15:07:12 UTC
(In reply to Fernando Apesteguía from comment #8)
Yes. That's not really an issue, that's some backup junk files, it's fine that they're orphaned
Comment 10 Fernando Apesteguía freebsd_committer 2019-07-30 15:43:16 UTC
Created attachment 206158 [details]
cvc4 patch v4

New patch.
Comment 11 Greg V 2019-07-30 15:46:39 UTC
(In reply to Fernando Apesteguía from comment #10)

> Usage: svndiff [OPTIONS] <file1> <file2>

That doesn't look right :)
Comment 12 Fernando Apesteguía freebsd_committer 2019-07-30 15:49:20 UTC
Created attachment 206159 [details]
cvc4 patch v4

Attaching proper file.
Comment 13 Greg V 2019-07-30 15:55:06 UTC
Comment on attachment 206159 [details]
cvc4 patch v4

hm, getting rid of bash and using sh worked fine for me, but that's not important, looks fine.
Comment 14 Fernando Apesteguía freebsd_committer 2019-07-30 16:06:09 UTC
Without the dependency on bash, in a *clean* environment:

env: bash: No such file or directory
[6/465] cd /wrkdirs/usr/ports/math/cvc4/work/.build/src/expr && /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/mkexpr /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7
/src/expr/type_checker_template.cpp /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/builtin/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/boolean
s/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/uf/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/kinds /wrkdirs/usr/ports/math/cvc4
/work/CVC4-1.7/src/theory/bv/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/fp/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arrays/kinds 
/wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/datatypes/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/sep/kinds /wrkdirs/usr/ports/math/cvc4/wo
rk/CVC4-1.7/src/theory/sets/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/strings/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifie
rs/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/idl/kinds > /wrkdirs/usr/ports/math/cvc4/work/.build/src/expr/type_checker.cpp
FAILED: src/expr/type_checker.cpp 
cd /wrkdirs/usr/ports/math/cvc4/work/.build/src/expr && /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/mkexpr /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/exp
r/type_checker_template.cpp /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/builtin/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/booleans/kinds 
/wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/uf/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/kinds /wrkdirs/usr/ports/math/cvc4/work/CV
C4-1.7/src/theory/bv/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/fp/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arrays/kinds /wrkdirs
/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/datatypes/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/sep/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-
1.7/src/theory/sets/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/strings/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/kinds
 /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/idl/kinds > /wrkdirs/usr/ports/math/cvc4/work/.build/src/expr/type_checker.cpp
env: bash: No such file or directory
[7/465] cd /wrkdirs/usr/ports/math/cvc4/work/.build/src/expr && /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/mkmetakind /wrkdirs/usr/ports/math/cvc4/work/CVC4
-1.7/src/expr/metakind_template.h /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/builtin/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/booleans/
kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/uf/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/kinds /wrkdirs/usr/ports/math/cvc4/w
ork/CVC4-1.7/src/theory/bv/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/fp/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arrays/kinds /w
rkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/datatypes/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/sep/kinds /wrkdirs/usr/ports/math/cvc4/work
/CVC4-1.7/src/theory/sets/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/strings/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers
/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/idl/kinds > /wrkdirs/usr/ports/math/cvc4/work/.build/src/expr/metakind.h
FAILED: src/expr/metakind.h 
cd /wrkdirs/usr/ports/math/cvc4/work/.build/src/expr && /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/expr/mkmetakind /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src
/expr/metakind_template.h /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/builtin/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/booleans/kinds /w
rkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/uf/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arith/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4
-1.7/src/theory/bv/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/fp/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/arrays/kinds /wrkdirs/u
sr/ports/math/cvc4/work/CVC4-1.7/src/theory/datatypes/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/sep/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.
7/src/theory/sets/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/strings/kinds /wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/quantifiers/kinds /
wrkdirs/usr/ports/math/cvc4/work/CVC4-1.7/src/theory/idl/kinds > /wrkdirs/usr/ports/math/cvc4/work/.build/src/expr/metakind.h
env: bash: No such file or directory
...
...
Comment 15 Greg V 2019-07-30 16:13:41 UTC
(In reply to Fernando Apesteguía from comment #14)

hm, that is supposed to be eliminated by the

	@${REINPLACE_CMD} -e 's|^#!/bin/bash|#!/bin/sh|g' \
		${WRKSRC}/doc/*.sh ${WRKSRC}/src/base/mk* ${WRKSRC}/src/options/*.sh
Comment 16 Fernando Apesteguía freebsd_committer 2019-07-31 17:53:00 UTC
(In reply to Greg V from comment #15)
It does but there are other scripts which use bash in these directories:

contrib/
src/
src/expr/
src/theory/
test/regress/regress0/uf/

Some of those scripts are actually bash specific (they use things like BASH_LINENO, PIPESTATUS, etc..)

So I truly think we need bash as a build dependency (see also INSTALL.md regarding this).

New version attached.
Comment 17 Fernando Apesteguía freebsd_committer 2019-07-31 17:53:57 UTC
Created attachment 206182 [details]
cvc4 patch v5
Comment 18 Fernando Apesteguía freebsd_committer 2019-08-01 15:23:33 UTC
Commited in r507774

https://svnweb.freebsd.org/ports?view=revision&revision=507774

Thanks!
Comment 19 Jan Beich freebsd_committer 2019-08-04 02:00:45 UTC
Do you plan to fix lang/maude and lang/solidity? If not mark as BROKEN to avoid wasting cycles as well as give users a hint where/how to look for a fix.

https://pkg-status.freebsd.org/builds/default:default:112amd64:507931:beefy9#new_failed
Comment 20 Fernando Apesteguía freebsd_committer 2019-08-04 09:38:50 UTC
(In reply to Jan Beich from comment #19)

I'll fix them ASAP.

Thanks!
Comment 21 commit-hook freebsd_committer 2019-08-05 17:00:25 UTC
A commit references this bug:

Author: fernape
Date: Mon Aug  5 16:59:26 UTC 2019
New revision: 508195
URL: https://svnweb.freebsd.org/changeset/ports/508195

Log:
  math/cvc4: Fix headers

  Fix headers so other programs can include them safely.

  This unbreaks lang/maude and lang/solidity

  PR:	238376
  Reported by:	jbeich@

Changes:
  head/math/cvc4/Makefile
Comment 22 Fernando Apesteguía freebsd_committer 2019-08-05 17:00:56 UTC
Done.

Thanks!