Questions about and suggestions for build system about z3 HOT 5 CLOSED

We have always supported Python 3, but we test it very rarely. We already have far too many combinations of systems and configurations to test every night and for some reason we all ended up using Python 2. I just committed a couple fixes that should make it work with 3 again.

I fixed the --onlymakefiles problem (it's now --makefiles as advertised). I didn't see any errors when running it. Could it be that you or me had some stale files around?

No reason for not using argparse as far as I know.

We haven't discussed anything that we would want and don't have in the build system. One of the important reasons behind many design decisions was that the primary target up until now was Windows, 32 bit. Python scripts seemed like the best solution to get some sort of unified cross-platform system. Previously, configure scripts and Makefiles would never be in sync with the Visual Studio solution files, so now we generate both from the same Python scripts.

from z3.

Thanks for the explanations. Regarding your idea about stale files, I re-checked the issue:
With a freshly cleaned repository, unstable branch as of b7bb534:

./configure --githash=$(git rev-parse HEAD) --makefiles --staticlib

Writing build/Makefile
Traceback (most recent call last):
  File "scripts/mk_make.py", line 20, in <module>
    mk_makefile()
  File "/tmp/z3-buildsystem/scripts/mk_util.py", line 1974, in mk_makefile
    c.mk_makefile(out)
  File "/tmp/z3-buildsystem/scripts/mk_util.py", line 916, in mk_makefile
    Component.mk_makefile(self, out)
  File "/tmp/z3-buildsystem/scripts/mk_util.py", line 868, in mk_makefile
    self.add_cpp_rules(out, include_defs, cppfile)
  File "/tmp/z3-buildsystem/scripts/mk_util.py", line 826, in add_cpp_rules
    self.add_rule_for_each_include(out, cppfile)
  File "/tmp/z3-buildsystem/scripts/mk_util.py", line 805, in add_rule_for_each_include
    owner = self.find_file(include, fullname)
  File "/tmp/z3-buildsystem/scripts/mk_util.py", line 789, in find_file
    raise MKException("Failed to find include file '%s' for '%s' when processing '%s'." % (fname, ownerfile, self.name))
mk_exception.MKException: "Failed to find include file 'algebraic_params.hpp' for 'src/math/polynomial/algebraic_numbers.cpp' when processing 'polynomial'."

from z3.

That's right, algebraic_params.hpp is one of many automatically generated files. mk_make.py with the --makefiles option will generate only the Makefile, it will not produce any other files. They are necessary to build Z3 though, so they have to be generated by some other means, for instance by running without --makefiles once. I didn't write the code for that, but it seems to me that this is the intended behavior for --makefiles.

from z3.

You are right; I was under the impression "--makefiles" would still generate dependencies the build relies on.

from z3.

Closing as resolved, pull request will be handled later.

from z3.