search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.15k stars 1.47k forks source link

pkg-config with the Make-based build? #5699

Open woodruffw opened 2 years ago

woodruffw commented 2 years ago

Hi there!

I see that z3 has support for pkg-config via CMake:

https://github.com/Z3Prover/z3/blob/658a334ecf5a06553ad16d2104440e892b31c31c/z3.pc.cmake.in

I noticed that there's a reference to pkg-config in the Make-based build system:

https://github.com/Z3Prover/z3/blob/658a334ecf5a06553ad16d2104440e892b31c31c/scripts/mk_util.py#L45

...but it doesn't seem to go anywhere, and the generated Makefile (in build) doesn't have any references to pkg-config or z3.pc that I can find.

Is there any way to get the Make-based build to generate a pkg-config file?

NikolajBjorner commented 2 years ago

I have as good idea as anybody else about this line. The cmake system is the preferred so unless there is some really good reason for using the python build (such as lacking ocaml support from cmake build so far) it is not something that is great spending bandwidth on. In other news, but highly related, there is now an internship opening https://careers.microsoft.com/us/en/job/1201362/Research-Intern-RiSE-Programming-Languages-Formal-Methods-High-Performance-Computing-Software-Engineering to address usability issues with z3. A big part of the usability issue, besides online usability, are the CI/CD and build issues of which there are many and needs dedication.

woodruffw commented 2 years ago

Thanks for the response! The main reason I ask about the Make-based build is because it's what Homebrew currently uses, which in turn is how a coworker of mine notice that the pkg-config file was missing 🙂

It sounds like the right answer is simply switching the Homebrew build to CMake, which is perfectly reasonable IMO.

NikolajBjorner commented 2 years ago

I can't say what homebrew should be doing, but it is obviously quite prolific. If homebrew can't use cmake or there is some obstacle the alternative would be to ensure the python build supports what you need. Unfortunately, the support calls on these build scenarios are perpetual. There is a possibly related bug open on fedora vs. ubuntu use of absolute/relative paths for the setup from the cmake build system.