Date: Wed, 7 Aug 2019 13:42:26 -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: <68CDAEA5-73D8-40FB-A22F-CC3B357FA992@yahoo.com> In-Reply-To: <20190807195613.GK94703@spindle.one-eyed-alien.net> 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> <20190807195613.GK94703@spindle.one-eyed-alien.net>
next in thread | previous in thread | raw e-mail | index | archive | help
On 2019-Aug-7, at 12:56, Brooks Davis <brooks at freebsd.org> wrote:
> 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> =
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).
>>>>>=20
>>>>> I saw a reference to:
>>>>>=20
>>>>> 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}
>>>>>=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.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 =
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
>> =46rom 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 =
editor.
>> # 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.)
Just for my curiosity: which way are you
initializing LLVM_ENABLE_Z3_SOLVER to OFF ?:
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)?
=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?68CDAEA5-73D8-40FB-A22F-CC3B357FA992>