Name a set of objects with a bundle

Record a set of accepted objects under export names once, then receive them all in a draft as Received bindings.

A bundle (lema.bundle/v1) maps export names to exact object IDs and roles. It is a store record, not an object, so creating one changes no ID. A draft that receives a bundle builds exactly the objects it would build with the same bindings written by hand. The example below is the one crates/lema-cli/tests/bundles.rs runs: two bundles received by lean/std/MapClient.lean.

Before you start

• A running server on a store where the objects to export are accepted. Here that is Core v2, with the aliases core.Prog, core.Prog.call, core.Prog.ret and core.Safe, and lean/std/Map.lean.
• You know how Received.* bindings work in elaborate (Reuse a proof by identity).
• In the commands, $SOCK is the server’s socket. Values in angle brackets are placeholders.

Steps

1. Create a bundle from aliases. Each alias is resolved once, now, to the ID it names, so later moves of the alias do not change the bundle:

   {"from_aliases": [
      {"alias": "core.Prog", "name": "Prog"},
      {"alias": "core.Prog.call", "name": "Prog.call"},
      {"alias": "core.Prog.ret", "name": "Prog.ret"},
      {"alias": "core.Safe", "name": "Safe"}],
    "doc": "Core v2 programs and their safety."}

   lema --socket $SOCK call bundle.create --params-file core-bundle.json

   The response is {id, created, exports}. A plain alias name in from_aliases, instead of an object, exports the alias under its own name.

2. Create a bundle from IDs. List exports as {name, id, role?}. Here each entry is a name’s {id, role?} from Map’s names map, with name added. A declaration is exported by its plain ID. A structure or inductive type needs one of its roles (type, ctor, ctor:i, field:i, generated:rec). The Map bundle exports Order, MapOp, MapOp.insert, MapOp.toList, MapReply, contract, Sorted, find, update_self and update_other:

   {"exports": [<ten entries, each {name, id, role?}>],
    "helpers": ["update_self", "update_other"],
    "depends": ["<core bundle id>"],
    "doc": "Std.Map: the finite map contract and its lemmas."}

   • helpers are left out of bundle.list’s names unless you ask for them. They are received like any other export.
   • depends records the bundles this one re-exports from. Receiving a bundle does not receive its dependencies.
   • Export names are dotted identifiers that Lean parses without escapes, and without ? or !. That is why find? is exported as find.

   Sending the same exports again, in any order, returns the same id with created: false.

3. Inspect the bundles:

   lema --socket $SOCK call bundle.get --params '{"id": "<core bundle id>"}'
   lema --socket $SOCK call bundle.list --params '{"names": true}'

   bundle.get returns the record. bundle.list returns one row per bundle, {id, exports, helpers, doc?, depends?, names?}, where exports and helpers are counts. names: true adds the export names, and helpers: true with it adds the helpers too.

4. Receive the bundles in elaborate, or in publish to accept the draft in the same call. Each export N becomes the binding Received.N, or Received.<as>.N when the receive gives as. rename maps an export name to another local name. MapClient uses names such as Received.call and Received.mapInsert, so it renames:

   {"source": "<text of lean/std/MapClient.lean>",
    "prefix": "LemaDraft",
    "seed_salt": "lean/std/MapClient",
    "receive": [
      {"bundle": "<core bundle id>",
       "rename": {"Prog.call": "call", "Prog.ret": "ret"}},
      {"bundle": "<map bundle id>",
       "rename": {"MapOp.insert": "mapInsert", "MapOp.toList": "mapToList",
                  "contract": "mapContract", "find": "mapFind",
                  "update_self": "updateSelf", "update_other": "updateOther"}}]}

   lema --socket $SOCK call publish --params-file client.json

   You can mix receive with explicit bindings. With receive, the response adds received_bundles, the sorted IDs of the bundles received, so a consumer can pin them. With {"bundle": "<core bundle id>", "as": "Core"} instead, the bindings would be Received.Core.Prog, Received.Core.Safe and so on.

A receive binds every export and installs the closure of all of them, so keep each bundle to what its consumers need. Json’s laws, for example, are a bundle of their own.

Refusals

All of these are refused before any native call: