Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 6 additions & 1 deletion .devcontainer/Dockerfile
Original file line number Diff line number Diff line change
Expand Up @@ -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 \
Expand Down
9 changes: 9 additions & 0 deletions .devcontainer/devcontainer-lock.json
Original file line number Diff line number Diff line change
@@ -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"
}
}
}
7 changes: 7 additions & 0 deletions .devcontainer/devcontainer.json
Original file line number Diff line number Diff line change
Expand Up @@ -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",
Expand Down
13 changes: 13 additions & 0 deletions .dockerignore
Original file line number Diff line number Diff line change
Expand Up @@ -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*
2 changes: 1 addition & 1 deletion .github/scripts/check-cachix-pin.sh
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
56 changes: 7 additions & 49 deletions .github/workflows/release.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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()
Expand All @@ -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()
Expand Down
1 change: 1 addition & 0 deletions .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@
__pycache__/
.coverage
.direnv/
.env

# Runtime artifacts written by the server / interpreter in the io dir
metadata.json
Expand Down
143 changes: 143 additions & 0 deletions CONTRIBUTING.md
Original file line number Diff line number Diff line change
@@ -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
```
58 changes: 0 additions & 58 deletions CONTRIBUTOR.md

This file was deleted.

Loading
Loading