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

Wed Aug 7 18:55:11 UTC 2019

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)