Skip site navigation (1)Skip section navigation (2)
Date:      Wed, 7 Aug 2019 19:56:13 +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:  <20190807195613.GK94703@spindle.one-eyed-alien.net>
In-Reply-To: <4FF9540B-E1FE-4947-8E45-8D4FB57A7E34@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> <20190807171714.GI94703@spindle.one-eyed-alien.net> <20190807180244.GJ94703@spindle.one-eyed-alien.net> <4FF9540B-E1FE-4947-8E45-8D4FB57A7E34@yahoo.com>

next in thread | previous in thread | raw e-mail | index | archive | help

--NyChO5MpGs3JHJbz
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
Content-Transfer-Encoding: quoted-printable

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> 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> wrot=
e:
> >>>>>>=20
> >>>>>>> I'd prefer to disable this dependency.  There's a knob that worke=
d 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, t=
he easy
> >>>>>>> workaround is probably to disable options LIT.  We could make tha=
t 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 o=
ff
> >>>>> 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, reb=
uild "
> >>>>                          "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_I=
NSTALL_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/modul=
es/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_n=
ame 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 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
> >>>=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 have
> >> z3 installed on the system and no LIB_DEPENDS line:
> >>=20
> >> Error: /usr/local/bin/FileCheck90 is linked to /usr/local/lib/libz3.so=
=2E0
> >> 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 lit
> >> (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 help
> > 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 editor.
> # If you do want to change a value, simply edit, save, and exit the edito=
r.
> # 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.

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.)

- Brooks

--NyChO5MpGs3JHJbz
Content-Type: application/pgp-signature; name="signature.asc"

-----BEGIN PGP SIGNATURE-----

iQEcBAEBAgAGBQJdSyzcAAoJEKzQXbSebgfAixMH+gJekos1JAIl6IAnt09byRKi
uelzg9rWWUaWTdAfOWqMSBvXuaGRoFNJL89o2Fr1CWEozwQ/6wDihmaBzUs6nn+8
Sofyz03RmwwcDnQn23X5OYEYOVVi7BqQ/eJ1WChyk3QfjvBdrKPoJrIEVVp+F5A4
49F16moJTEDg4TZMSk7zBIhpbXL5F6tyWsbNQVq4YbTv9/G5sL/6oGxCQdupWc6q
Hm6+7/DNu1NNJKM0PIY+7sf4JkfsrAGsqC4xR+HP8PsS3F5Wb4ugYt68DXz3CCiq
YlL4cTdug5gKD7fw2qoycPl/v+h2fX3HRhojCvAOlzKm2d/dsjt0GYC+AFTIka0=
=8gcE
-----END PGP SIGNATURE-----

--NyChO5MpGs3JHJbz--



Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?20190807195613.GK94703>