One of my favorite tools that belongs to Linux world is make. I'm a huge fan of it and, being a Linux programmer, use it in my everyday projects. But no, not as a build system I mostly use it. make is much more than just a casual build system.

Then, what is make? Having thought on that question, I think, I eventually devised a sound definition of what it actually does--or, at least, what its main activity is. Capability to build programs is just its tag feature that, unfortunately, hides more profound design principles.

What follows the red mark is just an utter garbage. While it may contain somewhat interesting observation, which are partially true, it is just wrong. I'll show it later.

make is a filesystem transformation prover. Its purpose is to prove that file system can be transformed from its current state to the specified, according to the rules in the makefile. The result is a proof, given (a) initial filesystem state, (b) set of inference rules and (c) target files that should be brought to up-to date state. make should provide the sequence of rules, in which every rule a: b c d ... is only triggered for an up-to-date b, c etc and not up-to-date a. Such makefile rules can be described as Assuming up-to-date-ness of b, c and d, infer up-to-date-ness of a after applying the commands listed in rule. And the sequence of rules built should have every target file (specified in make's command line) "inferred" this way.

Sounds familiar, right? Isn't it the same as proving logical formulas? It totally is. Up-to-date files from a given filesystem state are premises. Rules in makefile are the logical arguments (pattern rules resemble them even better). And targets are the formulas we're to prove.

Impressed? Now create a Makefile
aa%: a%
touch \$@

and try to make aaaaa in the folder where file named "a" exists. You'll fail to achieve this, and that's due to a huge limitation of make, which brings me back from mathematical dreams to reality: make is a build system. Flexible, but a build system.

### But

However, make, upon successful construction one of the possible "proofs" for all targets, actually executes the commands along the sequence of rules. And these commands can be arbitrary, while soundness of the whole transformation requires each rule to update its target and nothing else. This shatters the clean concept described above a bit.

Much of functionality of make unmentioned here may be treated just as tricky preprocessing of a makefile to shorten the number of characters needed to describe a set of explicit rules.

At the same time, this doesn't always suffice all users. The thing is, the rule format in make is quite limited and they can reason only about "up-to-dateness" of files in a given state. While users need more complex inference rules, for example "Target is up-to-date if its argument didn't change since the previous make invocation". While such rules can be implemented in terms of existing capabilities of make (like this), it would still be nice if make provided them out of the box.

Let alone many other caveats in GNU Make. Make is surely not ideal.

### However

But this is a positive post rather than negative. The declarative nature of make and its availability (all modern major Linux distributions provide it) make it a an invaluable tool if you need such a "filesystem transformation prover" as a part of your project. And it's all "Linux way": make can act as a manager that runs many small scripts (invoked via commands within a makefile or written inline) with specific narrow purposes.

I used it with various aims: to process header files, to run regression tests and to update a repository mirror; and I always found it a very flexible and robust tool. So, do not hesitate to use it. Make is more than just a build system. Though, just a little more.