k2nix proposal

[goodlyrottenapple]

Having investigated #47, it turns out that the nix provided clang/c++ binaries are specially wrapped to ignore system wide paths as suspected. This wiki gives a bit more detail https://nixos.wiki/wiki/C, see also https://nixos.wiki/wiki/FAQ/I_installed_a_library_but_my_compiler_is_not_finding_it._Why%3F. THe way nix does this is to wrap the binaries in a script which reads any additional includes from NIX_CFLAGS_COMPILE/NIX_LDFLAGS. When a nix derivation is added to the buildInputs, nix automagically adds the relevant includes/ from those derivation to these vars inside it's build environment. The same thing happens when we call nix develop inside the project (e.g. evm-semantics), i.e. nix provides a shell with the same set of evn vars set correctly for clang to find the necessary libraries.

Given that C/C++ has no package manager, I think this is a sensible decision, but it does pose a question of how to provide an environment for developing with K, which implicitly relies on clang for the llvm-backend. One option would be to just patch nix provided clang to either look at the system path or alternatively provide versions of clang with the relevant libraries included in its search path, as discussed previously. However, both approaches go somewhat counter to nix philosophy and more importantly, given the discussions around kbuild, I believe it would make more sense to instead design a kbuild YAML/TOML format which nix can consume to supply the extra dependencies various projects require. This way, users wouldn't have to drop into the full nix language for basic/pre-packaged scenarios. Using nix in conjunction with kbuild, we could leverage nix to not only build executables but also provide us with a deterministic developer shell, which is largely consistent across the various distros, thus not relying on any system wide tools.

Roughly speaking we could have a .kbuild file:

[project]
k = ">=5.3.0"
title = "evm-semantics"
version = "0.1.0"

[dependencies.k]
repo = "https://github.com/runtimeverification/k"
rev = "..."

[dependencies.blockchain-k-plugin]
repo = "https://github.com/runtimeverification/blockchain-k-plugin"
rev = "..."

[dependencies.secp256k1]
type = "nix"

[dependencies.runtime.solc]
type = "nix"

...

and a boilerplate nix flake

{
  inputs = {
    dream2nix.url = "github:nix-community/dream2nix";
  };

  outputs = {
    self,
    dream2nix,
  } @ inp:
    (dream2nix.lib.makeFlakeOutputs {
      systems = ["x86_64-linux"];
      config.projectRoot = ./.;
      source = ./.;
      projects = ./projects.toml;
    });
}

where the .kbuild file would actually get translated by dream2nix into a flake via makeFlakeOutputs.

Then, calling something like kbuild shell . would simply call nix develop ., providing us with a shell with k, blockchain plugin, solc, secp256k1, etc.

[Baltoli]

I think that following the conversation Sam and I had about this, I lean towards the dream2nix solution in the long run. The problems that we experience are basically all a result of kompile (and its downstream components llvm-kompile-*) behaving in some scenarios as if it were a C compiler for the purposes of building native extensions to K.

That is, we expect to be able to use C compiler flags with kompile in a way that closely mimics the behaviour of Clang etc. in similar situations (finding libraries, includes, ...). The Nix consensus (as Sam points out) is that C compilers should not be allowed to do so arbitrarily, and should instead be sandboxed inside these environment wrapper scripts.

I think in the long run things will be less painful and more reliable if we work with the Nix consensus, rather than trying to break out of it in some situations. We've made an investment in the Nix tooling, and it seems sensible to make further improvements to our tooling as idiomatic as possible.

Some actions to look into if we do decide this is the right approach (definitely not complete, and in no particular order):

• Audit our projects to get a better understanding of what the dependencies we can't currently build actually are. Is it largely just the blockchain crypto extensions?
• kup should be able to build and run C semantics #48 does the C semantics fit the same conceptual model as the other projects in terms of library use?
• Construct a minimal example of a semantics that uses external dependencies (i.e. a single C++ file) - what would kbuild support for this case look like?
• Tidy up the API exposed by the LLVM backend:
  • LLVM-Backend Generated Interpreter C API Documentation llvm-backend#692
  • Improve LLVM backend documentation llvm-backend#621
  • Duplications between llvm-backend and blockchain-k-plugin llvm-backend#383