Date: Wed, 7 Aug 2019 17:17:14 +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: <20190807171714.GI94703@spindle.one-eyed-alien.net> In-Reply-To: <086C99B8-1289-4D81-AAF5-85FB0AE70B7C@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> <086C99B8-1289-4D81-AAF5-85FB0AE70B7C@yahoo.com>
next in thread | previous in thread | raw e-mail | index | archive | help
--hcut4fGOf7Kh6EdG Content-Type: text/plain; charset=us-ascii Content-Disposition: inline Content-Transfer-Encoding: quoted-printable 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> 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 t= he > >>>> 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, rebui= ld " > > "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 so= lver.") > >=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_INS= TALL_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/modules/C= rossCompile.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_ALL= OW_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 part of t= he reland, to make sure that explicitly turning off Z3 works reliably. Than= ks for coming up with that, and thanks everyone for the good discussion her= e :) > 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.) 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 have z3 installed on the system and no LIB_DEPENDS line: Error: /usr/local/bin/FileCheck90 is linked to /usr/local/lib/libz3.so.0 =66rom math/z3 but it is not declared as a dependency Warning: you need LIB_DEPENDS+=3Dlibz3.so:math/z3 I've generally observed that the portions of the system that cover lit (which includes FileCheck) aren't very well behaved. -- Brooks --hcut4fGOf7Kh6EdG Content-Type: application/pgp-signature; name="signature.asc" -----BEGIN PGP SIGNATURE----- iQEcBAEBAgAGBQJdSweaAAoJEKzQXbSebgfAA5UIAJJzsmi0ab8JWHEycVSu3yNw cdYOkas553C7tDkhdPCrOmAwvKJqMQRJzLuQ5tQ3TEIn7txDcveq9lrtqy8qRMK0 c3lTHCWdUQUsLzGHNg0XXiBrb82jQb6yl4jT/qsQGXxRJcKkLs1tGO6vK6YYTuRO g2voU1wu+d7Fe5GT4LrCQTvHl8yMR5rpZQ21puWU2Z4lUWGDc2LdQGgDhzf4E2VF 37NrSfsb3LbiiffARRIVjoY3inTd+kCNOP9MtgcWSjiSCVMYQieJgc3a5cqkljmV oZT2rtwNhFSAhtf1q0BBzFKm22TNNIGu35W0N6dxAJxbd3XuXXoo19Z/T6nmdcw= =E2Aq -----END PGP SIGNATURE----- --hcut4fGOf7Kh6EdG--
Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?20190807171714.GI94703>