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

[Mark Millard via freebsd-toolchain]

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.


===
Mark Millard
marklmi at yahoo.com
( 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"