[RFC 0092] Computed derivations

[Ericson2314]

This is the spiritual successor of #40.

Rendered merged

Tracking issue

[asymmetric]

Left a couple of comments to make this more accessible.

[asymmetric]

Could you add a section explaining this syntax? I assume it's familiar for PLT folks, but it's very cryptic to me :)

[picnoir]

Those are inference rules expressed in operational semantics.

You can read that as if e evaluates to e' and e' is a derivation, then builtins.assumeDerivation e evaluates to e'.

I agree with asymmetric, we're not a PLT-focused symposium, prose is fine here.

[ocharles]

I think a more accessible presentation would be better. This is pseudo-formal, because (AFAIK) the ⇓ and is derivation judgements aren't actually defined anywhere.

[andir]

Agreed. Unfortunately not everyone has that background.

[blaggacao]

A "translation" would suffice. Those compaxt bits of formalisms are great, once one has learned to parse them.

[Ericson2314]

Well.....I'll put it this way:

1. I think CA derivations' various notions of store coherence (by far the subtlest part), GUIX-style "grafting", mixing native- and cross-compiled packages, and probably other things I can't anticipate are going to repeatedly keep us thinking about these sorts of inductive relations. Some sort of sequent-ish syntax, or prolog's horn clause syntax, or many other such things are far and away the clearest and most concise way to convey this information once the reader is familiar --- it's supposed to be nice and "pictoral" not inscrutable ivory tower. I think it be best if we start moving in that direction.

2. Even if I right some prose now, It's going to a pain to update. VS with this sort of syntax it can be easier to just stare at and have all the important bits come out, so it's easier to revise.

So I am fine writing some sort of prose explanation, but I rather do it once the RFC is further along.

---

P.S. whether you love our hate this stuff, https://www.youtube.com/watch?v=dCuZkaaou0Q is a fun talk.

[L-as]

You could include a link to a short introduction to natural deduction.

[L-as]

Since this is gone we can remove this.

[sternenseemann]

This should probably be clarified. I took me three readings to figure out that /nix/store/…foo.drv!* is to build all outputs (which is the current default behavior unless --derivation is specified, I assume?) and /nix/store/…foo.drv would just build the derivation.

[Ericson2314]

Oh sheesh, yes I never said what the semantics were. Did that in addition to the examples @asymmetric asked for.

[Ericson2314]

Does it make sense now? (before I mark this resolved.)

[sternenseemann]

The example clarifies things yeah! I am unsure though if the mention of --derivation is detremental at this point since it is a nixUnstable only thing and I could not find any documentation of the flag that even remotely explained to me what it does.

I guess we have a bit of a problem that this RFC somewhat overlaps with problems related to the Installables abstraction and the unstable CLI?

[L-as]

I think the FCP has passed?

[edolstra]

Yes indeed, so I've merged the RFC. Thanks all!

[nixos-discourse]

This pull request has been mentioned on NixOS Discourse. There might be relevant details there:

https://discourse.nixos.org/t/nixpkgss-current-development-workflow-is-not-sustainable/18741/73

[nixos-discourse]

This pull request has been mentioned on NixOS Discourse. There might be relevant details there:

https://discourse.nixos.org/t/recent-nix-change-worthy-of-greater-attention/18972/1

[Ericson2314]

[L-as]

We should post the pseudoshepherd meeting notes somewhere

[das-g]

We should post the pseudoshepherd meeting notes somewhere

I know our RFC process has the concept of shepherd teams, but what's a "pseudoshepherd meeting"?

[L-as]

@das-g We talked about this RFC at NixCon.

[tomberek]

Notes from NixCon opportunistic meeting in the courtyard:

Summary

• derivations that produce derivations
• IFD is normally used for bulk import of language-specifics
• ninja/make export for fine-grained caching
• performance characteristics
• equivalent ergonomics possible to full recursive-nix

History

• 2019 initial implementation
• Niel Mitchell, Applicative build systems are Monadic under the hood link
• on the fly lazy handling of the build graph instead of static build plan
• changes to the heart of Nix
• need more code review
• keep the momentum instead of exacerbating merge conflicts
• get John off of "single point of failure"
• add builtPath case of derivedPath
• treat the output of a derivation as a derivation

Summary of internals

• nix evaluation creates a derivation and it builds into another derivation.
• Uses the top-level goal to guide forward progress.
• Self-modifying graph, substitute new graphs in to the old.
• nix expression, with import nixpkgs hello, inside derivation, evaluate, build
• useful to avoid IFD
• parallelize evaluation
• Crates, extract names to do auto-completion
• repl supports IFD while live
• "^" for user feedback, interally the daemon protocol uses "!"
• RFC92 does not impact repl
• dervations produced do not have Nix values associated with them, store-layer concept
• override of dependency. with aeson we know static dependencies, with dynamic derivations
• might be possible to override, but might fail at build time

next step brainstorm

• create use cases (required for stabilization, not for experimental)

• make lang2nix examples

• needs library to make it ergonomic, or an extra primitive

• primary advantage is it is a limited IFD

• ninja2nix

• GNUMake 2 nix

• nixpkgs is limited because it cannot import nix code from elsewhere

• does this solve incremental builds

  • build Linux, it calculates the build graph
  • the evaluation inside the derivation can be cached
  • purs-nix

• IFD can be made correct, very hard to make it fast

• 92 is easy to make performant

• distcc, ccache

• "optimize IFD to do eval in parallel"

• Hercules-CI agent does some eval

• caching Nix evaluation, builtins.cache

• nix build .#x can make the derivation for you...

• this might also implement cached Nix evaluation (see Nix PR for caching primop)

• well suited for big builds

• recursive Nix is easier to adapt, speak the daemon protocol inside the sandbox

• The test case is the existing yarn2nix, old version of snack,

• cross system is an idiom question, how to express this?

• what conventions, when to use, when not to

• clearly describe when

• makePackage function, eval-time attributes added

there are simple advantages, but unclear if we can get the benefits for large projects

makes the sizes of necessary locks much smaller, making previously unpalatable appoaches better

Steps

1. review and merge PR
2. Nixpkgs? or branch with Hydra to test this
3. staging hydra
4. Project/example to prove it helps and measure

dependencies

5. determine if we need dynamic number of outputs? or recursive nix?
6. review existing PR to debug cycles of multi-output derivation (not a blocker, but helpful)
7. determine what we can do without the recursive-nix constraint

recursive-nix followup

"can we limit recursive-nix to only build from dynamic-derivation and use only nix-instantiate?"

question: dynamic derivation

• only limit to nix-instantiate
• "userspace" nix-instantiate
• "kernel" add store paths

[roberth]

Computed derivations could provide a means to access old packages in case of a major change to the language.

I'm not suggesting we should change the language in backwards incompatible ways, but if we were to do it, this feature would let us preserve Nix's unique selling point of being able to use very old software alongside very up to date software.

It will not generalize to any expression though; mostly just to derivations, so things like NixOS modules would still have to be ported, but this is much less effort than porting the entire toolchain and dependencies that produced the legacy package. (And you should probably review an old module anyway, if you even dare to run it as part of your OS)

Interestingly, this could be one way in which we'd have a need for nested computed derivations: if the legacy package before the language change was itself a computed derivation, because it uses a derivation-supported build system. Though for now it's a bit hard to imagine such a fancy package to be old.

More likely we'll first see a derivation-supported build system to rely on a computed derivation (to build the build system), though that seems to be a different kind of nesting, as such a build system is parented by Nixpkgs and could be injected into the final dynamic derivation by means of a store path, rather than having to do a double outputOf. We might not even call that nesting.

[nixos-discourse]

This pull request has been mentioned on NixOS Discourse. There might be relevant details there:

https://discourse.nixos.org/t/nixcon-governance-workshop/32705/9

[nixos-discourse]

This pull request has been mentioned on NixOS Discourse. There might be relevant details there:

https://discourse.nixos.org/t/community-calendar/18589/102