Date: Tue, 6 Aug 2019 20:23:39 -0700 From: Mark Millard <marklmi@yahoo.com> To: Brooks Davis <brooks@freebsd.org> Cc: freebsd-toolchain@freebsd.org, freebsd-ports@freebsd.org, freebsd-ppc@freebsd.org Subject: Re: devel/llvm90 requires math/z3 first; building math/z3 requires a c++ toolchain be in place Message-ID: <602EEB6C-D0B0-4EFB-AB0E-BE98FF1C4D90@yahoo.com> In-Reply-To: <20190807020826.GH94703@spindle.one-eyed-alien.net> References: <8DB3EAA4-2B88-4180-8386-673524D27C64@yahoo.com> <20190806165525.GC94703@spindle.one-eyed-alien.net> <2A88AADC-8ED0-4FFD-85A8-34C0186D5D4F@yahoo.com> <20190807020826.GH94703@spindle.one-eyed-alien.net>
next in thread | previous in thread | raw e-mail | index | archive | help
On 2019-Aug-6, at 19:08, Brooks Davis <brooks at freebsd.org> wrote:
> On Tue, Aug 06, 2019 at 05:59:21PM -0700, Mark Millard wrote:
>>=20
>>=20
>> On 2019-Aug-6, at 09:55, Brooks Davis <brooks at freebsd.org> wrote:
>>=20
>>> I'd prefer to disable this dependency. There's a knob that worked =
in
>>> the 8.0 timeframe, but the lit build now autodetects z3 when it is
>>> present and I've failed to find a knob to disable it. For now, the =
easy
>>> workaround is probably to disable options LIT. We could make that =
the
>>> default on non-LLVM platforms is that makes sense.
>>>=20
>>> -- Brooks
>>=20
>> Okay.
>>=20
>> poudriere-devel automatically built math/z3 because
>> I'd indicated to build devel/llvm90 . math/z3 was not
>> previously built: I've never had other use of it. So
>> my context was not one of an implicit autodetect.
>=20
> The dependency is there because if z3 is installed then the package
> that is built depends on z3. Thus I had not choice but to add a z3
> dependency until I find a way to turn it off. You can either help =
find
> a way to disable z3 detection in the cmake infrastructure or turn off
> LIT. I don't have any use for reports on the effects of commenting =
out
> the DEPENDS line. I know what that does.
I hope this helps. (I'm not a cmake expert.)
llvm-9.0.0rc1.src/lib/Support/Z3Solver.cpp does:
#if LLVM_WITH_Z3
=20
#include <z3.h>
=20
namespace {
. . .
} // end anonymous namespace
=20
#endif
llvm::SMTSolverRef llvm::CreateZ3Solver() {
#if LLVM_WITH_Z3
return llvm::make_unique<Z3Solver>();
#else
llvm::report_fatal_error("LLVM was not compiled with Z3 support, =
rebuild "
"with -DLLVM_ENABLE_Z3_SOLVER=3DON",
false);
return nullptr;
#endif
}
(There are other places LLVM_WITH_Z3 is used but the
above is suggestive.)
Working backwards finds that:
/wrkdirs/usr/ports/devel/llvm90/work/llvm-9.0.0rc1.src/CMakeLists.txt
shows LLVM_WITH_Z3 being conditionally set to 1 via . . .
set(LLVM_Z3_INSTALL_DIR "" CACHE STRING "Install directory of the Z3 =
solver.")
find_package(Z3 4.7.1)
=20
if (LLVM_Z3_INSTALL_DIR)
if (NOT Z3_FOUND)
message(FATAL_ERROR "Z3 >=3D 4.7.1 has not been found in =
LLVM_Z3_INSTALL_DIR: ${LLVM_Z3_INSTALL_DIR}.")
endif()
endif()
=20
set(LLVM_ENABLE_Z3_SOLVER_DEFAULT "${Z3_FOUND}")
=20
option(LLVM_ENABLE_Z3_SOLVER
"Enable Support for the Z3 constraint solver in LLVM."
${LLVM_ENABLE_Z3_SOLVER_DEFAULT}
)
=20
if (LLVM_ENABLE_Z3_SOLVER)
if (NOT Z3_FOUND)
message(FATAL_ERROR "LLVM_ENABLE_Z3_SOLVER cannot be enabled when Z3 =
is not available.")
endif()
set(LLVM_WITH_Z3 1)
endif()
if( LLVM_TARGETS_TO_BUILD STREQUAL "all" )
set( LLVM_TARGETS_TO_BUILD ${LLVM_ALL_TARGETS} )
endif()
If I read that correctly, LLVM_ENABLE_Z3_SOLVER set directly
appears to override the default (that tracks if z3 was found).
=3D=3D=3D
Mark Millard
marklmi at yahoo.com
( dsl-only.net went
away in early 2018-Mar)
Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?602EEB6C-D0B0-4EFB-AB0E-BE98FF1C4D90>