cmake: Fix include search for Z3 in testgen library

[vlstill]

@fruffy The change in 38ba8df#diff-b2d8f4059a838269ba2d86ef0f39a84301da327327cd0415e56e7e6d68507e92R117 broke build of testgen on systems where Z3 does not have includes in the default system directory. The reason is that add_dependencies only affects ordering, not include-/link- search paths. Instead if I set the (static) testgen library to be linked to Z3 and inja with the PUBLIC option it will mean that both the library itself, and anything that it is linked to will see the include paths for both Z3 and inja and any resulting binaries will be linked to both. This not only fixes the problem, but it is also cleaner (except for the cmake weirdness that target_link_libraries affects both include- and link-search, but that it a feature of cmake itself).

[fruffy]

Hmm, let me think about this. Z3 is already a publicly linked library in p4tools-common, so I am not sure why this fails.
Inja definitely should be a publicly linked library, however.

We will definitely need the add_dependencies call to ensure build order remains consistent in parallel builds. The intent for libtestgen was to be a minimal, standalone library. ${TESTGEN_LIBS} can pull in a lot of unnecessary things, depending on the extensions that are present.

[vlstill]

Hmm, let me think about this. Z3 is already a publicly linked library in p4tools-common, so I am not sure why this fails. Inja definitely should be a publicly linked library, however.

It fails because there is nothing connecting p4tools-common to (lib)testgen. While it does not link to anything (it is a static library), it needs the include paths to be set correctly. You did that for inja manually, but not for Z3. My guess is that your system (and CI here) has Z3 in the standard location so it works anyway, but not for me.

We will definitely need the add_dependencies call to ensure build order remains consistent in parallel builds.

I think the target_link_libraries should also implicitly add the dependency.

The intent for libtestgen was to be a minimal, standalone library. ${TESTGEN_LIBS} can pull in a lot of unnecessary things, depending on the extensions that are present.

In that case I suggest explicitly linking libtestgen to inja and z3::z3 and than linking the whole testgen to all ${TESTGEN_LIBS}. I don't think duplicates will be problematic here.

[fruffy]

Thanks for fixing this. We also install a custom version of Z3, but we install it in /usr/local/lib, which does not seem to run into these issues.

Maybe it is worthwhile to use fetchcontent to install Z3 explicitly to avoid these errors going forward. Just like we do with Inja.

[vlstill]

Thanks for fixing this. We also install a custom version of Z3, but we install it in /usr/local/lib, which does not seem to run into these issues.

Yes, that would be found by default I think.

Maybe it is worthwhile to use fetchcontent to install Z3 explicitly to avoid these errors going forward. Just like we do with Inja.

Maybe as a fallback we could. I think we should allow using system libs too (also for inja), but that is another topic.