Release an artifact

Pin a built artifact to the store's accepted closure and a deployment configuration, then run it by release ID.

A release (lema.release/v1) is a store record of what a deployment runs, and it never changes. It pins one artifact, the closure and receipts that artifact was built from, and the digest of a deployment configuration. A release adds no claim of its own. Its proof receipts are the store’s receipts from the pinned Lean 4.34.1 kernel (checked). The artifact and its IR receipts are tested. The compilers, runtime and OS are assumed.

Before you start

• A built artifact under the runtime output’s artifacts/. This is either an execution artifact from Build a native executable (kind exec), or an app artifact from Build a capability app (kind exec-app).
• A deployment, in $DEPLOYMENT:
  • for an execution artifact, a lema.cap-config/v1 configuration file (see “Configuration” in crates/lema-cap/FRAMES.md). The program never reads it, but the release pins its digest;
  • for an app artifact, the deployment directory. The release pins that directory’s lema-cap.json.
• The server stopped. lema release and lema run --release open the store directly.
• A shell at the repository root, for --lean lean in step 3.
• In the commands, $STORE is the store directory and $CONFIG your runtime configuration.

1. Check the deployment’s digest

lema release deployment --deployment $DEPLOYMENT

It prints the digest as sha256. With --input it also prints what the digest covers, which is your private configuration: it holds references to credentials, never their values. The release tool never opens a credential file, and an unknown field anywhere in the configuration is refused.

2. Create the release

lema release create --store $STORE --runtime $CONFIG --artifact sha-digest-native \
  --deployment $DEPLOYMENT --doc "SHA-256 command, first deployment."

The command verifies the artifact as a run would, re-derives its closure and proof receipts from the store, and writes the record. The output gives the release’s id (keep it as $ID), its kind and whether it was created. Add --bundles ID,.. to pin stored bundles too. The same parts always give the same ID. A different --doc, or a different deployment configuration, gives a different release.

3. Verify it

lema release verify --store $STORE --runtime $CONFIG --release $ID --artifact sha-digest-native \
  --deployment $DEPLOYMENT --lean lean

verify re-derives every binding: the record and its ID, the closure and receipts from the store, the bundles, and the artifact’s own bindings. With --deployment it also checks the configuration’s digest, and with --lean the digest of each piece file. Any difference is an error that names the binding.

4. Select and run it

lema release select --store $STORE --runtime $CONFIG --release $ID --artifact sha-digest-native \
  --deployment $DEPLOYMENT
lema run --runtime $CONFIG --artifact sha-digest-native --release $ID --store $STORE \
  --deployment $DEPLOYMENT --input FILE

A deployment selects a release by its ID only. The release must not be withdrawn, and its creation must be recorded in this store’s history. Selection re-derives every binding with the deployment’s own configuration. lema run --release goes through the same gate before it runs anything, and prints release ... selected on standard error. Every refusal comes before any native call.

For an app artifact, --deployment is its deployment directory, and lema run takes no arguments after --, because an app takes only an input.

5. Supersede or withdraw it

lema release show --store $STORE --release $ID
lema release list --store $STORE
lema release supersede --store $STORE --release $ID --by $NEW_ID --reason "Smaller binary."
lema release withdraw --store $STORE --release $ID --reason "Wrong configuration."

show gives the record and its status in this store. A superseded release can still be selected, as a rollback: its status names its successors, and lema run says it runs it as a rollback. A withdrawn release can never be selected again, and creating the same content again gives the same ID, still withdrawn. Withdrawal and supersession belong to this store and do not travel with a copied record.

Refusals you may see

A release record copied from another store passes verify, but it cannot be selected until it is created in this store. Nothing runs a capability application release (kind cap-app) yet.

What is tested

The release rules, store bindings, tamper refusals, withdrawal, supersession and the exclusion of secrets are tested without a runtime (crates/lema-store/tests/release.rs and the unit tests of lema release and lema run --release). The native suites are crates/lema-cli/tests/release.rs for an execution artifact and crates/lema-cli/tests/standalone.rs for app artifacts. The repository records no native pass of release.rs, and its documents disagree on whether the release part of standalone.rs has run natively, so this page claims neither.