Remove make build

[thomasspriggs]

Removing the make build will reduce the amount of maintenance work required, as it means only one build will need to be maintained, rather than 2. This will have benefits not only in reduced maintenance, but remove problems relating to the two builds being desynchronised.

I am initially raising this as a draft PR, so I can check CI passes.

• Each commit message has a non-empty body, explaining why the change was made.
• Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[martin-cs]

Please don't do this. There are a number of down-stream projects that use make and integrate into the CPROVER make system.

[thomasspriggs]

Hi @martin-cs would place-holder make files which kick off the cmake build instead be sufficient for compatibility? Are any of the downstream projects which you are referencing opensource projects which you could point me at for reference?

[kroening]

👎

[tautschnig]

@martin-cs @kroening Thank you for your comments - I suspected there still were a number of users of the Makefile builds, but don't actually have such data myself.

[tautschnig]

Also, before removing the Makefile builds we'd need to make sure the CMake builds support at least the same configurations of solvers.

[peterschrammel]

@piotr-grabalski, might be worth posting a survey on the CPROVER mailing list asking who is still using make, how easy it would be for them to move to cmake, and what would block them from doing so...

[martin-cs]

@thomasspriggs Projects that I am aware of include my project (not yet open source, definitely make), BTC's integrated version of CBMC (not going to be open source, build system unknown), whatever Diffblue is maintaining (not open source, build unknown), Hi-Frog (don't know if open source, build system unknown) and 2LS (open source, build is make IIRC). There may also be Toyota and Intel internal versions of CBMC but I don't know about these.

I don't know if Make wrapping CMake would work TBH. That sounds like one possible route.

/if/ this is going to happen we should go through a deprecation process.

[martin-cs]

@peterschrammel @piotr-grabalski more generally a survey of who uses it, what kinds of patch sets they maintain, if any, whether they follow develop, etc. might be useful.

[hannes-steffenhagen-diffblue]

@martin-cs Right, this would definitely not be a small change (I think tagging this as "cleanup" might’ve been a bit too optimistic) and would certainly warrant a major version bump. The problem is that having two parallel build systems is a significant maintenance burden (in that we had very real, actual bugs from that situation), not just for us but also for any new contributors. There are some other things I’d like to do in the future that would be annoying to get right with the Makefile build – for example, right now there is a single global include directory shared by all modules, which means that it’s easy to include files from modules you’ve not declared a dependency on (and as a side effect it’s also possible to accidentally introduce cyclical dependencies). This is worked around by a system I believe @peterschrammel introduced with module_dependencies.txt. It’d be better if we had separate include directories for each module, then it actually just wouldn’t be possible to include files without declaring a dependency – but this is tricky to get right because in the Make build this’d mean passing separate compile and linker flags across all modules, and Make doesn’t really have a concept of "high level" targets like CMake does and thus also no way of handling transitive dependencies (i.e. "if I link to library A that depends on B, I should also add the include directories for A and B and also link against B") – this, again is not the reason, this is just one among a long list of reasons.

FWIW I wouldn’t agree with just removing it out of the blue, we definitely need people some notice and time to migrate, but that’s why we wanted to put it here where we figured it’d be the most visible place for people following cbmc development to see it. The idea here wasn’t just making a decision over other people’s heads, but rather put this here to make it clear that this is something we’d like to do and then have a place where we can collect feedback.

I think what this needs for now is a better explanation of the motivation for this change, a migration guide for downstream (in principle I’d not expect this to be an intractable problem, but we’d have to provide some sort of guidance for people who are not used to CMake) – but especially for the latter we’d actually have to know how people use the existing Makefile build right now. If it’s just a matter of building cbmc itself with various flags and what not it should be enough to explain how to do the same with cmake, so this shouldn’t be a problem. If it’s adding new modules / flags this again, shouldn’t be a big problem. If you have any specific cases where you think this would be infeasible/unreasonable please let me know. If you feel like it’s worth doing we can have a chat offline about what exactly your specific concerns are.

[martin-cs]

@hannes-steffenhagen-diffblue Thanks for your thoughts and taking the time to write this up. I agree that two build systems seems like additional work. Ironicly this was one of my objections to us adding CMake in the first place!

From what I see there are two social issues here : A. there is a split between those that prefer Make and those that prefer CMake, B. the developers and code-level users of CPROVER are a fractured group and it is hard to have these kinds of discussion. Unfortunately I am not sure I know how to resolve either.

[thomasspriggs]

Given the objections this PR has received, I am going to close it out rather than leave it getting stale indefinitely. It would probably be quicker to make the changes again rather than re-base it anyway. Therefore a new PR could be raised should there be a collective agreement to move in this direction in future.

The cprover mailing list was mentioned in one of the comments on this PR. Is that a reference to this google group? https://groups.google.com/g/cprover It appears to have been unused since August 2018.