Summary: | math/cvc4: update to 1.7 | ||||||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Product: | Ports & Packages | Reporter: | Val Packett <val> | ||||||||||||||||
Component: | Individual Port(s) | Assignee: | Fernando Apesteguía <fernape> | ||||||||||||||||
Status: | Closed FIXED | ||||||||||||||||||
Severity: | Affects Only Me | CC: | fernape, val | ||||||||||||||||
Priority: | --- | ||||||||||||||||||
Version: | Latest | ||||||||||||||||||
Hardware: | Any | ||||||||||||||||||
OS: | Any | ||||||||||||||||||
Attachments: |
|
(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? Created attachment 206060 [details]
cvc4.patch v2
Added readline:port, added /bin/bash fix. Tested on aarch64.
(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! Created attachment 206064 [details]
cvc4.patch v2 real
sorry, diffed against wrong remote
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! (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). 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
(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? (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 Created attachment 206158 [details]
cvc4 patch v4
New patch.
(In reply to Fernando Apesteguía from comment #10) > Usage: svndiff [OPTIONS] <file1> <file2> That doesn't look right :) Created attachment 206159 [details]
cvc4 patch v4
Attaching proper file.
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.
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 ... ... (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 (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. Created attachment 206182 [details]
cvc4 patch v5
Commited in r507774 https://svnweb.freebsd.org/ports?view=revision&revision=507774 Thanks! 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 (In reply to Jan Beich from comment #19) I'll fix them ASAP. Thanks! 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 Done. Thanks! |
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.