Make `nixpkgs` updatable by CI and upgrade `nixpkgs` in all RV repositories

[juliankuners]

This repository provides a nix flake with a nixpkgs flake input that is followed by most other runtime verification repositories that make use of nix. Pinning nixpkgs in all tools, libraries, and frameworks by runtime verification has the benefit that only one copy of nixpkgs is required to build the tools. Otherwise, multiple copies would be required, which includes builds of transitive runtime and build dependencies. This would significantly increase build size and maybe build time, especially the more different nixpkgs copies are used.

The nixpkgs input is pinned to the revision 69493a13eaea0dc4682fd07e8a084f17813dbeeb, which is from 14th May 2024 and therefore already more than 1 year behind the unstable branch of nixpkgs. This is causing issues in other repositories such as haskell-backend, where we want to use a newer version of the haskell compiler or with uv2nix in kontrol, where uv2nix uses functions/derivations in nixpkgs.lib that are not available in the stale revision that we pin.

Currently, there is no mechanism to automatically update nixpkgs in rv-nix-tools. Also, rv-nix-tools is not pinned in the flake files of other runtime verification repositories, see e.g. haskell-backend. This means that currently nixpkgs would get updated everywhere when nix flake update is run by workflows on any update pull requests. In addition, nixpkgs is enforced onto dependent repository from top to bottom. E.g., k makes nixpkgs use the same revision as llvm-backend.

By convention, the revision of nixpkgs to use in a flake and its dependencies is enforced by the respective flake in a bottom-up approach. This makes usage and maintenance of nixpkgs revisions, dependency breakage due to nixpkgs, and usage of these dependencies more intuitive for nix end-users. E.g., consider a scenario where a user defined kontrol as a flake input in a project. In order to pin the revision of nixpkgs to use in the project, by kontrol, and the dependencies of kontrol to the same version, the multiple more lines of overriding are required in a top-down approach in contrast to a single line in case of the bottom-up approach. In addition, these multiple lines require internal implementation details of the flakes.

This issue collectively tracks all pull requests required for the nixpkgs migration to upstream unstable that includes mechanisms to automatically update nixpkgs in the future periodically by CI. In addition, the structure of nixpkgs input enforcement will be refactored in all runtime verification repositories that make use of rv-nix-tools. Finally, devops workflows will be configured and updated to create dedicated update pull requests for rv-nix-tools, which implicitly updates nixpkgs.

Tasks

• in rv-nix-tools:
  • include documentation about how nixpkgs is managed and maintained accross runtime verification repositories
    • Introduce documentation about nixpkgs and flakes at RV #14
  • update nixpkgs in update workflow
    • Add update-version.yml workflow for nixpkgs #15
• in devops:
  • add workflow for automatic periodic update pull requests in other repositories
    • runtimeverification/devops#236
  • configure update pull requests of rv-nix-tools for the following repositories:
    • blockchain-k-plugin
    • c-semantics
    • evm-semantics
    • haskell-backend
    • k
    • komet
    • kontrol
    • llvm-backend
    • mir-semantics
    • wasm-semantics
    • kup
    • imp-semantics
    • skribe
    • kontrol-node
    • runtimeverification/devops#237
  • configure periodic update pull requests of nixpkgs for the following repositories:
    • rv-nix-tools
    • rvsite
    • amp
    • kaas
    • kontrol-web
    • runtimeverification/devops#238
• update flake nixpkgs input structure from top-down to bottom-up, lock rv-nix-tools in nix flake file, and update rv-nix-tools in update workflow:
  • blockchain-k-plugin
    • Update nix flake inputs structure and add rv-nix-tools to dependency update workflow blockchain-k-plugin#217
  • c-semantics
    • runtimeverification/c-semantics#1193
  • evm-semantics
    • Update nix flake inputs structure and add rv-nix-tools to dependency update workflow evm-semantics#2767
  • haskell-backend
    • Update nix flake inputs structure and add dependency update workflow for rv-nix-tools haskell-backend#4109
  • k
    • Update nix flake inputs structure and add rv-nix-tools to dependency update workflow k#4824
  • komet
    • Update nix flake inputs structure and add rv-nix-tools to dependency update workflow komet#82
  • kontrol
    • Update nix flake inputs structure and add rv-nix-tools to dependency update workflow kontrol#1035
  • llvm-backend
    • Update nix flake inputs structure and add rv-nix-tools to dependency update workflow llvm-backend#1207
  • wasm-semantics
    • Update nix flake inputs structure and add rv-nix-tools to dependency update workflow wasm-semantics#727
  • kup
    • Update nix flake inputs structure and add rv-nix-tools to a new dependency update workflow kup#134
  • imp-semantics
    • Migrate from poetry to uv imp-semantics#45
  • skribe
    • Migrate from poetry to uv skribe#19
  • kontrol-node
    • runtimeverification/kontrol-node#42

[juliankuners]

This is currently blocked due to missing reviews.

@ehildenb Could you please review runtimeverification/blockchain-k-plugin#217, runtimeverification/c-semantics#1193, and runtimeverification/kup#134?

@palinatolmach Could you please review runtimeverification/kontrol#1035?

@tothtamas28 Could you please review runtimeverification/llvm-backend#1207 and #15.

After these and runtimeverification/skribe#19 are reviewed, runtimeverification/devops#237 and runtimeverification/devops#238 can be opened for review and merged. Once these are merged as well, nixpkgs can be updated step-by-step across all RV repositories.