---
title: 2020-12-11 meeting notes
date: 2020-12-11
---

# Agenda

- https://github.com/NixOS/nix/pull/4330
- https://github.com/NixOS/nix/issues/4344
- https://github.com/NixOS/nix/pull/4348

# PR 4330

- `realisation` might not be the best term, but keep it for the moment
- Needs a rebase to fix a conflict (and the OSX test)
- Could merge the json thing

# Issue 4344

Goal: Prevent weird states where several outputs can come from a different build.

Problematic example:

- Alice pushes `foo_1!out` to the binary cache
- Bob pushes `foo_2!dev` (depending on `foo_2!out`)
- Alice tries to fetch `foo!dev` from the cache, and gets an incoherence.

graph LR
    foo_1!dev --> foo_1!out
    foo_2!dev -.-> foo_1!out

## Aside

To ensure that we don't have any incoherence, mapping must form a closure

## DB rules for runtime coherence

forall p0 p1.
  p1 in runtimeClosure(p0)

forall drv out0 p0 p1. 
  all
     ( drv!out0 -> p0
     , p1 != p0
     , p1 in runtimeClosure(p0)
     , inputDrvs(drv) = {} # resolved drv
     ) 
  => oneof
     ( exists p2. all(p2 in inputSrcs(drv), p1 in runtimeClosure(p2))
     , exists out1. drv!out1 = p1
     )