[I found that the vintage of cmake matters: 3.12 and
earlier work differently. Details later.]

On 2019-Aug-7, at 14:37, Mark Millard <marklm at yahoo.com> wrote:

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

I ran into the following issue for CMake 3.12 and earlier
(before 01 Dec 2018 07:37:57 according to freshports) . . .

QUOTE
option() honors normal variables.

The option() command is typically used to create a cache entry to allow users 
to set the option. However, there are cases in which a normal (non-cached) 
variable of the same name as the option may be defined by the project prior to 
calling the option() command. For example, a project that embeds another 
project as a subdirectory may want to hard-code options of the subproject to 
build the way it needs.

For historical reasons in CMake 3.12 and below the option() command removes a 
normal (non-cached) variable of the same name when:

        • a cache entry of the specified name does not exist at all, or
        • a cache entry of the specified name exists but has not been given a 
type (e.g. via -D<name>=ON on the command line).
END QUOTE

So the setting of LLVM_ENABLE_Z3_SOLVER:BOOL=OFF will not work
for CMake 3.12 and before.

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

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

Reply via email to