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)? === 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"
Re: devel/llvm90 requires math/z3 first; building math/z3 requires a c++ toolchain be in place
Mark Millard via freebsd-ports Wed, 07 Aug 2019 13:43:00 -0700
- Re: devel/llvm90 requires math/z3 first; bu... Mark Millard via freebsd-ports
- Re: devel/llvm90 requires math/z3 firs... Mark Millard via freebsd-ports
- Re: devel/llvm90 requires math/z3 ... Mark Millard via freebsd-ports
- Re: devel/llvm90 requires math/z3 firs... Brooks Davis
- Re: devel/llvm90 requires math/z3 ... Mark Millard via freebsd-ports
- Re: devel/llvm90 requires math... Mark Millard via freebsd-ports
- Re: devel/llvm90 requires ... Brooks Davis
- Re: devel/llvm90 requ... Brooks Davis
- Re: devel/llvm90 requ... Mark Millard via freebsd-ports
- Re: devel/llvm90 requ... Brooks Davis
- Re: devel/llvm90 requ... Mark Millard via freebsd-ports
- Re: devel/llvm90 requ... Brooks Davis
- Re: devel/llvm90 requ... Mark Millard via freebsd-ports
- Re: devel/llvm90 requ... Mark Millard via freebsd-ports