Skip to content

Hole And Bridge Tutorial

Status: Current canonical

This is the smallest end-to-end workflow for Gaia's public-premise and bridge model:

  1. Package A exports a conclusion.
  2. Gaia automatically derives a local_hole from A's unresolved premise.
  3. Package B declares fills(...) against that hole.
  4. Both packages register into the registry.

This flow has been exercised against the official SiliconEinstein/gaia-registry.

What Gaia Does Automatically

You do not mark holes manually.

Given an exported conclusion, Gaia computes its dependency closure during gaia build compile:

  • unresolved local claim premise -> local_hole
  • unresolved foreign claim premise -> foreign_dependency

Those results are written into:

  • .gaia/manifests/exports.json
  • .gaia/manifests/premises.json
  • .gaia/manifests/holes.json
  • .gaia/manifests/bridges.json

When a package is registered, the same manifest files are copied into the registry release directory under packages/<name>/releases/<version>/. holes.json is just the local_hole subset of premises.json.

Package A: Produce A Hole

pyproject.toml:

[project]
name = "paper-a-gaia"
version = "1.0.0"
dependencies = [
  "gaia-lang>=0.5",
]

[tool.gaia]
namespace = "github"
type = "knowledge-package"
uuid = "11111111-1111-1111-1111-111111111111"

src/paper_a/__init__.py:

from gaia.engine.lang import claim
from gaia.engine.lang.compat import deduction

missing_lemma = claim("A missing lemma.")
main_theorem = claim("A theorem that depends on the missing lemma.")

deduction(
    premises=[missing_lemma],
    conclusion=main_theorem,
)

__all__ = ["main_theorem"]

Why compat.deduction? deduction is the v5 named-strategy verb; in v0.5 the canonical replacement is derive(main_theorem, given=[missing_lemma]), which is functionally equivalent. We use compat.deduction here only because the tutorial deliberately walks you through the legacy authoring shape that exposes a missing premise as a local_hole. New v0.5 packages should prefer derive(...); see Migration to alpha 0 §Layer 3.

Compile and inspect:

gaia build compile .
gaia build check .

Expected result:

  • exports.json contains main_theorem
  • premises.json contains missing_lemma with role = "local_hole"
  • holes.json contains the same missing_lemma

Package B: Fill The Hole

Package B depends on package A.

If you are following this tutorial locally before package A is registered, make package A importable inside package B's environment after compiling A:

cd ../paper-b-gaia
uv add --editable ../paper-a-gaia

For an already registered dependency, gaia pkg add paper-a-gaia is the preferred path; it installs the pinned package version and caches any release beliefs.

pyproject.toml:

[project]
name = "paper-b-gaia"
version = "1.0.0"
dependencies = [
  "gaia-lang>=0.5",
  "paper-a-gaia>=1.0.0,<2.0.0",
]

[tool.gaia]
namespace = "github"
type = "knowledge-package"
uuid = "22222222-2222-2222-2222-222222222222"

src/paper_b/__init__.py:

from gaia.engine.lang import claim
from gaia.engine.lang.compat import fills
from paper_a import missing_lemma

bridge_result = claim("A result that establishes the missing lemma.")

fills(
    source=bridge_result,
    target=missing_lemma,
    reason="This result proves the lemma required by package A.",
)

__all__ = ["bridge_result"]

Compile and inspect:

gaia build compile .
gaia build check .

Expected result:

  • exports.json contains bridge_result
  • bridges.json contains one fills relation
  • that relation points to:
  • A's target_qid
  • A's target_interface_hash
  • the resolved dependency version

Important Constraint

fills(target=...) is validated against the dependency package's compiled manifests.

That means:

  1. A must be compiled first.
  2. B must resolve the same package that Gaia validates.
  3. The target claim must appear in A's premises.json.
  4. Its role must be local_hole.

If A's current release no longer exposes that premise as a hole, B's compile fails.

Registration Order

Register package A first, then package B.

gaia pkg register /path/to/paper-a
gaia pkg register /path/to/paper-b

Why the order matters:

  • B's bridge manifest records A's target_resolved_version
  • registry validation checks B against A's registered release interface

What To Look For In The Registry

After A is registered:

  • packages/paper-a/releases/1.0.0/premises.json
  • packages/paper-a/releases/1.0.0/holes.json

After B is registered:

  • packages/paper-b/releases/1.0.0/bridges.json

After index build:

  • index/premises/by-qid/...
  • index/holes/by-qid/...
  • index/bridges/by-target-qid/...
  • index/bridges/by-target-interface/...

Practical Notes

  • Today, authors still write from paper_a import missing_lemma at the source level.
  • Gaia does not trust that import by itself.
  • During compile, Gaia re-validates the target against A's manifest interface.

So the stable contract is not "this symbol is forever a hole". The stable contract is:

  • this claim has a given qid
  • in this release
  • with this interface_hash
  • and role local_hole

That is the object that fills really targets.