Date: Wed, 7 Aug 2019 20:58:46 +0000 From: Brooks Davis <brooks@freebsd.org> To: Mark Millard <marklmi@yahoo.com> 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: <20190807205846.GM94703@spindle.one-eyed-alien.net> In-Reply-To: <68CDAEA5-73D8-40FB-A22F-CC3B357FA992@yahoo.com> References: <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> <086C99B8-1289-4D81-AAF5-85FB0AE70B7C@yahoo.com> <20190807171714.GI94703@spindle.one-eyed-alien.net> <20190807180244.GJ94703@spindle.one-eyed-alien.net> <4FF9540B-E1FE-4947-8E45-8D4FB57A7E34@yahoo.com> <20190807195613.GK94703@spindle.one-eyed-alien.net> <68CDAEA5-73D8-40FB-A22F-CC3B357FA992@yahoo.com>
next in thread | previous in thread | raw e-mail | index | archive | help
--IJFRpmOek+ZRSQoz
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
Content-Transfer-Encoding: quoted-printable
On Wed, Aug 07, 2019 at 01:42:26PM -0700, Mark Millard wrote:
>=20
>=20
> On 2019-Aug-7, at 12:56, Brooks Davis <brooks at freebsd.org> wrote:
>=20
> > On Wed, Aug 07, 2019 at 11:55:04AM -0700, Mark Millard wrote:
> >>=20
> >>=20
> >> On 2019-Aug-7, at 11:02, Brooks Davis <brooks at freebsd.org> wrote:
> >>=20
> >>> On Wed, Aug 07, 2019 at 05:17:14PM +0000, Brooks Davis wrote:
> >>>> On Tue, Aug 06, 2019 at 09:22:52PM -0700, Mark Millard wrote:
> >>>>> [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 .]
> >>>>>=20
> >>>>> On 2019-Aug-6, at 20:23, Mark Millard <marklmi at yahoo.com> wrote:
> >>>>>=20
> >>>>>=20
> >>>>>=20
> >>>>>> On 2019-Aug-6, at 19:08, Brooks Davis <brooks at freebsd.org> wrot=
e:
> >>>>>>=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> wr=
ote:
> >>>>>>>>=20
> >>>>>>>>> I'd prefer to disable this dependency. There's a knob that wor=
ked 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 t=
hat 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 packa=
ge
> >>>>>>> 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 hel=
p 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 commenti=
ng 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, r=
ebuild "
> >>>>>> "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).
> >>>>>=20
> >>>>> I saw a reference to:
> >>>>>=20
> >>>>> diff --git a/llvm/cmake/modules/CrossCompile.cmake b/llvm/cmake/mod=
ules/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_TOOLCHAIN}"
> >>>>> + -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}
> >>>>>=20
> >>>>> in https://reviews.llvm.org/D54978 on Feb 12 2019, 5:41 PM
> >>>>> and it had the comment:
> >>>>>=20
> >>>>> QUOTE
> >>>>> Independent of the rest of the discussion, this patch should be par=
t of the reland, to make sure that explicitly turning off Z3 works reliably=
=2E Thanks for coming up with that, and thanks everyone for the good discus=
sion here :)
> >>>>> END QUOTE
> >>>>>=20
> >>>>> 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.)
> >>>>=20
> >>>> Thanks for digging this up. Unfortunately, this doesn't seem to have
> >>>> solved the problem. With this patch applied I still get this if I h=
ave
> >>>> z3 installed on the system and no LIB_DEPENDS line:
> >>>>=20
> >>>> Error: /usr/local/bin/FileCheck90 is linked to /usr/local/lib/libz3.=
so.0
> >>>> from math/z3 but it is not declared as a dependency
> >>>> Warning: you need LIB_DEPENDS+=3Dlibz3.so:math/z3
> >>>>=20
> >>>> I've generally observed that the portions of the system that cover l=
it
> >>>> (which includes FileCheck) aren't very well behaved.
> >>>=20
> >>> I've filed https://bugs.llvm.org/show_bug.cgi?id=3D42921 upstream,
> >>> hopefully someone who understand this part of the cmake system will h=
elp
> >>> us out.
> >>=20
> >> You mentioned applying the patch but not also
> >> setting:
> >>=20
> >> LLVM_ENABLE_Z3_SOLVER:BOOL=3DOFF
> >>=20
> >> with either:
> >>=20
> >> -D LLVM_ENABLE_Z3_SOLVER:BOOL=3DOFF
> >>=20
> >> on the command line or some line early in CMakeCache.txt .
> >> (Actually, I had to look around to know to say those
> >> specifics of what it means to have already initialized
> >> LLVM_ENABLE_Z3_SOLVER .)
> >>=20
> >> From what I see, taking the initial assignment via CMakeCache.txt
> >> after it is initialized seems to be a common technique of controlling
> >> the configuration.
> >>=20
> >> Taking from an example from web of a CMakeCache.txt . . .
> >>=20
> >>=20
> >> # This is the CMakeCache file.
> >> # For build in directory: [edited out]
> >> # It was generated by CMake: /Applications/CMake.app/Contents/bin/cmake
> >> # You can edit this file to change values found and used by cmake.
> >> # If you do not want to change any of the values, simply exit the edit=
or.
> >> # If you do want to change a value, simply edit, save, and exit the ed=
itor.
> >> # The syntax for the file is as follows:
> >> # KEY:TYPE=3DVALUE
> >> # KEY is the name of a variable in the cache.
> >> # TYPE is a hint to GUIs for the type of VALUE, DO NOT EDIT TYPE!.
> >> # VALUE is the current value for the KEY.
> >>=20
> >> ########################
> >> # EXTERNAL cache entries
> >> ########################
> >>=20
> >> //Build a 32 bit version of the library.
> >> BENCHMARK_BUILD_32_BITS:BOOL=3DOFF
> >>=20
> >> . . . (lots omitted) . . .
> >>=20
> >>=20
> >> //Fail and stop if a warning is triggered.
> >> LLVM_ENABLE_WERROR:BOOL=3DOFF
> >>=20
> >> //Enable Support for the Z3 constraint solver in LLVM.
> >> LLVM_ENABLE_Z3_SOLVER:BOOL=3DOFF
> >>=20
> >> //Use zlib for compression/decompression if available.
> >> LLVM_ENABLE_ZLIB:BOOL=3DON
> >>=20
> >> . . . (lots more omitted) . . .
> >>=20
> >>=20
> >> The example already had the "LLVM_ENABLE_Z3_SOLVER:BOOL=3DOFF"
> >> line, I did not adjust it.
> >=20
> > Upstream spotted this error as well. I've hopefully committed a fix (of
> > course just as I committed I discovered I'd had the patch applied and it
> > shouldn't be needed so I'm now rebuilding again and will add the patch
> > if needed.)
>=20
> Just for my curiosity: which way are you
> initializing LLVM_ENABLE_Z3_SOLVER to OFF ?:
>=20
> A) Having -D LLVM_ENABLE_Z3_SOLVER:BOOL=3DOFF on the cmake command line?
> B) Having LLVM_ENABLE_Z3_SOLVER:BOOL=3DOFF in the CMakeCache.txt file?
> C) Something else (that I missed as a technique)?
(A) via:
CMAKE_ARGS+=3D -DLLVM_ENABLE_Z3_SOLVER=3DOFF
-- Brooks
--IJFRpmOek+ZRSQoz
Content-Type: application/pgp-signature; name="signature.asc"
-----BEGIN PGP SIGNATURE-----
iQEcBAEBAgAGBQJdSzuFAAoJEKzQXbSebgfAk8kIAKSC8auB8taB5Fd81iZqj26U
mKfbd4/zNTvgo1v+c7c6EsiAm2JKbL0U0NcGyXH0+z1z25kdnPxEFTUdbs3G1YXd
IQNlwK3F7OhOoRMbkbeGbaNjuzZnYBDxZyFBGGGeYw/uMooCv/+tXNDr02dtmhPN
/SNnuCwWBkU8oghaffjmSg1VbqB2PZCdSu8YzvGPpU/V3iIpUThvb7HDYHbyx11K
lC7UzFez2JwTjZQffPv1rSo/SNVubY47HtLQDJWPiiGEiG1KwzSMMQ9kN5833vBp
wGyLrDUu/SL9vXWNSSZQ8P9+t4HIj9oo4WhSyX1aDyvJtCMQZG2UmjkVsvnghaE=
=VKgt
-----END PGP SIGNATURE-----
--IJFRpmOek+ZRSQoz--
Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?20190807205846.GM94703>