Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Questions about and suggestions for build system #27

Closed
daniel-j-h opened this issue Apr 7, 2015 · 5 comments
Closed

Questions about and suggestions for build system #27

daniel-j-h opened this issue Apr 7, 2015 · 5 comments

Comments

@daniel-j-h
Copy link
Contributor

The build system currently fails with python3 as the default python interpreter (which is the case e.g. for debian jessie, gentoo, arch, ..), since the mk/* scripts use deprecated python2 syntax.

I saw comments about the python2 requirement being added and then again removed from the readme; but as far as I see it, python2 is still required. Is this intended? What are the assumptions about the target platforms? python2 and optionally python3? If so, which versions do you want to support?

There is also at least one argument mismatch that I encountered: --help lists the "--makefiles" flag, but if you specify it, the script fails. Looking through the source reveals why: "--onlymakefiles" is the flag's name and not "--makefiles".

Now after trying "--onlymakefiles" the script still fails, this time because it's unable to find a c++ file, rendering this flag completely useless.

Is there a reason for not using e.g. python's argparse and calling it a day?

Please don't see this as criticism, I just want to understand the reasons behind the build system's design. I'm more than glad to help out with the Linux specific parts, if you need any help -- but for this I need a more precise specification of what you actually want :)

wintersteiger pushed a commit to wintersteiger/z3 that referenced this issue Apr 8, 2015
wintersteiger pushed a commit to wintersteiger/z3 that referenced this issue Apr 8, 2015
@wintersteiger
Copy link
Contributor

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.

@daniel-j-h
Copy link
Contributor Author

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'."

@wintersteiger
Copy link
Contributor

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.

@daniel-j-h
Copy link
Contributor Author

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

@wintersteiger
Copy link
Contributor

Closing as resolved, pull request will be handled later.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants