From 35b294694c3b5c6058944917ba6c9859d40cec8b Mon Sep 17 00:00:00 2001 From: Raoul Date: Fri, 24 Jul 2026 09:37:38 +0000 Subject: [PATCH 1/5] init From 3ef76aab470710c0909f098ea2afa820527fb3d5 Mon Sep 17 00:00:00 2001 From: Raoul Date: Fri, 24 Jul 2026 10:21:48 +0000 Subject: [PATCH 2/5] Add manual deployment script as single source of truth CI is unavailable, so releases must be deployed by hand. Add scripts/deploy.sh, which reproduces the Release workflow's deployment steps, and have the workflow call it so the two never drift. scripts/deploy.sh: - nix-cache: build komet-node once, push the closure to the k-framework cache (cachix), publish the binary to k-framework-binary (kup), and verify the push and pin. - docker: build the image, smoke-test it, push to Docker Hub; logs out on exit so credentials do not linger. - Preflight guards: required tools on PATH, a clean worktree (so a manual build matches the published REV), and required secrets. scripts/README.md: manual-deployment runbook. release.yml: the nix-cache and dockerhub jobs now invoke the script instead of duplicating the commands inline. .dockerignore: exclude local secret/credential files so a manual `docker build .` cannot bake them into a published image layer. .devcontainer: install cachix and add the docker-in-docker feature so both subcommands run inside the container. --- .devcontainer/Dockerfile | 7 +- .devcontainer/devcontainer-lock.json | 9 ++ .devcontainer/devcontainer.json | 7 ++ .dockerignore | 13 ++ .github/scripts/check-cachix-pin.sh | 2 +- .github/workflows/release.yml | 56 ++------- scripts/README.md | 84 +++++++++++++ scripts/deploy.sh | 181 +++++++++++++++++++++++++++ 8 files changed, 308 insertions(+), 51 deletions(-) create mode 100644 .devcontainer/devcontainer-lock.json create mode 100644 scripts/README.md create mode 100755 scripts/deploy.sh diff --git a/.devcontainer/Dockerfile b/.devcontainer/Dockerfile index a3fe744..8a2adff 100644 --- a/.devcontainer/Dockerfile +++ b/.devcontainer/Dockerfile @@ -59,13 +59,18 @@ ENV PATH=/home/vscode/.nix-profile/bin:/home/vscode/.npm-global/bin:$PATH # - gh → GitHub CLI for PRs/issues/auth; global so it's usable # from anywhere. Auth is persisted across rebuilds via a # named volume on ~/.config/gh (see devcontainer.json). +# - cachix → required by scripts/deploy.sh `nix-cache` to push the +# build closure to the k-framework cache. kup (the other +# half of that deploy step) is fetched via nix at run +# time, so only cachix needs provisioning here. RUN . /home/vscode/.nix-profile/etc/profile.d/nix.sh \ && nix registry add nixpkgs github:NixOS/nixpkgs/nixos-25.05 \ && nix profile install \ nixpkgs#direnv \ nixpkgs#nix-direnv \ nixpkgs#nodejs_22 \ - nixpkgs#gh + nixpkgs#gh \ + nixpkgs#cachix # Claude Code CLI — installed to a per-user prefix so root isn't required. RUN . /home/vscode/.nix-profile/etc/profile.d/nix.sh \ diff --git a/.devcontainer/devcontainer-lock.json b/.devcontainer/devcontainer-lock.json new file mode 100644 index 0000000..5c99099 --- /dev/null +++ b/.devcontainer/devcontainer-lock.json @@ -0,0 +1,9 @@ +{ + "features": { + "ghcr.io/devcontainers/features/docker-in-docker:2": { + "version": "2.17.0", + "resolved": "ghcr.io/devcontainers/features/docker-in-docker@sha256:25b9f05705ffba7dbe503230ac76081419306f8c8bc88e0ce78c4ecd99a0c78c", + "integrity": "sha256:25b9f05705ffba7dbe503230ac76081419306f8c8bc88e0ce78c4ecd99a0c78c" + } + } +} diff --git a/.devcontainer/devcontainer.json b/.devcontainer/devcontainer.json index 8dd1c06..3605b7e 100644 --- a/.devcontainer/devcontainer.json +++ b/.devcontainer/devcontainer.json @@ -3,6 +3,13 @@ "build": { "dockerfile": "Dockerfile" }, + // An isolated Docker daemon inside the container, so `scripts/deploy.sh docker` + // can build and push the release image without touching the host's Docker. The + // feature adds the docker CLI, runs dockerd, and puts `vscode` in the docker + // group; it also marks the container privileged, which dockerd requires. + "features": { + "ghcr.io/devcontainers/features/docker-in-docker:2": {} + }, "remoteUser": "vscode", "workspaceFolder": "/workspace", "workspaceMount": "source=${localWorkspaceFolder},target=/workspace,type=bind", diff --git a/.dockerignore b/.dockerignore index 4ab3cf6..e027727 100644 --- a/.dockerignore +++ b/.dockerignore @@ -15,3 +15,16 @@ cov-* result result-* state.kore + +# Never ship local secrets. The build context is the whole repo, and the +# Dockerfile does `COPY . komet-node`, so any credential file sitting here +# would be baked into a published image layer (a later `rm` does not remove +# it from history). deploy.sh is run by hand with tokens exported, often via a +# direnv `.envrc` or a `.env`, so keep those and any key/token files out. +.envrc +.env +.env.* +*.pem +*.key +*.token +secrets* diff --git a/.github/scripts/check-cachix-pin.sh b/.github/scripts/check-cachix-pin.sh index 936c66e..48d73d8 100755 --- a/.github/scripts/check-cachix-pin.sh +++ b/.github/scripts/check-cachix-pin.sh @@ -2,7 +2,7 @@ set -euo pipefail # Verifies that `kup publish` actually pushed AND pinned komet-node in the -# private k-framework-binary cache. Cachix has intermittently dropped the +# k-framework-binary cache. Cachix has intermittently dropped the # `cachix pin` requests kup makes under the hood, so we confirm both the pin # (visible via the pin API) and the narinfo (the pushed store path) before # treating the publish as successful. diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index 62759bd..9f0c48c 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -40,38 +40,16 @@ jobs: ref: ${{ github.sha }} fetch-depth: 0 - # Build the komet-node derivation once, then push it to both the public - # k-framework cache (full build closure, via `cachix push`) and the - # private k-framework-binary cache (the kup-installable binary, via - # `kup publish`). Both pushes reuse the build output already present in - # this runner's Nix store, so the derivation is never built twice. + # The build-and-publish logic lives in scripts/deploy.sh so CI and manual + # deployments stay in sync (single source of truth). See scripts/README.md. - name: 'Build and publish komet-node to both Nix caches' shell: bash env: - GC_DONT_GC: '1' - # Enable flakes for every nix invocation in this step (the initial - # build, the kup build, and the builds kup runs internally) so the - # job does not depend on flakes being globally enabled on the runner. - NIX_CONFIG: 'extra-experimental-features = nix-command flakes' CACHIX_PUBLIC_TOKEN: '${{ secrets.CACHIX_PUBLIC_TOKEN }}' CACHIX_PRIVATE_KFB_TOKEN: '${{ secrets.CACHIX_PRIVATE_KFB_TOKEN }}' OWNER_REPO: '${{ github.repository }}' REV: '${{ github.sha }}' - run: | - KOMET_NODE=$(nix build .#komet-node --no-link --print-out-paths) - DRV=$(nix-store --query --deriver "${KOMET_NODE}") - - # Push the full build closure to the public k-framework cache. - export CACHIX_AUTH_TOKEN="${CACHIX_PUBLIC_TOKEN}" - nix-store --query --requisites --include-outputs "${DRV}" | cachix push k-framework - - # Publish the binary to the private k-framework-binary cache. kup - # reuses the store paths built above. - export CACHIX_AUTH_TOKEN="${CACHIX_PRIVATE_KFB_TOKEN}" - export PATH="$(nix build github:runtimeverification/kup --no-link --print-out-paths)/bin:$PATH" - kup publish k-framework-binary .#komet-node --keep-days 180 - # Cachix has not been responding to 'cachix pin' requests made under the hood by kup. Verify the push and pin manually. - bash .github/scripts/check-cachix-pin.sh + run: ./scripts/deploy.sh nix-cache - name: 'On failure, delete drafted release' if: failure() @@ -96,32 +74,12 @@ jobs: ref: ${{ github.sha }} fetch-depth: 0 - - name: 'Set environment' - run: | - KOMET_NODE_VERSION=$(cat package/version) - TAG=runtimeverificationinc/komet-node:ubuntu-jammy-${KOMET_NODE_VERSION} - echo "TAG=${TAG}" >> ${GITHUB_ENV} - - - name: 'Build Docker image' - run: | - K_VERSION=$(cat deps/k_release) - docker build . --no-cache --tag ${TAG} --build-arg K_VERSION=${K_VERSION} - - - name: 'Run Docker image' - run: docker run --rm ${TAG} komet-node --help - - - name: 'Push Docker image to Docker Hub' + # Build, smoke-test, and push logic lives in scripts/deploy.sh so CI and + # manual deployments stay in sync (single source of truth). See scripts/README.md. + - name: 'Build, test, and push Docker image to Docker Hub' env: - DOCKERHUB_USERNAME: rvdockerhub DOCKERHUB_PASSWORD: ${{ secrets.DOCKERHUB_PASSWORD }} - DOCKERHUB_NAMESPACE: runtimeverificationinc - DOCKERHUB_REPO: komet-node - run: | - # Log in to Docker Hub - echo "${DOCKERHUB_PASSWORD}" | docker login --username "${DOCKERHUB_USERNAME}" --password-stdin - - # Push the image - docker image push ${TAG} + run: ./scripts/deploy.sh docker - name: 'On failure, delete drafted release' if: failure() diff --git a/scripts/README.md b/scripts/README.md new file mode 100644 index 0000000..8365af6 --- /dev/null +++ b/scripts/README.md @@ -0,0 +1,84 @@ +# Deployment scripts + +`deploy.sh` builds and publishes the komet-node release artifacts. It is the +single source of truth for the deployment steps: the `Release` workflow +(`.github/workflows/release.yml`) invokes its subcommands, and you run the same +subcommands by hand when CI is unavailable. + +## What it does + +The script has three subcommands: + +| Subcommand | Action | +| ----------- | ------ | +| `nix-cache` | Builds `.#komet-node`, pushes the full build closure to the `k-framework` Cachix cache, publishes the kup-installable binary to the `k-framework-binary` cache, then verifies the push and pin. Both caches are public; `binary` is a historical name, not an access level. | +| `docker` | Builds the runtime image from `Dockerfile`, runs `komet-node --help` in it as a smoke test, then pushes it to Docker Hub. | +| `all` | Runs `nix-cache` then `docker`. | + +The image tag is `runtimeverificationinc/komet-node:ubuntu-jammy-`, +where `` comes from `package/version`. + +## Prerequisites + +Both subcommands run from a checkout of the revision you are releasing, with the +following tools on `PATH`: + +- `nix-cache` needs `nix` and `cachix`. It fetches `kup` from + `github:runtimeverification/kup` itself, so you do not install kup separately. +- `docker` needs `docker`. + +Each subcommand checks its tools up front and exits with a clear message if one +is missing, before starting the build. + +The project devcontainer (`.devcontainer/`) provides all of these: `nix` and +`cachix` are installed into the Nix profile, and the docker-in-docker feature +supplies `docker`. If you added these to an existing container, rebuild it +("Dev Containers: Rebuild Container") so the new tools are present. + +Provide the secrets as environment variables. Everything else has a default (see +the `Shared configuration` block in `deploy.sh`), so a normal checkout needs no +further setup. + +| Subcommand | Required environment variables | +| ----------- | ------------------------------ | +| `nix-cache` | `CACHIX_PUBLIC_TOKEN`, `CACHIX_PRIVATE_KFB_TOKEN` | +| `docker` | `DOCKERHUB_PASSWORD` | + +`OWNER_REPO` and `REV` default to the current checkout's `origin` remote and +`HEAD`. Override them if you are publishing a revision other than the one checked +out. `DOCKERHUB_USERNAME`, `DOCKERHUB_NAMESPACE`, and `DOCKERHUB_REPO` default to +the release account and repository; override them only to publish elsewhere. + +Both subcommands refuse to run if the working tree is not clean. CI builds from a +fresh checkout, so a manual build must too: uncommitted changes and untracked +files would otherwise be baked into the published image or flake build without +matching the `REV` they are published under. Commit, stash, or clean the tree +first. `git status --porcelain` ignores `.gitignore`d paths, so runtime artifacts +and dev caches do not count. Set `ALLOW_DIRTY=1` to override the check when you +deliberately want to publish an uncommitted state. + +## Manual release while CI is down + +The workflow also drafts, cleans up, and finalizes the GitHub release around the +deployment jobs. When you deploy by hand, run those `gh` steps yourself in this +order. `nix-cache` runs once per architecture (the workflow uses an `x86_64` and +an `ARM64` runner), so run it on a machine of each architecture that should be +cached. + +```sh +VERSION=v$(cat package/version) + +# 1. Draft the release. +gh release create "$VERSION" --draft --title "$VERSION" --target "$(git rev-parse HEAD)" + +# 2. Deploy. Export the secrets first (see the table above). +# Run nix-cache once per architecture; docker once. +./scripts/deploy.sh nix-cache +./scripts/deploy.sh docker + +# 3. Finalize the release once every deployment has succeeded. +gh release edit "$VERSION" --draft=false + +# If a deployment fails, remove the draft instead: +# gh release delete "$VERSION" --yes --cleanup-tag +``` diff --git a/scripts/deploy.sh b/scripts/deploy.sh new file mode 100755 index 0000000..5ee4055 --- /dev/null +++ b/scripts/deploy.sh @@ -0,0 +1,181 @@ +#!/usr/bin/env bash +set -euo pipefail + +# NOTE: do not run this script under `set -x` / `bash -x`: the cachix and Docker +# Hub tokens flow through the environment and the `docker login` pipe, and shell +# tracing would print them to the logs. + +# deploy.sh -- build and publish komet-node release artifacts. +# +# This is the single source of truth for the deployment steps that the Release +# workflow (.github/workflows/release.yml) performs. The workflow calls the +# subcommands below, and you can run the exact same steps by hand when CI is +# unavailable. See scripts/README.md for the full manual-deployment runbook. +# +# Subcommands: +# nix-cache Build komet-node and push it to both Nix caches (the +# k-framework closure + the k-framework-binary kup binary). +# docker Build the Docker image, smoke-test it, and push to Docker Hub. +# all Run nix-cache then docker. +# +# Usage: +# scripts/deploy.sh + +REPO_ROOT="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)" +cd "${REPO_ROOT}" + +# --- Shared configuration -------------------------------------------------- +# Defaults live here (not in the workflow) so the manual and CI paths stay +# identical. Anything already set in the environment wins, which lets the +# workflow inject secrets and lets a developer override values locally. + +# Keep the Nix daemon from garbage-collecting store paths mid-build, and enable +# flakes for every nix invocation (the build, the kup build, and the builds kup +# runs internally) so we do not depend on flakes being globally enabled. +export GC_DONT_GC="${GC_DONT_GC:-1}" +export NIX_CONFIG="${NIX_CONFIG:-extra-experimental-features = nix-command flakes}" + +# owner/repo and revision, used by kup publish + the cachix pin check. Default +# to the current checkout so manual runs work without extra setup. The first +# sed clause strips any `user:token@` userinfo from an https remote before +# parsing, so a credential embedded in the remote URL never ends up in +# OWNER_REPO (which is later echoed into the deploy log by check-cachix-pin.sh). +OWNER_REPO="${OWNER_REPO:-$(git remote get-url origin | sed -E 's#^[a-z]+://[^@/]*@#https://#; s#(git@github.com:|https://github.com/)##; s#\.git$##')}" +REV="${REV:-$(git rev-parse HEAD)}" +export OWNER_REPO REV + +# Docker Hub coordinates. Only DOCKERHUB_PASSWORD is a secret. +DOCKERHUB_USERNAME="${DOCKERHUB_USERNAME:-rvdockerhub}" +DOCKERHUB_NAMESPACE="${DOCKERHUB_NAMESPACE:-runtimeverificationinc}" +DOCKERHUB_REPO="${DOCKERHUB_REPO:-komet-node}" + +KOMET_NODE_VERSION="$(cat package/version)" + +# Fail early with a clear message if a required secret is missing. +require_env() { + local missing=0 var + for var in "$@"; do + if [ -z "${!var:-}" ]; then + echo "error: required environment variable '${var}' is not set" >&2 + missing=1 + fi + done + [ "${missing}" -eq 0 ] || exit 1 +} + +# Fail before the (long) build if a required tool is not on PATH, so a missing +# dependency surfaces immediately rather than after minutes of building. kup is +# not checked here: nix-cache fetches it via `nix build` at run time. +require_cmd() { + local missing=0 cmd + for cmd in "$@"; do + if ! command -v "${cmd}" >/dev/null 2>&1; then + echo "error: required command '${cmd}' not found on PATH" >&2 + missing=1 + fi + done + [ "${missing}" -eq 0 ] || exit 1 +} + +# CI always builds from a fresh checkout at a known revision. A manual run +# builds from your working tree, so uncommitted changes to tracked files (which +# a dirty flake build embeds) and untracked files (which `docker build .` copies +# into the image) would silently end up in the published artifacts -- and would +# not match the REV they are published under. Require a clean tree so a manual +# deploy is byte-for-byte what CI would produce. `git status --porcelain` skips +# .gitignored paths, so runtime artifacts and dev caches do not trip this. +require_clean_worktree() { + [ -n "${ALLOW_DIRTY:-}" ] && return 0 + if [ -n "$(git status --porcelain)" ]; then + echo "error: working tree is not clean." >&2 + echo "CI deploys from a fresh checkout; these changes would be baked into the" >&2 + echo "published artifacts but would not match REV (${REV}):" >&2 + git status --short >&2 + echo "Commit, stash, or clean them -- or set ALLOW_DIRTY=1 to override." >&2 + exit 1 + fi +} + +# --- nix-cache ------------------------------------------------------------- +# Build the komet-node derivation once, then push it to both Nix caches: the +# k-framework cache (full build closure, via `cachix push`) and the +# k-framework-binary cache (the kup-installable binary, via `kup publish`). +# Both caches are public; "binary" is a historical name, not an access level. +# Both pushes reuse the build output already present in this machine's Nix +# store, so the derivation is never built twice. +deploy_nix_cache() { + require_cmd nix nix-store cachix git curl jq + require_clean_worktree + require_env CACHIX_PUBLIC_TOKEN CACHIX_PRIVATE_KFB_TOKEN + + local komet_node drv + komet_node="$(nix build .#komet-node --no-link --print-out-paths)" + drv="$(nix-store --query --deriver "${komet_node}")" + + # Push the full build closure to the public k-framework cache. + echo ":: pushing build closure to the public k-framework cache" + export CACHIX_AUTH_TOKEN="${CACHIX_PUBLIC_TOKEN}" + nix-store --query --requisites --include-outputs "${drv}" | cachix push k-framework + + # Publish the binary to the k-framework-binary cache. kup reuses the + # store paths built above. + echo ":: publishing komet-node binary to the k-framework-binary cache" + export CACHIX_AUTH_TOKEN="${CACHIX_PRIVATE_KFB_TOKEN}" + export PATH="$(nix build github:runtimeverification/kup --no-link --print-out-paths)/bin:${PATH}" + kup publish k-framework-binary .#komet-node --keep-days 180 + + # Cachix has not been reliably honoring the `cachix pin` requests kup makes + # under the hood. Verify the push and pin explicitly. + bash .github/scripts/check-cachix-pin.sh +} + +# --- docker ---------------------------------------------------------------- +# Build the runtime image, smoke-test it, then push it to Docker Hub. +deploy_docker() { + require_cmd docker git + require_clean_worktree + require_env DOCKERHUB_PASSWORD + + local tag k_version + tag="${DOCKERHUB_NAMESPACE}/${DOCKERHUB_REPO}:ubuntu-jammy-${KOMET_NODE_VERSION}" + k_version="$(cat deps/k_release)" + + echo ":: building Docker image ${tag} (K ${k_version})" + docker build . --no-cache --tag "${tag}" --build-arg K_VERSION="${k_version}" + + echo ":: smoke-testing the image" + docker run --rm "${tag}" komet-node --help + + echo ":: pushing ${tag} to Docker Hub" + # Log out on the way out (success or failure) so the base64 credential + # `docker login` writes to ~/.docker/config.json does not linger on the + # self-hosted runner or on the operator's machine. EXIT (not RETURN) so it + # still fires when `set -e` aborts on a failed login or push. + trap 'docker logout >/dev/null 2>&1 || true' EXIT + echo "${DOCKERHUB_PASSWORD}" | docker login --username "${DOCKERHUB_USERNAME}" --password-stdin + docker image push "${tag}" +} + +usage() { + sed -n '8,22p' "${BASH_SOURCE[0]}" | sed 's/^# \{0,1\}//' +} + +main() { + case "${1:-}" in + nix-cache) deploy_nix_cache ;; + docker) deploy_docker ;; + all) deploy_nix_cache; deploy_docker ;; + -h | --help | help | "") + usage + [ -n "${1:-}" ] # exit non-zero when no subcommand was given + ;; + *) + echo "error: unknown subcommand '${1}'" >&2 + echo >&2 + usage >&2 + exit 1 + ;; + esac +} + +main "$@" From 3a43bbe6b4d51dc4eafc60e704141892cf05b237 Mon Sep 17 00:00:00 2001 From: Raoul Date: Fri, 24 Jul 2026 10:30:38 +0000 Subject: [PATCH 3/5] Move deployment docs into CONTRIBUTOR.md Fold the manual-deployment runbook into CONTRIBUTOR.md ("Deploying a release") and drop scripts/README.md so the contributor guide is the single home for it. Repoint the references in deploy.sh and release.yml. --- .github/workflows/release.yml | 4 +- CONTRIBUTOR.md | 85 +++++++++++++++++++++++++++++++++++ scripts/README.md | 84 ---------------------------------- scripts/deploy.sh | 2 +- 4 files changed, 88 insertions(+), 87 deletions(-) delete mode 100644 scripts/README.md diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index 9f0c48c..f816e50 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -41,7 +41,7 @@ jobs: fetch-depth: 0 # The build-and-publish logic lives in scripts/deploy.sh so CI and manual - # deployments stay in sync (single source of truth). See scripts/README.md. + # deployments stay in sync (single source of truth). See CONTRIBUTOR.md. - name: 'Build and publish komet-node to both Nix caches' shell: bash env: @@ -75,7 +75,7 @@ jobs: fetch-depth: 0 # Build, smoke-test, and push logic lives in scripts/deploy.sh so CI and - # manual deployments stay in sync (single source of truth). See scripts/README.md. + # manual deployments stay in sync (single source of truth). See CONTRIBUTOR.md. - name: 'Build, test, and push Docker image to Docker Hub' env: DOCKERHUB_PASSWORD: ${{ secrets.DOCKERHUB_PASSWORD }} diff --git a/CONTRIBUTOR.md b/CONTRIBUTOR.md index ce4d40f..5976a91 100644 --- a/CONTRIBUTOR.md +++ b/CONTRIBUTOR.md @@ -56,3 +56,88 @@ your GitHub account. > Never place an SSH key registered as an **Authentication key** in the container. > An authentication key grants full account-wide git access and would bypass the > minimal permissions of your fine-grained PAT. Use a **signing-only** key here. + +## Deploying a release + +`scripts/deploy.sh` builds and publishes the komet-node release artifacts. It is +the single source of truth for the deployment steps: the `Release` workflow +(`.github/workflows/release.yml`) invokes its subcommands, and you run the same +subcommands by hand when CI is unavailable. + +### What it does + +The script has three subcommands: + +| Subcommand | Action | +| ----------- | ------ | +| `nix-cache` | Builds `.#komet-node`, pushes the full build closure to the `k-framework` Cachix cache, publishes the kup-installable binary to the `k-framework-binary` cache, then verifies the push and pin. Both caches are public; `binary` is a historical name, not an access level. | +| `docker` | Builds the runtime image from `Dockerfile`, runs `komet-node --help` in it as a smoke test, then pushes it to Docker Hub. | +| `all` | Runs `nix-cache` then `docker`. | + +The image tag is `runtimeverificationinc/komet-node:ubuntu-jammy-`, +where `` comes from `package/version`. + +### Prerequisites + +Both subcommands run from a checkout of the revision you are releasing, with the +following tools on `PATH`: + +- `nix-cache` needs `nix` and `cachix`. It fetches `kup` from + `github:runtimeverification/kup` itself, so you do not install kup separately. +- `docker` needs `docker`. + +Each subcommand checks its tools up front and exits with a clear message if one +is missing, before starting the build. + +The devcontainer provides all of these: `nix` and `cachix` are installed into the +Nix profile, and the docker-in-docker feature supplies `docker`. If you added +these to an existing container, rebuild it ("Dev Containers: Rebuild Container") +so the new tools are present. + +Provide the secrets as environment variables. Everything else has a default (see +the `Shared configuration` block in `deploy.sh`), so a normal checkout needs no +further setup. + +| Subcommand | Required environment variables | +| ----------- | ------------------------------ | +| `nix-cache` | `CACHIX_PUBLIC_TOKEN`, `CACHIX_PRIVATE_KFB_TOKEN` | +| `docker` | `DOCKERHUB_PASSWORD` | + +`OWNER_REPO` and `REV` default to the current checkout's `origin` remote and +`HEAD`. Override them if you are publishing a revision other than the one checked +out. `DOCKERHUB_USERNAME`, `DOCKERHUB_NAMESPACE`, and `DOCKERHUB_REPO` default to +the release account and repository; override them only to publish elsewhere. + +Both subcommands refuse to run if the working tree is not clean. CI builds from a +fresh checkout, so a manual build must too: uncommitted changes and untracked +files would otherwise be baked into the published image or flake build without +matching the `REV` they are published under. Commit, stash, or clean the tree +first. `git status --porcelain` ignores `.gitignore`d paths, so runtime artifacts +and dev caches do not count. Set `ALLOW_DIRTY=1` to override the check when you +deliberately want to publish an uncommitted state. + +### Manual release while CI is down + +The workflow also drafts, cleans up, and finalizes the GitHub release around the +deployment jobs. When you deploy by hand, run those `gh` steps yourself in this +order. `nix-cache` runs once per architecture (the workflow uses an `x86_64` and +an `ARM64` runner), so run it on a machine of each architecture that should be +cached. + +```sh +VERSION=v$(cat package/version) + +# 1. Draft the release. +gh release create "$VERSION" --draft --title "$VERSION" --target "$(git rev-parse HEAD)" + +# 2. Deploy. Export the secrets first (see the table above). +# Run nix-cache once per architecture; docker once. +./scripts/deploy.sh nix-cache +./scripts/deploy.sh docker + +# 3. Finalize the release once every deployment has succeeded. +gh release edit "$VERSION" --draft=false + +# If a deployment fails, remove the draft instead: +# gh release delete "$VERSION" --yes --cleanup-tag +``` diff --git a/scripts/README.md b/scripts/README.md deleted file mode 100644 index 8365af6..0000000 --- a/scripts/README.md +++ /dev/null @@ -1,84 +0,0 @@ -# Deployment scripts - -`deploy.sh` builds and publishes the komet-node release artifacts. It is the -single source of truth for the deployment steps: the `Release` workflow -(`.github/workflows/release.yml`) invokes its subcommands, and you run the same -subcommands by hand when CI is unavailable. - -## What it does - -The script has three subcommands: - -| Subcommand | Action | -| ----------- | ------ | -| `nix-cache` | Builds `.#komet-node`, pushes the full build closure to the `k-framework` Cachix cache, publishes the kup-installable binary to the `k-framework-binary` cache, then verifies the push and pin. Both caches are public; `binary` is a historical name, not an access level. | -| `docker` | Builds the runtime image from `Dockerfile`, runs `komet-node --help` in it as a smoke test, then pushes it to Docker Hub. | -| `all` | Runs `nix-cache` then `docker`. | - -The image tag is `runtimeverificationinc/komet-node:ubuntu-jammy-`, -where `` comes from `package/version`. - -## Prerequisites - -Both subcommands run from a checkout of the revision you are releasing, with the -following tools on `PATH`: - -- `nix-cache` needs `nix` and `cachix`. It fetches `kup` from - `github:runtimeverification/kup` itself, so you do not install kup separately. -- `docker` needs `docker`. - -Each subcommand checks its tools up front and exits with a clear message if one -is missing, before starting the build. - -The project devcontainer (`.devcontainer/`) provides all of these: `nix` and -`cachix` are installed into the Nix profile, and the docker-in-docker feature -supplies `docker`. If you added these to an existing container, rebuild it -("Dev Containers: Rebuild Container") so the new tools are present. - -Provide the secrets as environment variables. Everything else has a default (see -the `Shared configuration` block in `deploy.sh`), so a normal checkout needs no -further setup. - -| Subcommand | Required environment variables | -| ----------- | ------------------------------ | -| `nix-cache` | `CACHIX_PUBLIC_TOKEN`, `CACHIX_PRIVATE_KFB_TOKEN` | -| `docker` | `DOCKERHUB_PASSWORD` | - -`OWNER_REPO` and `REV` default to the current checkout's `origin` remote and -`HEAD`. Override them if you are publishing a revision other than the one checked -out. `DOCKERHUB_USERNAME`, `DOCKERHUB_NAMESPACE`, and `DOCKERHUB_REPO` default to -the release account and repository; override them only to publish elsewhere. - -Both subcommands refuse to run if the working tree is not clean. CI builds from a -fresh checkout, so a manual build must too: uncommitted changes and untracked -files would otherwise be baked into the published image or flake build without -matching the `REV` they are published under. Commit, stash, or clean the tree -first. `git status --porcelain` ignores `.gitignore`d paths, so runtime artifacts -and dev caches do not count. Set `ALLOW_DIRTY=1` to override the check when you -deliberately want to publish an uncommitted state. - -## Manual release while CI is down - -The workflow also drafts, cleans up, and finalizes the GitHub release around the -deployment jobs. When you deploy by hand, run those `gh` steps yourself in this -order. `nix-cache` runs once per architecture (the workflow uses an `x86_64` and -an `ARM64` runner), so run it on a machine of each architecture that should be -cached. - -```sh -VERSION=v$(cat package/version) - -# 1. Draft the release. -gh release create "$VERSION" --draft --title "$VERSION" --target "$(git rev-parse HEAD)" - -# 2. Deploy. Export the secrets first (see the table above). -# Run nix-cache once per architecture; docker once. -./scripts/deploy.sh nix-cache -./scripts/deploy.sh docker - -# 3. Finalize the release once every deployment has succeeded. -gh release edit "$VERSION" --draft=false - -# If a deployment fails, remove the draft instead: -# gh release delete "$VERSION" --yes --cleanup-tag -``` diff --git a/scripts/deploy.sh b/scripts/deploy.sh index 5ee4055..128d83e 100755 --- a/scripts/deploy.sh +++ b/scripts/deploy.sh @@ -10,7 +10,7 @@ set -euo pipefail # This is the single source of truth for the deployment steps that the Release # workflow (.github/workflows/release.yml) performs. The workflow calls the # subcommands below, and you can run the exact same steps by hand when CI is -# unavailable. See scripts/README.md for the full manual-deployment runbook. +# unavailable. See CONTRIBUTOR.md ("Deploying a release") for the runbook. # # Subcommands: # nix-cache Build komet-node and push it to both Nix caches (the From 0e15a1be0c8fbbb05cd0035c37c9d5e690833cbd Mon Sep 17 00:00:00 2001 From: Raoul Date: Fri, 24 Jul 2026 10:33:43 +0000 Subject: [PATCH 4/5] Rename CONTRIBUTOR.md to CONTRIBUTING.md Use the conventional name so GitHub auto-links it in the PR and issue UI. Update the references in deploy.sh and release.yml. --- .github/workflows/release.yml | 4 ++-- CONTRIBUTOR.md => CONTRIBUTING.md | 0 scripts/deploy.sh | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) rename CONTRIBUTOR.md => CONTRIBUTING.md (100%) diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index f816e50..7860a35 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -41,7 +41,7 @@ jobs: fetch-depth: 0 # The build-and-publish logic lives in scripts/deploy.sh so CI and manual - # deployments stay in sync (single source of truth). See CONTRIBUTOR.md. + # deployments stay in sync (single source of truth). See CONTRIBUTING.md. - name: 'Build and publish komet-node to both Nix caches' shell: bash env: @@ -75,7 +75,7 @@ jobs: fetch-depth: 0 # Build, smoke-test, and push logic lives in scripts/deploy.sh so CI and - # manual deployments stay in sync (single source of truth). See CONTRIBUTOR.md. + # manual deployments stay in sync (single source of truth). See CONTRIBUTING.md. - name: 'Build, test, and push Docker image to Docker Hub' env: DOCKERHUB_PASSWORD: ${{ secrets.DOCKERHUB_PASSWORD }} diff --git a/CONTRIBUTOR.md b/CONTRIBUTING.md similarity index 100% rename from CONTRIBUTOR.md rename to CONTRIBUTING.md diff --git a/scripts/deploy.sh b/scripts/deploy.sh index 128d83e..2e3bcd5 100755 --- a/scripts/deploy.sh +++ b/scripts/deploy.sh @@ -10,7 +10,7 @@ set -euo pipefail # This is the single source of truth for the deployment steps that the Release # workflow (.github/workflows/release.yml) performs. The workflow calls the # subcommands below, and you can run the exact same steps by hand when CI is -# unavailable. See CONTRIBUTOR.md ("Deploying a release") for the runbook. +# unavailable. See CONTRIBUTING.md ("Deploying a release") for the runbook. # # Subcommands: # nix-cache Build komet-node and push it to both Nix caches (the From 0ff68a21e05bf7a96808e74d2fd31c2e46980f40 Mon Sep 17 00:00:00 2001 From: Raoul Date: Fri, 24 Jul 2026 10:37:57 +0000 Subject: [PATCH 5/5] Ignore .env files --- .gitignore | 1 + 1 file changed, 1 insertion(+) diff --git a/.gitignore b/.gitignore index 6caff64..2a43feb 100644 --- a/.gitignore +++ b/.gitignore @@ -2,6 +2,7 @@ __pycache__/ .coverage .direnv/ +.env # Runtime artifacts written by the server / interpreter in the io dir metadata.json