From 788ac2938ad855713d739f2f37ceef67ea8d6ef8 Mon Sep 17 00:00:00 2001 From: Raoul Date: Mon, 20 Jul 2026 13:27:25 +0000 Subject: [PATCH 1/4] Add dev.sh for local iteration across the semantics chain Working on a debugger change that also needs a komet/wasm-semantics change previously meant manually cloning the chain, wiring pins, and rebuilding each repo by hand. The chain is pinned by uv git dependencies (not Nix flake inputs), so `kup --override` can't reach komet/wasm-semantics. dev.sh is a single front-end for that workflow: - setup checks the chain out under .deps/ (gitignored) at the versions each downstream currently pins, and wires them with uv path sources so an edit flows up the chain with no version bumps. - build/shell drive the fast incremental loop (nix devShell + uv + kdist); use installs the local build as the debugger's komet-node for parity. - pr open/status/link/unlink opens coordinated PRs across the repos. nix/uv/kdist stay hidden behind the script. CONTRIBUTING documents the three modes (debug / change semantics / upstream) and notes this repo carries no version-pin files of its own. --- .gitignore | 1 + CONTRIBUTING.md | 46 +++++++ scripts/dev.sh | 336 ++++++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 383 insertions(+) create mode 100755 scripts/dev.sh diff --git a/.gitignore b/.gitignore index 1098682..8a833dc 100644 --- a/.gitignore +++ b/.gitignore @@ -1,4 +1,5 @@ node_modules/ +.deps/ dist/ out/ coverage/ diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 15d9a18..1d980a4 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -46,6 +46,52 @@ extension loaded and the [`examples/`](examples/) workspace open. Pick a configuration from the Run and Debug view — the **Replay … with symbols** configs need no toolchain at all. +## Changing the semantics (komet / wasm-semantics) + +The debugger consumes an upstream chain, +`komet-node → komet → wasm-semantics`, but you rarely touch it. Pick your mode: + +**1. Just debugging (almost always).** Do nothing special — the devcontainer +already has the `komet-node` binary (from `kup`). Press **F5**. You never need +nix, uv, or any of the tooling below. + +**2. Changing the semantics and seeing it in the debugger.** Use the single +front-end [`scripts/dev.sh`](scripts/dev.sh): + +```bash +./scripts/dev.sh setup # check out the chain into .deps/ and wire it up +# …edit .deps/wasm-semantics or .deps/komet… +./scripts/dev.sh build # fast incremental rebuild +./scripts/dev.sh use # make it the debugger's komet-node, then press F5 +``` + +**3. Upstreaming the change as PRs.** Once you have commits on a shared branch in +the checkouts, `dev.sh pr open ` opens a cross-linked PR in each +repo (`pr status ` / `--dry-run` to preview first). + +That's the whole developer surface. Everything else is plumbing the script drives +for you: + +- You never run `nix`, `uv`, or `kdist` by hand — `setup`/`build` do. +- **`.deps/`** (leading dot) is generated and gitignored — throwaway local + checkouts; delete it any time to reset. Not to be confused with the committed + `deps/` folders in komet/komet-node, which hold version pins (below). +- This repo carries **no version-pin files**. The pins that connect the chain + (`deps/*_release`, `uv.lock`, flake inputs) live upstream in komet/komet-node + and are bumped by CI, not by you. + +
Why it needs checkouts (background) + +The chain is pinned by **uv git dependencies**, not Nix flake inputs, so +`kup --override` can't reach `komet`/`wasm-semantics`. `setup` therefore checks +the repos out side-by-side (at the versions currently pinned, or `--tip` for +latest) and wires them with uv **path sources** so an edit flows up the chain +with no version bumps. `build`/`shell` are the fast inner loop (`kdist` caches +per target, toolchain from komet-node's Nix dev shell); `use` does one Nix +realize so the debugger gets the exact release build — doubling as a parity +check. Revert with `kup install komet-node`. +
+ ## Testing conventions - **Write tests first.** New behavior should arrive with a failing test that diff --git a/scripts/dev.sh b/scripts/dev.sh new file mode 100755 index 0000000..8b260db --- /dev/null +++ b/scripts/dev.sh @@ -0,0 +1,336 @@ +#!/usr/bin/env bash +# +# dev.sh — one entry point for working across the semantics chain. +# +# stellar-debugger -> komet-node -> komet -> wasm-semantics +# +# You only need this when you are CHANGING the semantics. For plain debugging the +# devcontainer already has the komet-node binary (via `kup`) — just press F5. +# +# When you are changing the semantics: +# +# ./scripts/dev.sh setup # check out the chain + wire it together +# …edit .deps/wasm-semantics or .deps/komet… +# ./scripts/dev.sh build # fast incremental rebuild +# ./scripts/dev.sh use # make it the debugger's komet-node, then press F5 +# +# When you are upstreaming that change as PRs across the repos: +# +# ./scripts/dev.sh pr status # what would be opened +# ./scripts/dev.sh pr open [--draft] [--dry-run] +# +# Everything below (nix, uv, kdist, checkouts) is plumbing this script drives for +# you — you never run those directly. The chain is pinned by uv git dependencies, +# not flake inputs, which is why local iteration needs checkouts wired with uv +# path sources rather than `kup --override`. Details: CONTRIBUTING.md. +# +set -euo pipefail + +# --- configuration --------------------------------------------------------- +REPO_ROOT="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)" +CHAIN_DIR="${DEV_DEPS_DIR:-$REPO_ROOT/.deps}" +GH_ORG="https://github.com/runtimeverification" +# Leaf -> root: build/PR order so an upstream checkout/PR always exists first. +CHAIN_ORDER=(wasm-semantics komet komet-node) + +SENTINEL_OPEN="# >>> dev.sh: local path sources (generated; do not commit) >>>" +SENTINEL_CLOSE="# <<< dev.sh <<<" + +# `pr link` pin rewrites: repo|dep|tag-pin-regex|url-prefix|url-suffix +LINK_KOMET_NODE='komet-node|komet|komet.git@v[0-9.]*|komet.git@|' +LINK_KOMET='komet|pykwasm|wasm-semantics.git@v[0-9.]*#subdirectory=pykwasm|wasm-semantics.git@|#subdirectory=pykwasm' + +log() { printf '\033[1;34m[dev]\033[0m %s\n' "$*"; } +warn() { printf '\033[1;33m[dev]\033[0m %s\n' "$*" >&2; } +die() { printf '\033[1;31m[dev]\033[0m %s\n' "$*" >&2; exit 1; } +need() { command -v "$1" >/dev/null 2>&1 || die "required tool not found on PATH: $1"; } + +# --- checkout helpers ------------------------------------------------------ + +dir_of() { printf '%s/%s' "$CHAIN_DIR" "$1"; } +default_of() { git -C "$(dir_of "$1")" symbolic-ref --short refs/remotes/origin/HEAD 2>/dev/null | sed 's#^origin/##'; } + +# Ensure is checked out under .deps/ with tags available. Clones if +# absent, otherwise fetches (branches + tags). Does NOT move HEAD. +fetch_repo() { + local repo="$1" dir; dir="$(dir_of "$1")" + if [[ -d "$dir/.git" ]]; then + log "fetching $repo" + git -C "$dir" fetch --quiet --tags origin + else + log "cloning $repo" + git clone --quiet "$GH_ORG/$repo.git" "$dir" + fi +} + +# Move to . Refuses if the tree carries real local work (ignoring the +# generated path-source block + relock churn), so we never discard a dev's edits. +checkout_rev() { + local repo="$1" rev="$2" dir; dir="$(dir_of "$1")" + if ! git -C "$dir" diff --quiet || ! git -C "$dir" diff --cached --quiet; then + if git -C "$dir" status --porcelain | grep -qvE 'pyproject\.toml|uv\.lock'; then + warn "$repo: local changes present; leaving at $(git -C "$dir" rev-parse --abbrev-ref HEAD)" + return + fi + git -C "$dir" checkout --quiet -- pyproject.toml uv.lock 2>/dev/null || true + fi + git -C "$dir" checkout --quiet "$rev" + log "$repo -> $rev" +} + +# Extract the version a downstream pyproject pins for , e.g. "0.1.85" from +# `komet.git@v0.1.85`. Empty if not found. +pinned_version() { + grep -oE "${2}@v[0-9.]+" "$1" 2>/dev/null | head -1 | grep -oE '[0-9.]+$' || true +} + +# Append a [tool.uv.sources] block to pointing deps at local +# checkouts. Idempotent (keyed on the sentinel); refuses to clobber a hand-written +# [tool.uv.sources]. Usage: inject_sources "=" ... +inject_sources() { + local file="$1"; shift + [[ -f "$file" ]] || die "no pyproject.toml at $file" + if grep -qF "$SENTINEL_OPEN" "$file"; then + local tmp; tmp="$(mktemp)" + sed "/$(printf '%s' "$SENTINEL_OPEN" | sed 's/[.[\*^$/]/\\&/g')/,/$(printf '%s' "$SENTINEL_CLOSE" | sed 's/[.[\*^$/]/\\&/g')/d" "$file" > "$tmp" + mv "$tmp" "$file" + elif grep -qE '^\[tool\.uv\.sources\]' "$file"; then + die "$file already has a hand-written [tool.uv.sources]; refusing to edit." + fi + { + printf '\n%s\n[tool.uv.sources]\n' "$SENTINEL_OPEN" + local pair + for pair in "$@"; do + printf '%s = { path = "%s", editable = true }\n' "${pair%%=*}" "${pair#*=}" + done + printf '%s\n' "$SENTINEL_CLOSE" + } >> "$file" + log "wired path sources into ${file#"$REPO_ROOT"/}" +} + +# Run a command inside komet-node's Nix dev shell (uv + kompile + toolchain). +# `nix develop --command` does NOT cd into the flake dir, so cd explicitly. +in_devshell() { + need nix + local dir; dir="$(dir_of komet-node)" + nix develop --extra-experimental-features 'nix-command flakes' \ + "$dir" --command bash -lc "cd '$dir' && $1" +} + +# --- semantics-dev subcommands --------------------------------------------- + +cmd_setup() { + need git + local tip=""; [[ "${1:-}" == "--tip" ]] && tip=1 + mkdir -p "$CHAIN_DIR" + + # komet-node is the root of what we build; take it at its default branch tip. + fetch_repo komet-node + + # Resolve each upstream at the version its downstream PINS, not at tip. Pulling + # to tip skews the K-framework version (komet-node constrains `kframework`, but + # tip pykwasm may need newer K) and uv resolution fails. Editing relative to the + # current release is the real dev scenario; --tip overrides (then bump pins). + fetch_repo komet + local kv; kv="$(pinned_version "$CHAIN_DIR/komet-node/pyproject.toml" 'komet\.git')" + if [[ -n "$tip" ]]; then log "komet: --tip (default branch)" + else [[ -n "$kv" ]] || die "could not read komet pin from komet-node/pyproject.toml"; checkout_rev komet "v$kv"; fi + + fetch_repo wasm-semantics + local pv; pv="$(pinned_version "$CHAIN_DIR/komet/pyproject.toml" 'wasm-semantics\.git')" + if [[ -n "$tip" ]]; then log "wasm-semantics: --tip (default branch)" + else [[ -n "$pv" ]] || die "could not read pykwasm pin from komet/pyproject.toml"; checkout_rev wasm-semantics "v$pv"; fi + + # uv only honours sources in the *root* project, so komet-node overrides BOTH + # komet and (transitively) pykwasm; komet gets pykwasm too for standalone use. + inject_sources "$CHAIN_DIR/komet/pyproject.toml" "pykwasm=../wasm-semantics/pykwasm" + inject_sources "$CHAIN_DIR/komet-node/pyproject.toml" "komet=../komet" "pykwasm=../wasm-semantics/pykwasm" + + log "checkouts wired. Building the chain (first build is slow)…" + cmd_build + printf '\n'; log "setup complete — edit under .deps/, then: dev.sh build && dev.sh use" +} + +cmd_build() { + [[ -d "$(dir_of komet-node)" ]] || die "run 'setup' first" + log "rebuilding semantics (incremental; only changed kdist targets recompile)" + in_devshell 'uv sync && make kdist-build' + log "build done" +} + +cmd_shell() { + [[ -d "$(dir_of komet-node)" ]] || die "run 'setup' first" + need nix + log "entering komet-node dev shell (uv/kdist/komet-node available); exit to leave" + nix develop --extra-experimental-features 'nix-command flakes' "$(dir_of komet-node)" +} + +cmd_use() { + [[ -d "$(dir_of komet-node)" ]] || die "run 'setup' first" + need kup + log "installing local komet-node onto PATH via kup (exact release build)…" + kup install komet-node --version "$(dir_of komet-node)" + log "done — the debugger's default 'komet-node' is now your local build." + log "revert with: kup install komet-node" +} + +cmd_status() { + for repo in "${CHAIN_ORDER[@]}"; do + local dir; dir="$(dir_of "$repo")" + if [[ -d "$dir/.git" ]]; then + printf ' %-16s %s\n' "$repo" "$(git -C "$dir" log -1 --format='%h %s' 2>/dev/null)" + else + printf ' %-16s (not checked out)\n' "$repo" + fi + done +} + +# --- pr subcommands (coordinated upstreaming) ------------------------------ + +# Does have locally, ahead of its remote default branch? +pr_participates() { + local dir; dir="$(dir_of "$1")" + [[ -d "$dir/.git" ]] || return 1 + git -C "$dir" show-ref --verify --quiet "refs/heads/$2" || return 1 + [[ "$(git -C "$dir" rev-list --count "origin/$(default_of "$1")..$2" 2>/dev/null || echo 0)" -gt 0 ]] +} + +pr_status() { + local branch="${1:?usage: pr status }" + for repo in "${CHAIN_ORDER[@]}"; do + local dir; dir="$(dir_of "$repo")" + if [[ ! -d "$dir/.git" ]]; then printf ' %-16s (not checked out)\n' "$repo"; continue; fi + if pr_participates "$repo" "$branch"; then + local base; base="$(default_of "$repo")" + printf ' %-16s \033[1;32mparticipates\033[0m — %s commit(s) ahead of %s\n' \ + "$repo" "$(git -C "$dir" rev-list --count "origin/$base..$branch")" "$base" + else + printf ' %-16s —\n' "$repo" + fi + done +} + +pr_apply_link() { + local branch="$2" repo dep regex prefix suffix + IFS='|' read -r repo dep regex prefix suffix <<< "$1" + local dir file; dir="$(dir_of "$repo")"; file="$dir/pyproject.toml" + [[ -f "$file" ]] || { warn "$repo: no pyproject.toml; skipping"; return; } + grep -qE "$regex" "$file" || { log "$repo: $dep pin already rewritten or absent; skipping"; return; } + sed -i -E "s#${regex}#${prefix}${branch}${suffix}#" "$file" + git -C "$dir" add pyproject.toml + git -C "$dir" commit -q -m "TEMP: point $dep at branch $branch (revert before merge)" + log "$repo: $dep -> @$branch (committed; 'pr unlink' to revert)" +} + +pr_link() { + local branch="${1:?usage: pr link }"; need git + pr_apply_link "$LINK_KOMET" "$branch" + pr_apply_link "$LINK_KOMET_NODE" "$branch" + warn "Pins now point at '$branch'. Re-lock (dev.sh build) before pushing;" + warn "these TEMP commits MUST be reverted (pr unlink) before merging." +} + +pr_unlink() { + local branch="${1:?usage: pr unlink }"; need git + for repo in komet komet-node; do + local dir; dir="$(dir_of "$repo")"; [[ -d "$dir/.git" ]] || continue + if git -C "$dir" log -1 --format='%s' 2>/dev/null | grep -q "^TEMP: point .* at branch $branch"; then + git -C "$dir" reset -q --hard HEAD~1 + log "$repo: reverted TEMP link commit" + fi + done +} + +pr_open() { + local branch="" title="" body="" draft="" dry="" + while [[ $# -gt 0 ]]; do + case "$1" in + --title) title="$2"; shift 2 ;; + --body) body="$2"; shift 2 ;; + --draft) draft="--draft"; shift ;; + --dry-run) dry=1; shift ;; + -*) die "unknown flag: $1" ;; + *) branch="$1"; shift ;; + esac + done + [[ -n "$branch" ]] || die "usage: pr open [--title T] [--body B] [--draft] [--dry-run]" + need git; [[ -n "$dry" ]] || need gh + + local participating=() + for repo in "${CHAIN_ORDER[@]}"; do pr_participates "$repo" "$branch" && participating+=("$repo"); done + [[ ${#participating[@]} -gt 0 ]] || die "no repo has commits on branch '$branch' (see: pr status $branch)" + log "participating (leaf->root): ${participating[*]}" + + declare -A pr_url=() + for repo in "${participating[@]}"; do + local dir base links="" up; dir="$(dir_of "$repo")"; base="$(default_of "$repo")" + for up in "${participating[@]}"; do + [[ "$up" == "$repo" ]] && break + [[ -n "${pr_url[$up]:-}" ]] && links+="- upstream: ${pr_url[$up]}"$'\n' + done + local fbody="${body:-Coordinated change across the semantics chain.}" + [[ -n "$links" ]] && fbody+=$'\n\n'"Chain:"$'\n'"$links" + if [[ -n "$dry" ]]; then + log "[dry-run] $repo: push $branch; gh pr create --base $base --title \"${title:-$branch}\" $draft" + pr_url[$repo]="(dry-run)"; continue + fi + log "$repo: pushing $branch"; git -C "$dir" push -u origin "$branch" + log "$repo: opening PR against $base" + pr_url[$repo]="$(cd "$dir" && gh pr create --base "$base" --head "$branch" \ + --title "${title:-$branch}" --body "$fbody" $draft 2>/dev/null || gh pr view "$branch" --json url -q .url)" + log "$repo: ${pr_url[$repo]}" + done + log "done. PRs:" + for repo in "${participating[@]}"; do printf ' %-16s %s\n' "$repo" "${pr_url[$repo]}"; done +} + +cmd_pr() { + local sub="${1:-}"; shift || true + case "$sub" in + status) pr_status "$@" ;; + link) pr_link "$@" ;; + unlink) pr_unlink "$@" ;; + open) pr_open "$@" ;; + *) die "unknown pr subcommand: $sub (status|link|unlink|open)" ;; + esac +} + +# --- entry point ----------------------------------------------------------- + +usage() { + cat <<'EOF' +dev.sh — work across the semantics chain (komet-node -> komet -> wasm-semantics) + +Only needed when CHANGING the semantics. For plain debugging, the devcontainer +already has komet-node (via kup) — just press F5. + + setup [--tip] check out the chain (at pinned versions) + wire it together + build fast incremental rebuild after an edit + shell drop into the komet-node dev shell + use install the local build as the debugger's komet-node + status show checked-out revisions + + pr status show which repos would open a PR + pr open [--draft] [--dry-run] [--title T] [--body B] + pr link point downstream pins at sibling branches (for CI) + pr unlink revert the link commits + +nix/uv/kdist are plumbing this script drives — you never run them directly. +EOF +} + +main() { + local cmd="${1:-}"; shift || true + case "$cmd" in + setup) cmd_setup "$@" ;; + build) cmd_build "$@" ;; + shell) cmd_shell "$@" ;; + use) cmd_use "$@" ;; + status) cmd_status "$@" ;; + pr) cmd_pr "$@" ;; + ""|-h|--help|help) usage ;; + *) die "unknown command: $cmd (try --help)" ;; + esac +} + +main "$@" From b629a67d476e90aa4805d134e1643cf31612828f Mon Sep 17 00:00:00 2001 From: Raoul Date: Mon, 20 Jul 2026 14:37:09 +0000 Subject: [PATCH 2/4] Build komet-node from committed git sources in dev.sh use MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `use` installs a release-parity komet-node via kup + nix, which copies only the flake dir into the Nix store and so cannot consume the editable PATH sources the fast loop (build/shell) relies on. Rework it to: - Point komet-node at any locally-*changed* chain repo (komet, wasm-semantics/pykwasm) via a git file:// source pinned to its committed HEAD — the same git -> uv2nix -> nix path a real release takes — and keep the upstream pin for repos still on their pinned tag. - Refuse to proceed if a changed repo has uncommitted work (nix builds from committed history only), ignoring generated pyproject/uv.lock churn. - Always restore the editable path sources afterward so `build` stays instant, even when the build fails. Factor the shared block-writer out of inject_sources into write_uv_sources, and add pinned_for() to resolve each repo's downstream pin. Also install the GitHub CLI in the devcontainer (used by `dev.sh pr`), and drop the komet-node path override from examples/.vscode/settings.json since the local build now lands on PATH. --- .devcontainer/Dockerfile | 9 ++++ examples/.vscode/settings.json | 7 +-- scripts/dev.sh | 78 ++++++++++++++++++++++++++++++---- 3 files changed, 79 insertions(+), 15 deletions(-) diff --git a/.devcontainer/Dockerfile b/.devcontainer/Dockerfile index 71906bb..9a67ba9 100755 --- a/.devcontainer/Dockerfile +++ b/.devcontainer/Dockerfile @@ -36,6 +36,15 @@ RUN curl -sSL \ | tar xz -C /usr/local/bin stellar \ && stellar --version +# --- GitHub CLI (prebuilt) ------------------------------------------------- +# Used by `scripts/dev.sh pr` to open coordinated PRs across the semantics chain. +ARG GH_CLI_VERSION=2.63.2 +RUN curl -sSL \ + "https://github.com/cli/cli/releases/download/v${GH_CLI_VERSION}/gh_${GH_CLI_VERSION}_linux_amd64.tar.gz" \ + | tar xz -C /usr/local --strip-components=1 \ + "gh_${GH_CLI_VERSION}_linux_amd64/bin/gh" \ + && gh --version + # --- Nix prep -------------------------------------------------------------- # Single-user Nix is installed under /nix as the `node` user (no systemd in the # container). Pre-create /nix with node ownership so the installer can write it. diff --git a/examples/.vscode/settings.json b/examples/.vscode/settings.json index dc73fc0..0db3279 100644 --- a/examples/.vscode/settings.json +++ b/examples/.vscode/settings.json @@ -1,8 +1,3 @@ { - // The nix-cached `komet-node` on $PATH in this devcontainer predates the fix - // for value-returning contract calls (it hardcoded a Void result and got stuck - // on any function returning a value). The fixed build lives in the uv venv, so - // point the extension at it here. Remove this once the nix cache ships the fix - // and plain `komet-node` on $PATH is current. - "soroban.kometNode.path": "/home/node/.komet-node/bin/komet-node" + } diff --git a/scripts/dev.sh b/scripts/dev.sh index 8b260db..8a259de 100755 --- a/scripts/dev.sh +++ b/scripts/dev.sh @@ -84,10 +84,19 @@ pinned_version() { grep -oE "${2}@v[0-9.]+" "$1" 2>/dev/null | head -1 | grep -oE '[0-9.]+$' || true } -# Append a [tool.uv.sources] block to pointing deps at local -# checkouts. Idempotent (keyed on the sentinel); refuses to clobber a hand-written -# [tool.uv.sources]. Usage: inject_sources "=" ... -inject_sources() { +# The version is pinned at by its immediate downstream (empty if unknown). +pinned_for() { + case "$1" in + komet) pinned_version "$CHAIN_DIR/komet-node/pyproject.toml" 'komet\.git' ;; + wasm-semantics) pinned_version "$CHAIN_DIR/komet/pyproject.toml" 'wasm-semantics\.git' ;; + esac +} + +# Write a generated [tool.uv.sources] block into . Each remaining arg +# is "=", e.g. 'komet={ path = "../komet", editable = true }'. +# Idempotent (keyed on the sentinel); refuses to clobber a hand-written block. An +# empty arg list leaves an empty, override-free block (deps fall back to their pins). +write_uv_sources() { local file="$1"; shift [[ -f "$file" ]] || die "no pyproject.toml at $file" if grep -qF "$SENTINEL_OPEN" "$file"; then @@ -100,11 +109,21 @@ inject_sources() { { printf '\n%s\n[tool.uv.sources]\n' "$SENTINEL_OPEN" local pair - for pair in "$@"; do - printf '%s = { path = "%s", editable = true }\n' "${pair%%=*}" "${pair#*=}" - done + for pair in "$@"; do printf '%s = %s\n' "${pair%%=*}" "${pair#*=}"; done printf '%s\n' "$SENTINEL_CLOSE" } >> "$file" +} + +# Wire deps at local checkouts via editable PATH sources — the fast-loop wiring +# (`build`/`shell` run uv against the real filesystem, so out-of-tree paths are +# fine). Usage: inject_sources "=" ... +inject_sources() { + local file="$1"; shift + local -a specs=(); local pair + for pair in "$@"; do + specs+=("${pair%%=*}={ path = \"${pair#*=}\", editable = true }") + done + write_uv_sources "$file" "${specs[@]}" log "wired path sources into ${file#"$REPO_ROOT"/}" } @@ -165,11 +184,52 @@ cmd_shell() { nix develop --extra-experimental-features 'nix-command flakes' "$(dir_of komet-node)" } +# `use` builds komet-node with a real `nix build` (release parity), which copies +# ONLY the flake dir into the Nix store — so it cannot consume the editable PATH +# sources the fast loop uses (`../komet` escapes the store, "do not know how to +# unpack …/source/../komet"). So for `use` we point komet-node at any locally- +# *changed* chain repo via a git file:// source at its committed HEAD — the exact +# git -> uv2nix -> nix pipeline a real release uses — and drop the override for +# unchanged repos (they build from their upstream pins). nix git-fetch sees only +# committed history, so changes must be committed first. The fast-loop path +# sources are restored afterwards so `build` stays instant. cmd_use() { [[ -d "$(dir_of komet-node)" ]] || die "run 'setup' first" - need kup + need kup; need git + + local -a git_specs=() + local repo dir head pintag + for repo in komet wasm-semantics; do + dir="$(dir_of "$repo")"; [[ -d "$dir/.git" ]] || continue + head="$(git -C "$dir" rev-parse HEAD)" + pintag="v$(pinned_for "$repo")" + # Unchanged (still exactly on the pinned tag) -> keep the upstream pin. + if git -C "$dir" rev-parse -q --verify "$pintag^{commit}" >/dev/null 2>&1 \ + && [[ "$(git -C "$dir" rev-parse "$pintag^{commit}")" == "$head" ]]; then + continue + fi + # Changed -> must be committed; nix builds from committed history only. Ignore + # the generated pyproject/uv.lock churn when judging "uncommitted". + if git -C "$dir" status --porcelain -- . ':!pyproject.toml' ':!uv.lock' | grep -q .; then + die "$repo has uncommitted changes — commit them before 'use' (nix builds from committed history). See: git -C '$dir' status" + fi + case "$repo" in + komet) git_specs+=("komet={ git = \"file://$dir\", rev = \"$head\" }") ;; + wasm-semantics) git_specs+=("pykwasm={ git = \"file://$dir\", rev = \"$head\", subdirectory = \"pykwasm\" }") ;; + esac + log "$repo: local build -> git file:// @ ${head:0:7}" + done + [[ ${#git_specs[@]} -gt 0 ]] || warn "no local changes vs pins — 'use' will rebuild the pinned release." + log "installing local komet-node onto PATH via kup (exact release build)…" - kup install komet-node --version "$(dir_of komet-node)" + # Swap the fast-loop path sources for git sources nix can build, re-lock, build. + write_uv_sources "$CHAIN_DIR/komet-node/pyproject.toml" "${git_specs[@]}" + local rc=0 + { in_devshell 'uv lock' && kup install komet-node --version "$(dir_of komet-node)"; } || rc=$? + # Always restore the editable path sources so the fast loop keeps working. + inject_sources "$CHAIN_DIR/komet-node/pyproject.toml" "komet=../komet" "pykwasm=../wasm-semantics/pykwasm" + in_devshell 'uv lock' >/dev/null 2>&1 || true + [[ $rc -eq 0 ]] || die "use failed (see above); restored fast-loop path sources." log "done — the debugger's default 'komet-node' is now your local build." log "revert with: kup install komet-node" } From 7397d03913121f2c272c6c7d20a6764b54662312 Mon Sep 17 00:00:00 2001 From: Raoul Date: Mon, 20 Jul 2026 17:06:23 +0000 Subject: [PATCH 3/4] Provide more info on status sub command --- scripts/dev.sh | 72 +++++++++++++++++++++++++++++++++++++++++++++----- 1 file changed, 66 insertions(+), 6 deletions(-) diff --git a/scripts/dev.sh b/scripts/dev.sh index 8a259de..8ead0d3 100755 --- a/scripts/dev.sh +++ b/scripts/dev.sh @@ -234,14 +234,74 @@ cmd_use() { log "revert with: kup install komet-node" } +# Current local branch of , or "detached@" when not on a branch +# (the normal pinned state sits detached at a version tag). +current_branch() { + local dir; dir="$(dir_of "$1")" + local b; b="$(git -C "$dir" symbolic-ref --short -q HEAD || true)" + if [[ -n "$b" ]]; then printf '%s' "$b"; return; fi + local t; t="$(git -C "$dir" describe --tags --exact-match 2>/dev/null || true)" + printf 'detached@%s' "${t:-$(git -C "$dir" rev-parse --short HEAD)}" +} + +# Working-tree state of , ignoring the generated uv wiring churn (dev.sh +# rewrites the root pyproject.toml + uv.lock, so those are never "real" edits). +worktree_state() { + local dir; dir="$(dir_of "$1")" + local porcelain; porcelain="$(git -C "$dir" status --porcelain)" + [[ -z "$porcelain" ]] && { printf 'clean'; return; } + local real; real="$(printf '%s\n' "$porcelain" | grep -vE ' (pyproject\.toml|uv\.lock)$' || true)" + [[ -z "$real" ]] && { printf 'clean (only generated wiring)'; return; } + printf '%s uncommitted change(s)' "$(printf '%s\n' "$real" | grep -c .)" +} + +# Whether 's current branch exists on origin, and how it relates to HEAD. +# Uses ls-remote (network) so it reflects the real remote, not a stale tracking ref. +remote_state() { + local repo="$1" branch="$2" dir; dir="$(dir_of "$repo")" + [[ "$branch" == detached@* ]] && { printf 'n/a (detached)'; return; } + local remote_sha + remote_sha="$(GIT_TERMINAL_PROMPT=0 git -C "$dir" ls-remote --heads origin "$branch" 2>/dev/null | cut -f1)" + [[ -z "$remote_sha" ]] && { printf 'not pushed'; return; } + local local_sha; local_sha="$(git -C "$dir" rev-parse HEAD)" + if [[ "$remote_sha" == "$local_sha" ]]; then printf 'pushed (up to date)' + elif git -C "$dir" merge-base --is-ancestor "$remote_sha" "$local_sha" 2>/dev/null; then printf 'pushed (local ahead — push again)' + else printf 'pushed (diverged)'; fi +} + +# Open-PR / merged state of 's branch on GitHub. Needs gh + jq; one PR line +# answers both "is there an open PR?" (OPEN) and "merged into the default branch?" +# (MERGED) since a branch has at most one live PR to its base. +pr_state() { + local repo="$1" branch="$2" + [[ "$branch" == detached@* ]] && { printf 'n/a (detached)'; return; } + command -v gh >/dev/null 2>&1 || { printf 'unknown (gh not installed)'; return; } + command -v jq >/dev/null 2>&1 || { printf 'unknown (jq not installed)'; return; } + local json + json="$(gh pr list --repo "runtimeverification/$repo" --head "$branch" \ + --state all --limit 1 --json number,state,url 2>/dev/null)" \ + || { printf 'unknown (gh error / not authenticated)'; return; } + [[ -z "$json" || "$json" == "[]" ]] && { printf 'none'; return; } + printf '#%s %s — %s' \ + "$(printf '%s' "$json" | jq -r '.[0].number')" \ + "$(printf '%s' "$json" | jq -r '.[0].state')" \ + "$(printf '%s' "$json" | jq -r '.[0].url')" +} + cmd_status() { + local repo dir branch for repo in "${CHAIN_ORDER[@]}"; do - local dir; dir="$(dir_of "$repo")" - if [[ -d "$dir/.git" ]]; then - printf ' %-16s %s\n' "$repo" "$(git -C "$dir" log -1 --format='%h %s' 2>/dev/null)" - else - printf ' %-16s (not checked out)\n' "$repo" + dir="$(dir_of "$repo")" + if [[ ! -d "$dir/.git" ]]; then + printf '\n \033[1m%s\033[0m\n (not checked out)\n' "$repo" + continue fi + branch="$(current_branch "$repo")" + printf '\n \033[1m%s\033[0m %s\n' "$repo" "$(git -C "$dir" log -1 --format='%h %s' 2>/dev/null)" + printf ' branch %s\n' "$branch" + printf ' worktree %s\n' "$(worktree_state "$repo")" + printf ' remote %s\n' "$(remote_state "$repo" "$branch")" + printf ' PR %s\n' "$(pr_state "$repo" "$branch")" done } @@ -368,7 +428,7 @@ already has komet-node (via kup) — just press F5. build fast incremental rebuild after an edit shell drop into the komet-node dev shell use install the local build as the debugger's komet-node - status show checked-out revisions + status per-repo: branch, worktree, push state, and PR/merge state pr status show which repos would open a PR pr open [--draft] [--dry-run] [--title T] [--body B] From 026d6d5b70a28eeb692721b3d0a8d9a8e109ce95 Mon Sep 17 00:00:00 2001 From: Raoul Date: Mon, 20 Jul 2026 17:21:37 +0000 Subject: [PATCH 4/4] Add an .ssh-volume to persist key pairs over rebuilds. --- .devcontainer/devcontainer.json | 5 +++-- CONTRIBUTING.md | 22 ++++++++++++++++++++++ 2 files changed, 25 insertions(+), 2 deletions(-) diff --git a/.devcontainer/devcontainer.json b/.devcontainer/devcontainer.json index 8e29ee5..c60efdb 100755 --- a/.devcontainer/devcontainer.json +++ b/.devcontainer/devcontainer.json @@ -7,12 +7,13 @@ "workspaceFolder": "/workspace", "workspaceMount": "source=${localWorkspaceFolder},target=/workspace,type=bind", "mounts": [ - "source=claude-code-config-${devcontainerId},target=/home/node/.claude,type=volume" + "source=claude-code-config-${devcontainerId},target=/home/node/.claude,type=volume", + "source=komet-ssh-${devcontainerId},target=/home/node/.ssh,type=volume" ], "containerEnv": { "CLAUDE_CONFIG_DIR": "/home/node/.claude" }, - "postCreateCommand": "sudo chown -R node:node /home/node/.claude", + "postCreateCommand": "sudo chown -R node:node /home/node/.claude /home/node/.ssh && chmod 700 /home/node/.ssh", "customizations": { "vscode": { "extensions": [ diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 1d980a4..f97874d 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -31,6 +31,28 @@ Then: npm install ``` +### SSH keys in the devcontainer + +`~/.ssh` is a named Docker volume, so keys **persist across container rebuilds** +— but the volume starts **empty** on first build, so add a key once. The volume +lives outside `/workspace`, so keys can't be committed to the repo, and Docker +excludes volumes from `docker commit` / image builds. (Anyone with root or +`docker`-group access on the host can still read the volume, so prefer a +passphrase or a dedicated, revocable key.) + +Inside the container, generate a key: + +```bash +ssh-keygen -t ed25519 -C "you@example.com" # writes ~/.ssh/id_ed25519[.pub] +chmod 700 ~/.ssh +chmod 600 ~/.ssh/id_ed25519 +chmod 644 ~/.ssh/id_ed25519.pub +``` + +Then add the **public** key (`~/.ssh/id_ed25519.pub`) to your GitHub account at +. To reuse an existing host key instead, +`docker cp` it into the container's `~/.ssh` and apply the same `chmod`. + ## Everyday commands ```bash