Skip to content

Commit e1e0b0b

Browse files
RaoulSchaffranekRaoulSchaffranek
authored
Merge pull request #22 from runtimeverification/fix/komet-node-kdist-semantics
fix(nix): build kdist K semantics so komet-node runs
2 parents 0d6307c + 4bf813f commit e1e0b0b

3 files changed

Lines changed: 174 additions & 52 deletions

File tree

‎flake.nix‎

Lines changed: 33 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -33,18 +33,45 @@
3333
uvOverlay = final: prev: {
3434
uv = uv2nix.packages.${final.system}.uv-bin;
3535
};
36-
komet-nodeOverlay = final: prev: {
37-
komet-node = final.callPackage ./nix/komet-node {
36+
# The k-framework overlay also pulls in a lot of unrelated packages, so we
37+
# only expose the `k` binary that we actually consume.
38+
kOverlay = final: prev: {
39+
k = k-framework.packages.${final.system}.k;
40+
};
41+
komet-nodeOverlay = final: prev:
42+
let
43+
# The Python virtual environment, built against a modern stdenv from
44+
# nixpkgs-unstable (see below). It carries the `komet-node` entrypoint
45+
# together with the `kdist` tool and the K sources for every kdist target.
46+
komet-node-pyk = pkgs.callPackage ./nix/komet-node-pyk {
3847
inherit pyproject-nix pyproject-build-systems uv2nix;
39-
python = final."python${pythonVer}";
48+
python = pkgs."python${pythonVer}";
49+
};
50+
in {
51+
# Build the wrapper against `nixpkgs` (the RV-pinned package set that the K
52+
# toolchain is built and tested against) rather than nixpkgs-unstable, so
53+
# the C/C++ toolchain that kompiles the LLVM semantics matches `k`. The
54+
# compiled semantics run as a subprocess (krun), so there is no ABI
55+
# coupling with the nixpkgs-unstable Python environment.
56+
komet-node = final.callPackage ./nix/komet-node {
57+
inherit komet-node-pyk;
58+
rev = self.rev or null;
4059
};
4160
};
42-
# Use nixpkgs-unstable for the package set so the Python environment is
43-
# built against a modern stdenv on all platforms.
61+
# Use nixpkgs-unstable for the Python package set so the Python environment
62+
# is built against a modern stdenv on all platforms.
4463
pkgs = import nixpkgs-unstable {
4564
inherit system;
4665
overlays = [
4766
uvOverlay
67+
];
68+
};
69+
# The native toolchain for kompiling the K semantics comes from the RV-pinned
70+
# nixpkgs so it matches the `k` binary.
71+
pkgsK = import nixpkgs {
72+
inherit system;
73+
overlays = [
74+
kOverlay
4875
komet-nodeOverlay
4976
];
5077
};
@@ -70,7 +97,7 @@
7097
'';
7198
};
7299
packages = rec {
73-
inherit (pkgs) komet-node;
100+
inherit (pkgsK) komet-node;
74101
default = komet-node;
75102
};
76103
}) // {

‎nix/komet-node-pyk/default.nix‎

Lines changed: 55 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,55 @@
1+
{
2+
lib,
3+
callPackage,
4+
nix-gitignore,
5+
6+
pyproject-nix,
7+
pyproject-build-systems,
8+
uv2nix,
9+
10+
python
11+
}:
12+
let
13+
pyproject-packages = callPackage pyproject-nix.build.packages {
14+
inherit python;
15+
};
16+
17+
# load a uv workspace from a workspace root
18+
workspace = uv2nix.lib.workspace.loadWorkspace {
19+
workspaceRoot = lib.cleanSource (nix-gitignore.gitignoreSourcePure [
20+
../../.gitignore
21+
".github/"
22+
"result*"
23+
# do not include submodule directories that might be initilized empty or non-existent due to nix/git
24+
# otherwise cachix build might not match the version that is requested by `kup`
25+
# TODO: for new projects, add your submodule directories that are not required for nix builds here!
26+
# e.g., `"/docs/external-computation"` with `external-computation` being a git submodule directory
27+
# "/docs/external-computation"
28+
] ../..
29+
);
30+
};
31+
32+
# create overlay
33+
lockFileOverlay = workspace.mkPyprojectOverlay {
34+
# prefer "wheel" over "sdist" due to maintance overhead
35+
# there is no bundled set of overlays for "sdist" in uv2nix, in contrast to poetry2nix
36+
sourcePreference = "wheel";
37+
};
38+
39+
buildSystemsOverlay = import ../komet-node/build-systems-overlay.nix;
40+
41+
# construct package set
42+
pythonSet = pyproject-packages.overrideScope (lib.composeManyExtensions [
43+
# make build tools available by default as these are not necessarily specified in python lock files
44+
pyproject-build-systems.overlays.default
45+
# include all packages from the python lock file
46+
lockFileOverlay
47+
# add build system overrides to certain python packages
48+
buildSystemsOverlay
49+
]);
50+
in
51+
# Expose the full virtual environment (not `mkApplication`): the `komet-node`
52+
# wrapper needs both the `komet-node` entrypoint AND the `kdist` tool (provided
53+
# by the kframework dependency) to build the K semantics. `workspace.deps.default`
54+
# excludes the dev dependency groups, so this is only the runtime closure.
55+
pythonSet.mkVirtualEnv "komet-node-env" workspace.deps.default

‎nix/komet-node/default.nix‎

Lines changed: 86 additions & 46 deletions
Original file line numberDiff line numberDiff line change
@@ -1,55 +1,95 @@
11
{
22
lib,
3-
callPackage,
4-
nix-gitignore,
3+
stdenv,
4+
makeWrapper,
55

6-
pyproject-nix,
7-
pyproject-build-systems,
8-
uv2nix,
6+
clang,
7+
cmake,
8+
git,
9+
k,
10+
boost,
11+
mpfr,
12+
openssl,
13+
gmp,
14+
secp256k1,
15+
which,
916

10-
python
17+
komet-node-pyk,
18+
rev ? null
1119
}:
12-
let
13-
pyproject-util = callPackage pyproject-nix.build.util {};
14-
pyproject-packages = callPackage pyproject-nix.build.packages {
15-
inherit python;
16-
};
20+
stdenv.mkDerivation {
21+
pname = "komet-node";
22+
version = if (rev != null) then rev else "dirty";
1723

18-
# load a uv workspace from a workspace root
19-
workspace = uv2nix.lib.workspace.loadWorkspace {
20-
workspaceRoot = lib.cleanSource (nix-gitignore.gitignoreSourcePure [
21-
../../.gitignore
22-
".github/"
23-
"result*"
24-
# do not include submodule directories that might be initilized empty or non-existent due to nix/git
25-
# otherwise cachix build might not match the version that is requested by `kup`
26-
# TODO: for new projects, add your submodule directories that are not required for nix builds here!
27-
# e.g., `"/docs/external-computation"` with `external-computation` being a git submodule directory
28-
# "/docs/external-computation"
29-
] ../..
30-
);
31-
};
24+
outputs = [
25+
"bin"
26+
# contains kdist artifacts (the compiled K semantics)
27+
"out"
28+
# this empty `dev` output is required as we otherwise get cyclic dependencies between `bin` and `out`
29+
# this is due to a setup-hook creating references in a new directory `nix-support` in either `out` or `dev`
30+
"dev"
31+
];
3232

33-
# create overlay
34-
lockFileOverlay = workspace.mkPyprojectOverlay {
35-
# prefer "wheel" over "sdist" due to maintance overhead
36-
# there is no bundled set of overlays for "sdist" in uv2nix, in contrast to poetry2nix
37-
sourcePreference = "wheel";
38-
};
33+
# The K sources for every kdist target (`soroban-semantics.*` from the `komet`
34+
# dependency and `komet-node.*` from this project) ship inside `komet-node-pyk`,
35+
# so there are no sources to unpack here; the build only needs a working
36+
# directory to place the kdist output into.
37+
dontUnpack = true;
38+
39+
buildInputs = [
40+
clang
41+
cmake
42+
git
43+
boost
44+
mpfr
45+
openssl
46+
gmp
47+
secp256k1
48+
komet-node-pyk
49+
k
50+
];
51+
52+
nativeBuildInputs = [ makeWrapper ];
53+
54+
dontUseCmakeConfigure = true;
3955

40-
buildSystemsOverlay = import ./build-systems-overlay.nix;
41-
42-
# construct package set
43-
pythonSet = pyproject-packages.overrideScope (lib.composeManyExtensions [
44-
# make build tools available by default as these are not necessarily specified in python lock files
45-
pyproject-build-systems.overlays.default
46-
# include all packages from the python lock file
47-
lockFileOverlay
48-
# add build system overrides to certain python packages
49-
buildSystemsOverlay
50-
]);
51-
in pyproject-util.mkApplication {
52-
# default dependancy group enables no optional dependencies and no dependency-groups
53-
venv = pythonSet.mkVirtualEnv "komet-node-env" workspace.deps.default;
54-
package = pythonSet.komet-node;
56+
enableParallelBuilding = true;
57+
58+
# `kdist` writes the compiled semantics under `$XDG_CACHE_HOME/kdist-<hash>/`.
59+
# Build the same targets the Makefile's `kdist-build` does. The `komet-node.*`
60+
# targets pull in `soroban-semantics.source` as a dependency automatically.
61+
#
62+
# Cap concurrency at 2 (matching the Makefile's `kdist-build`): each LLVM/Haskell
63+
# `kompile` job links a large generated interpreter and peaks at several GB of
64+
# RAM, so an unbounded `-j$NIX_BUILD_CORES` can OOM the builder on machines with
65+
# many cores but limited memory.
66+
buildPhase = ''
67+
runHook preBuild
68+
XDG_CACHE_HOME=$(pwd) ${
69+
lib.optionalString
70+
(stdenv.isAarch64 && stdenv.isDarwin)
71+
"APPLE_SILICON=true"
72+
} kdist -v build -j2 'soroban-semantics.*' 'komet-node.*'
73+
runHook postBuild
74+
'';
75+
76+
installPhase = ''
77+
runHook preInstall
78+
mkdir -p $bin/bin
79+
mkdir -p $out/kdist
80+
81+
cp -r ./kdist-*/* $out/kdist/
82+
83+
# Wrap the `komet-node` entrypoint so that, at runtime, it finds the compiled
84+
# semantics via `KDIST_DIR` and the K tools (krun/kore) via `PATH`.
85+
makeWrapper ${komet-node-pyk}/bin/komet-node $bin/bin/komet-node \
86+
--prefix PATH : ${lib.makeBinPath [ which k ]} \
87+
--set KDIST_DIR $out/kdist
88+
runHook postInstall
89+
'';
90+
91+
meta = {
92+
description = "Local development testnet for Stellar based on K semantics";
93+
mainProgram = "komet-node";
94+
};
5595
}

0 commit comments

Comments
 (0)