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.
(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!