Skip site navigation (1)Skip section navigation (2)
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>