Merge pull request #49 from runtimeverification/add-deploy-script

Add manual deployment script as single source of truth

Author: RaoulSchaffranek

.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 \

.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"
+    }
+  }
+}

.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",

.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*

.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.

.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 CONTRIBUTING.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 CONTRIBUTING.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()

.gitignore

@@ -2,6 +2,7 @@
 __pycache__/
 .coverage
 .direnv/
+.env
 
 # Runtime artifacts written by the server / interpreter in the io dir
 metadata.json

CONTRIBUTING.md

@@ -0,0 +1,143 @@
+# Contributing to Komet Node
+
+## Development environment
+
+This repository ships a [devcontainer](.devcontainer/) that provisions the full
+toolchain (Nix, the flake's `nix develop` shell, the Claude Code CLI, and the
+GitHub CLI). Open the repo in a devcontainer-aware editor and everything below is
+available out of the box.
+
+## Using the GitHub CLI (`gh`)
+
+`gh` is preinstalled in the devcontainer for creating pull requests, reviewing
+issues, and other GitHub tasks from the terminal.
+
+### Authenticating
+
+Authenticate once with a personal access token:
+
+```bash
+gh auth login
+```
+
+Choose **GitHub.com** → **HTTPS** → **Paste an authentication token** when
+prompted, then paste the token you create below.
+
+Your credentials are stored in `~/.config/gh` inside the container, which is
+backed by a named volume. This means **your token survives container rebuilds** —
+you only need to authenticate once, not every time the container is recreated.
+
+To check or reset your authentication at any time:
+
+```bash
+gh auth status   # show the current login
+gh auth logout   # remove stored credentials
+```
+
+### Creating a token with minimal permissions
+
+Create a **fine-grained** personal access token at **GitHub → Settings → Developer
+settings → [Fine-grained personal access tokens](https://github.com/settings/personal-access-tokens/new)**
+with the least privilege for your work:
+
+- **Repository access** → *Only select repositories* → `runtimeverification/komet-node`
+- **Contents** → *Read and write*
+- **Pull requests** → *Read and write*
+- **Issues** → *Read and write* (only if you triage issues)
+
+`Metadata → Read` is selected automatically; leave everything else at *No access*.
+
+## Signing commits
+
+To sign commits made with `git`, add an SSH or GPG key of type **Signing key** to
+your GitHub account.
+
+> [!WARNING]
+> 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-<version>`,
+where `<version>` 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
+```