Re-work the nix infrastructure

[goodlyrottenapple]

Motivation

Nix in it's current stable version on most systems 2.3.* does not handle git submodules well, i.e. as far as i can tell, there is no way in nix 2.3 to recursively clone all submodules before building a derivation of the current repo. The current nix expression for building the k framework relies on the ttuegel/nix-lib library, to ensure nix correctly builds the derivations for haskell-backend and llvm-backend which are included as submodules. This works ok, but causes problems when trying to build the backends inside the evm-semantics repo, where k is included as a submodule.

Currently this is blocking runtimeverification/evm-semantics#1248 and https://github.com/runtimeverification/ksummarize/issues/33 by proxy

Proposed solution

A possible fix might be to try to modify the ttuegel/nix-lib utilities to handle several nested layers of submdules (namely evm-semantics -> k -> haskell-backend), but the code for these functions looks quite complex and potentially fragile.

There are several potential solutions to this problem I will outline in this proposal, but all essentially hinge on ignoring the included sub-modules and instead building the nix expressions for k by pulling in the llvm/haskell-backend nix expressions directly from their github repos.

This can be accomplished (I think) in two ways. Either we stick to the current setup and use niv to maintain a link to haskell-backend and llvm-backend in sources.json and build the k derivation against these.

Alternatively, we could switch to a new nix feature called flakes, which is basically designed to replace niv and add several conveniences to building nix expressions with carefully pinned dependencies (see e.g. https://www.tweag.io/blog/2020-05-25-flakes/ for an overview)

Both approaches come with advantages and disadvantages, outlined below

just using niv

+ probably requires fewer changes
+ if engineered well should allow us to easily switch out different versions of z3 or the back-ends for things like the evm-semantics test profiling
- requires keeping submodule versions of backends to be in sync with the niv sources.json versions

nix >=2.4 + nix flakes

+ flakes subsume the functionality of niv and are built into nix
+ looks like it's easier to manage/minimize dependencies of nested packages, for example, we could have

haskell-backend/flake.nix:

{
  inputs.z3.url = github:Z3Prover/z3/z3-4.8.15;
  inputs.nixpkgs.url = github:nixpkgs/nixos-21.11;
...
}

k/flake.nix:

{
  inputs.haskell-backend.url = github:runtimeverification/haskell-backend/<commit_hash>;
  inputs.z3.follows = "haskell-backend/z3";
  inputs.nixpkgs.follows = "haskell-backend/nixpkgs";
...
}

Which should keep everything in step and hopefully minimize having e.g. several different versions of nix-pkgs when building the expression. Potentially, when working on a local version, it should be possible to e.g.

• change the version of z3

  nix flake lock --override-input haskell-backend/z3 github:Z3Prover/z3/z3-4.8.17
  

• change haskell-backend to a different commit

  nix flake lock --override-input haskell-backend github:runtimeverification/haskell-backend/<different_commit_hash>
  

• change to a checked out local version of haskell-backend

  nix flake lock --override-input haskell-backend ~/git/haskell-backend
  

+ flakes makes things more tidy
+ we have already started to flake-ify llvm-backend runtimeverification/llvm-backend#460
- flakes are still experimental
- requires nix >=2.4 with experimental flakes feature turned on, tho there is https://github.com/edolstra/flake-compat
- requires keeping submodule versions of back-ends to be in sync with the flake.nix/flake.lock versions

Keeping submodules and nix expressions in sync

The best way would probably to both add a script for updating both versions at the same time, plus a CI check which ensures that the hashes for the nix sources and submodules match

Questions

• I'm not sure what happens with nix-flakes and locking of flake B when I update an input foo in flake A where flake B has inputs.foo.follows = "A/foo"
• How do we deal with the integration testing shell in the haskell-backend repo? This seems awkward atm anyway, given we do not run against the nix version of master but the current release which lags behind several days?/weeks?

[Baltoli]

On the points you make regarding keeping the versions in sync, I think the devops job that bumps the submodules can just be modified to keep the niv / flake version in sync.

[goodlyrottenapple]

Ah perfect. Tho I would also include the CI check to make sure they stay the same across commits to master, because if you were to use the nix flake lock or the analogous niv update you could accidentaly unlik them until the next submodule update by the CI.

[goodlyrottenapple]

Perhaps we should close this issue now? Flakes have been deployed to k, llvm and haskell backends. There are of course lots of specific improvements, but those may be outside of the scope of this original issue.