Date: Tue, 6 Aug 2019 21:22:52 -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: <086C99B8-1289-4D81-AAF5-85FB0AE70B7C@yahoo.com> In-Reply-To: <602EEB6C-D0B0-4EFB-AB0E-BE98FF1C4D90@yahoo.com> 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> <602EEB6C-D0B0-4EFB-AB0E-BE98FF1C4D90@yahoo.com>
next in thread | previous in thread | raw e-mail | index | archive | help
[I found something known to be missing in the
in at least some versions of
llvm/cmake/modules/CrossCompile.cmake that messes
up the overall handling of LLVM_ENABLE_Z3_SOLVER .]
On 2019-Aug-6, at 20:23, Mark Millard <marklmi at yahoo.com> wrote:
> On 2019-Aug-6, at 19:08, Brooks Davis <brooks at freebsd.org> wrote:
>=20
>> 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.
>=20
>=20
> I hope this helps. (I'm not a cmake expert.)
>=20
> llvm-9.0.0rc1.src/lib/Support/Z3Solver.cpp does:
>=20
> #if LLVM_WITH_Z3
>=20
> #include <z3.h>
>=20
> namespace {
> . . .
> } // end anonymous namespace
>=20
> #endif
>=20
> 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
> }
>=20
> (There are other places LLVM_WITH_Z3 is used but the
> above is suggestive.)
>=20
> Working backwards finds that:
>=20
> /wrkdirs/usr/ports/devel/llvm90/work/llvm-9.0.0rc1.src/CMakeLists.txt
>=20
> shows LLVM_WITH_Z3 being conditionally set to 1 via . . .
>=20
> set(LLVM_Z3_INSTALL_DIR "" CACHE STRING "Install directory of the Z3 =
solver.")
>=20
> 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()
>=20
> set(LLVM_WITH_Z3 1)
> endif()
>=20
> if( LLVM_TARGETS_TO_BUILD STREQUAL "all" )
> set( LLVM_TARGETS_TO_BUILD ${LLVM_ALL_TARGETS} )
> endif()
>=20
>=20
> If I read that correctly, LLVM_ENABLE_Z3_SOLVER set directly
> appears to override the default (that tracks if z3 was found).
I saw a reference to:
diff --git a/llvm/cmake/modules/CrossCompile.cmake =
b/llvm/cmake/modules/CrossCompile.cmake
index bc3b210f018..0c30b88f80f 100644
--- a/llvm/cmake/modules/CrossCompile.cmake
+++ b/llvm/cmake/modules/CrossCompile.cmake
@@ -53,6 +53,7 @@ function(llvm_create_cross_target_internal target_name =
toolchain buildtype)
-DLLVM_DEFAULT_TARGET_TRIPLE=3D"${TARGET_TRIPLE}"
-DLLVM_TARGET_ARCH=3D"${LLVM_TARGET_ARCH}"
=
-DLLVM_TEMPORARILY_ALLOW_OLD_TOOLCHAIN=3D"${LLVM_TEMPORARILY_ALLOW_OLD_TOO=
LCHAIN}"
+ -DLLVM_ENABLE_Z3_SOLVER=3D"${LLVM_ENABLE_Z3_SOLVER}"
${build_type_flags} ${linker_flag} ${external_clang_dir}
WORKING_DIRECTORY ${LLVM_${target_name}_BUILD}
DEPENDS CREATE_LLVM_${target_name}
in https://reviews.llvm.org/D54978 on Feb 12 2019, 5:41 PM
and it had the comment:
QUOTE
Independent of the rest of the discussion, this patch should be part of =
the reland, to make sure that explicitly turning off Z3 works reliably. =
Thanks for coming up with that, and thanks everyone for the good =
discussion here :)
END QUOTE
This apparently fixes a sub-cmake not respecting the
LLVM_ENABLE_Z3_SOLVER setting in the parent cmake.
(The overall review earlier describes the sub-cmake
not doing the right thing.)
=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?086C99B8-1289-4D81-AAF5-85FB0AE70B7C>