[HN Gopher] Propositions as Filenames, Builds as Proofs: The Ess...
___________________________________________________________________
Propositions as Filenames, Builds as Proofs: The Essence of Make
(2015)
Author : 082349872349872
Score : 9 points
Date : 2023-01-16 19:44 UTC (3 hours ago)
(HTM) web link (bentnib.org)
(TXT) w3m dump (bentnib.org)
| 082349872349872 wrote:
| > _Proof of a compound proposition "x and y implies z" is a
| command to run that will generate the proof of the atomic
| proposition z from the proofs of the atomic propositions x and y.
| For pattern rules, this proof is parameterised by the
| instantiation of the universally quantified variable. For some
| reason, in make, the universally quantified variable is written
| as "%" in the proposition, and "$_ " in the proof.*
|
| I guess using this model we only care about existence of a proof
| (although which proof is relevant in the actual contents of the
| updated target?); come to think of it I don't know how _make_
| handles having multiple viable paths to freshen a target.
___________________________________________________________________
(page generated 2023-01-16 23:02 UTC)