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

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

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