... | ... | @@ -54,9 +54,11 @@ Also note, this implies that all indicating inputs of all rules must match some |
|
|
|
|
|
# Reducing the Indicating Inputs set
|
|
|
|
|
|
## Picking a smaller set
|
|
|
As `need`ing files generally means more code. As you must `need` all indicating inputs, you often want to pick a convenient (i.e. minimal) indicating inputs set. Remember this set is not unique so you're free to pick whatever indicating input set you want, but the responsibility is on you to ensure is in fact a valid indicating set.
|
|
|
|
|
|
Assuming you have an indicating set `I` for vital output `O` i.e. `change(O) -> change(I)`. We are wondering if some other set `I'` is also an indicating set for `O` (`I'` would often but not necessarily be a subset of `I`). One way you can be sure this is safe is to show that `I'` is an "indicating set" for `I` i.e.:
|
|
|
## Transitivity
|
|
|
|
|
|
Assuming you have an indicating set `I` for vital output `O` i.e. `change(O) -> change(I)`. We are wondering if some other (possibly overlapping) set `I'` is also an indicating set for `O`. One way you can be sure this is safe is to show that `I'` is an "indicating set" for `I` i.e.:
|
|
|
|
|
|
```
|
|
|
change(I) -> change(I')
|
... | ... | @@ -64,7 +66,47 @@ change(I) -> change(I') |
|
|
|
|
|
By transitivity of `->` we then have `change(O) -> change(I')`. In other words the "has indicating set" relationship is transitive.
|
|
|
|
|
|
In practice you may be asking a
|
|
|
## Eliminating non-indicating files
|
|
|
|
|
|
While writing a rule, you may suspect that a certain `need`ed file is not necessary. How can you be sure it is safe to remove? It is safe to remove if the remaining needs still form an indicating input set. Say the rule currently `need`s set `I` (`I` is your indicating inputs set) and the file you want to no longer `need` is `f ∈ I` forming a new set `I' = I \ {f}`. The question you must ask is "is `I'` a valid indicating inputs set?" i.e. it is safe to no longer `need` f if and only if:
|
|
|
|
|
|
```
|
|
|
change(O) -> change(I \ {f})
|
|
|
```
|
|
|
|
|
|
This may be hard to answer, but there is a convenient trick you can do here. If you know that `I'` is an indicating inputs set for for `{f}` then you know `I'` is an indicating inputs set for `O` and it is safe to remove the `need` for `f`. Formally:
|
|
|
|
|
|
```
|
|
|
f ∈ I AND
|
|
|
I' = I \ {f} AND
|
|
|
change(f) -> change(I') AND
|
|
|
change(O) -> change(I)
|
|
|
-> ( change(O) -> change(I') )
|
|
|
```
|
|
|
|
|
|
In fact this generalizes to removing a whole set of files `F` from `I`:
|
|
|
|
|
|
```
|
|
|
F ⊂ I AND
|
|
|
I' = I \ F AND
|
|
|
change(F) -> change(I') AND
|
|
|
change(O) -> change(I)
|
|
|
-> ( change(O) -> change(I') )
|
|
|
```
|
|
|
This reasoning is applied in the case of Haskell [.hi dependencies](Haskell-object-files-and-.hi-inputs): we know that a change in transitive `.hi` files (`R`) will result in a change in the immediate `.hi` file `f`: `change(R) -> change({f})` and by `{f} ⊂ I' = I \ R` we get `change(R) -> change(I')` and by the above we see that it is safe to remove the `need`s of the transitive `.hi` files.
|
|
|
|
|
|
### Even more general
|
|
|
|
|
|
We can remove the requirement that `F ⊂ I` and make a more general statement:
|
|
|
|
|
|
```
|
|
|
change(I \ I') -> change(I') AND
|
|
|
change(O) -> change(I)
|
|
|
-> ( change(O) -> change(I') )
|
|
|
```
|
|
|
|
|
|
But I'm not quite sure if this is useful in practice.
|
|
|
|
|
|
|
|
|
# Examples in Hadrian
|
|
|
|
... | ... | |