Re: devel/llvm90 requires math/z3 first; building math/z3 requires a c++ toolchain be in place

Wed, 07 Aug 2019 14:37:23 -0700 


On 2019-Aug-7, at 13:58, Brooks Davis <brooks at freebsd.org> wrote:

> On Wed, Aug 07, 2019 at 01:42:26PM -0700, Mark Millard wrote:
>> 
>> 
>> 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:
>>>> 
>>>> 
>>>> On 2019-Aug-7, at 11:02, Brooks Davis <brooks at freebsd.org> wrote:
>>>> 
>>>>> 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 .]
>>>>>>> 
>>>>>>> On 2019-Aug-6, at 20:23, Mark Millard <marklmi at yahoo.com> wrote:
>>>>>>> 
>>>>>>> 
>>>>>>> 
>>>>>>>> On 2019-Aug-6, at 19:08, Brooks Davis <brooks at freebsd.org> wrote:
>>>>>>>> 
>>>>>>>>> On Tue, Aug 06, 2019 at 05:59:21PM -0700, Mark Millard wrote:
>>>>>>>>>> 
>>>>>>>>>> 
>>>>>>>>>> On 2019-Aug-6, at 09:55, Brooks Davis <brooks at freebsd.org> wrote:
>>>>>>>>>> 
>>>>>>>>>>> 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.
>>>>>>>>>>> 
>>>>>>>>>>> -- Brooks
>>>>>>>>>> 
>>>>>>>>>> Okay.
>>>>>>>>>> 
>>>>>>>>>> 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.
>>>>>>>>> 
>>>>>>>>> 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.
>>>>>>>> 
>>>>>>>> 
>>>>>>>> I hope this helps. (I'm not a cmake expert.)
>>>>>>>> 
>>>>>>>> llvm-9.0.0rc1.src/lib/Support/Z3Solver.cpp does:
>>>>>>>> 
>>>>>>>> #if LLVM_WITH_Z3
>>>>>>>> 
>>>>>>>> #include <z3.h>
>>>>>>>> 
>>>>>>>> namespace {
>>>>>>>> . . .
>>>>>>>> } // end anonymous namespace
>>>>>>>> 
>>>>>>>> #endif
>>>>>>>> 
>>>>>>>> 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=ON",
>>>>>>>>                        false);
>>>>>>>> return nullptr;
>>>>>>>> #endif
>>>>>>>> }
>>>>>>>> 
>>>>>>>> (There are other places LLVM_WITH_Z3 is used but the
>>>>>>>> above is suggestive.)
>>>>>>>> 
>>>>>>>> Working backwards finds that:
>>>>>>>> 
>>>>>>>> /wrkdirs/usr/ports/devel/llvm90/work/llvm-9.0.0rc1.src/CMakeLists.txt
>>>>>>>> 
>>>>>>>> shows LLVM_WITH_Z3 being conditionally set to 1 via . . .
>>>>>>>> 
>>>>>>>> set(LLVM_Z3_INSTALL_DIR "" CACHE STRING "Install directory of the Z3 
>>>>>>>> solver.")
>>>>>>>> 
>>>>>>>> find_package(Z3 4.7.1)
>>>>>>>> 
>>>>>>>> if (LLVM_Z3_INSTALL_DIR)
>>>>>>>> if (NOT Z3_FOUND)
>>>>>>>> message(FATAL_ERROR "Z3 >= 4.7.1 has not been found in 
>>>>>>>> LLVM_Z3_INSTALL_DIR: ${LLVM_Z3_INSTALL_DIR}.")
>>>>>>>> endif()
>>>>>>>> endif()
>>>>>>>> 
>>>>>>>> set(LLVM_ENABLE_Z3_SOLVER_DEFAULT "${Z3_FOUND}")
>>>>>>>> 
>>>>>>>> option(LLVM_ENABLE_Z3_SOLVER
>>>>>>>> "Enable Support for the Z3 constraint solver in LLVM."
>>>>>>>> ${LLVM_ENABLE_Z3_SOLVER_DEFAULT}
>>>>>>>> )
>>>>>>>> 
>>>>>>>> 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()
>>>>>>>> 
>>>>>>>> set(LLVM_WITH_Z3 1)
>>>>>>>> endif()
>>>>>>>> 
>>>>>>>> if( LLVM_TARGETS_TO_BUILD STREQUAL "all" )
>>>>>>>> set( LLVM_TARGETS_TO_BUILD ${LLVM_ALL_TARGETS} )
>>>>>>>> endif()
>>>>>>>> 
>>>>>>>> 
>>>>>>>> If I read that correctly, LLVM_ENABLE_Z3_SOLVER set directly
>>>>>>>> appears to override the default (that tracks if z3 was found).
>>>>>>> 
>>>>>>> I saw a reference to:
>>>>>>> 
>>>>>>> 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="${TARGET_TRIPLE}"
>>>>>>>       -DLLVM_TARGET_ARCH="${LLVM_TARGET_ARCH}"
>>>>>>>       
>>>>>>> -DLLVM_TEMPORARILY_ALLOW_OLD_TOOLCHAIN="${LLVM_TEMPORARILY_ALLOW_OLD_TOOLCHAIN}"
>>>>>>> +        -DLLVM_ENABLE_Z3_SOLVER="${LLVM_ENABLE_Z3_SOLVER}"
>>>>>>>       ${build_type_flags} ${linker_flag} ${external_clang_dir}
>>>>>>>   WORKING_DIRECTORY ${LLVM_${target_name}_BUILD}
>>>>>>>   DEPENDS CREATE_LLVM_${target_name}
>>>>>>> 
>>>>>>> in https://reviews.llvm.org/D54978 on Feb 12 2019, 5:41 PM
>>>>>>> and it had the comment:
>>>>>>> 
>>>>>>> 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
>>>>>>> 
>>>>>>> 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
>>>>>> from math/z3 but it is not declared as a dependency
>>>>>> Warning: you need LIB_DEPENDS+=libz3.so:math/z3
>>>>>> 
>>>>>> I've generally observed that the portions of the system that cover lit
>>>>>> (which includes FileCheck) aren't very well behaved.
>>>>> 
>>>>> I've filed https://bugs.llvm.org/show_bug.cgi?id=42921 upstream,
>>>>> hopefully someone who understand this part of the cmake system will help
>>>>> us out.
>>>> 
>>>> You mentioned applying the patch but not also
>>>> setting:
>>>> 
>>>> LLVM_ENABLE_Z3_SOLVER:BOOL=OFF
>>>> 
>>>> with either:
>>>> 
>>>> -D LLVM_ENABLE_Z3_SOLVER:BOOL=OFF
>>>> 
>>>> 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 .)
>>>> 
>>>> 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.
>>>> 
>>>> Taking from an example from web of a CMakeCache.txt . . .
>>>> 
>>>> 
>>>> # 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=VALUE
>>>> # 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.
>>>> 
>>>> ########################
>>>> # EXTERNAL cache entries
>>>> ########################
>>>> 
>>>> //Build a 32 bit version of the library.
>>>> BENCHMARK_BUILD_32_BITS:BOOL=OFF
>>>> 
>>>> . . . (lots omitted) . . .
>>>> 
>>>> 
>>>> //Fail and stop if a warning is triggered.
>>>> LLVM_ENABLE_WERROR:BOOL=OFF
>>>> 
>>>> //Enable Support for the Z3 constraint solver in LLVM.
>>>> LLVM_ENABLE_Z3_SOLVER:BOOL=OFF
>>>> 
>>>> //Use zlib for compression/decompression if available.
>>>> LLVM_ENABLE_ZLIB:BOOL=ON
>>>> 
>>>> . . . (lots more omitted) . . .
>>>> 
>>>> 
>>>> The example already had the "LLVM_ENABLE_Z3_SOLVER:BOOL=OFF"
>>>> 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.)
>> 
>> Just for my curiosity: which way are you
>> initializing LLVM_ENABLE_Z3_SOLVER to OFF ?:
>> 
>> A) Having -D LLVM_ENABLE_Z3_SOLVER:BOOL=OFF on the cmake command line?
>> B) Having LLVM_ENABLE_Z3_SOLVER:BOOL=OFF in the CMakeCache.txt file?
>> C) Something else (that I missed as a technique)?
> 
> (A) via:
> 
> CMAKE_ARGS+=    -DLLVM_ENABLE_Z3_SOLVER=OFF

Thanks.

>From what I've seen the :BOOL part of the syntax should be used:

CMAKE_ARGS+=    -DLLVM_ENABLE_Z3_SOLVER:BOOL=OFF

It is not a textual definition from what I gather and
the intended type should be specified as well. (But
I'm learning things as I go.)

===
Mark Millard
marklmi at yahoo.com
( dsl-only.net <http://dsl-only.net/> went
away in early 2018-Mar)

_______________________________________________
freebsd-toolchain@freebsd.org mailing list
https://lists.freebsd.org/mailman/listinfo/freebsd-toolchain
To unsubscribe, send any mail to "freebsd-toolchain-unsubscr...@freebsd.org"

























					Reply via email to