Bob Atkey's musings

[Gabor Greif]

Bob wrote a blog post about the limits and perspectives of make. http://bentnib.org/posts/2015-04-17-propositions-as-filenames-essence-of-make.html

Some of these might apply to shake too, I particularly liked the bottom-up build idea. I always wished for a continuously running builder that eagerly rebuilds stuff in an infinite loop.

Cheers,

Gabor

[Neil Mitchell]

Intresting!

"I think that the Ninja system essentially gets its speed ups by
caching the some of results of the proof search step..." - I'm fairly
certain this isn't true, having implemented a faster Ninja than Ninja
based on Shake without doing that. That said, the Ninja people claim
this is why their system is faster, so can't really fault Bob here.

"dynamically depend on dependencies listed in generated files, via
“scanner” dependencies. I think this corresponds to proof search in a
dependently-typedlogic" - I suspect that's what Shake corresponds to
as well, although perhaps Shake is a better example than OMake as its
less restricted.

"Build rules that generate multiple files are Horn clauses with
conclusions that are conjunctions (ands) of atomic propositions. GNU
make and others make multiple targets difficult, but from a logical
point-of-view, there is no problem." Very interesting. So Shake
doesn't really have support for multiple files, it just has
polymorphic rules, and once you have that, multiple files just falls
out - much like Shake can actually capture the logic properly.

"make implements a “top-down” approach to evaluating its logic
program. Why not also implement a “bottom-up” evaluation too?" - that
is far harder if you had dependency types, and if to execute your
typing judgement you execute arbitrary side-effecting IO.

"Can logics that incorporate forms of (sound) circular reasoning be
used to do build jobs that require iteration until a fixpoint" - that
doesn't require anything in the logic, see
http://stackoverflow.com/q/14622169/160673. You need constructs for
iteration, but as long as you have universal quantification, you can
just keep reusing fresh variables.

"Do all atomic propositions have to be filenames?" - no, you want them
to be polymorphic, exactly like Shake.

"Can we use a make-like tool to query a database, and generate
reports" - this is just a subset of "can you make the rules
polymorphic"

"Can we automatically augment the proof graphs that make implicitly
generates to add provenance information?" - not totally sure what this
means. The provenance of a proof seems obvious in Make (its
dependencies) and in Shake you can get it out of the profiling. I
guess it makes sense if the proof is made of a number of atomic parts,
but those would be atomic files, and thus you can get provenance
anyway.

The bottom up idea is certainly appealing - and works fine for rebuild
the world scenarios. It's much trickier to pull off if you want to
only rebuild a subset of files. As an example of one approach that
does go bottom up, see Fabricate: https://code.google.com/p/fabricate/

For continuous rebuilding, you can certainly put Shake in a loop, and
I have a plan to make that a little bit easier -
https://github.com/ndmitchell/shake/issues/161 - but even now it's not
too difficult. However, my experience is that something like ghcid
(https://github.com/ndmitchell/ghcid) works better, relying on
interpretation instead of compilation, being driven off a subset of
files and doing intelligent things with error messages. Of course, its
not as general as Shake.

Thanks, Neil