Markdown for LLMs

Importing external knowledge

The source Markdown for this article. Copy it into your assistant or download it as a text file.

# Importing external knowledge

External knowledge — ontologies, measurement systems, proof-assistant
libraries — enters the corpus through a pipeline, never by pasting. The
`ingest` command walks a recipe from survey to compiled packages, and every
declaration it produces carries an explicit outcome. The worked example
below comes first; the stages, the command forms, and the formats follow.

Environment: `ingest` **requires a source checkout** (I). It is absent
from the public `law-v0.1.1` composition and runs through the checkout
launcher `./law` from the repository root — see
[Before you start](/corpus/lab/#before-you-start). Input files: the
`docs/corpus/lab/fixtures/import-mini/` fixture. The (I) marks below
track the command's status, not the engine's: the worked example
verifies the transformation itself.

Confirmation marks in parentheses, such as (S) or (I), follow the
[legend on the topic index](/corpus/#how-this-topic-marks-confidence).

## A minimal worked import

The lab ships a minimal import fixture: a recipe naming a snapshot and a
mapping, plus a package policy. The snapshot holds two declarations over
parcel words — one plain rule, one asking for an extension the pipeline
does not have. The recipe itself is three lines:

```json
{
  "format": "arxo.import.recipe/0.1",
  "input": "input.json",
  "mapping": "mapping.json"
}
```

The policy assigns everything to one new package with no split:

```json
{
  "format": "arxo.import.package-policy/0.1",
  "packages": {
    "labparcels.glossary": {
      "version": "0.1.0",
      "namespace": "urn:law:lab:parcels:glossary",
      "boundary": "lab"
    }
  },
  "assignments": []
}
```

Reading the report shows what the recipe selects: one declaration
becomes a rule, the other is blocked with its reason. **(I)**

```text
$ ./law ingest inspect docs/corpus/lab/fixtures/import-mini/recipe.json | python3 -c "import json,sys; r=json.load(sys.stdin); [print(k,'->',v['status'],v['code'],'-',v['message']) for k,v in r['declarations'].items()]"
registered-when-held -> rule IIM-RULE - rule obtained with kept conditions
remote-proof-case -> blocked IIM-UNSUPPORTED - required extension remote_proof
```

The plan form previews the package split before anything is built. Note
the compiler verdict: the plan never runs the compiler, so it reads
`not_run`. **(I)**

```text
$ ./law ingest plan docs/corpus/lab/fixtures/import-mini/recipe.json --policy docs/corpus/lab/fixtures/import-mini/policy.json | python3 -c "import json,sys; r=json.load(sys.stdin); print('compiler_check:',r['compiler_check'],'| basis:',r['basis']); print('order:',r['order']); print('outcomes:',{k:v['status'] for k,v in r['outcomes'].items()}); print('members:',len(r['packages']['labparcels.glossary']['members']))"
compiler_check: not_run | basis: emitted_references/0.1
order: ['labparcels.glossary']
outcomes: {'registered-when-held': 'rule', 'remote-proof-case': 'blocked'}
members: 6
```

Building without the partial flag is refused while a blocked record
stands; the command exits nonzero. **(I)**

```text
$ ./law ingest build docs/corpus/lab/fixtures/import-mini/recipe.json --policy docs/corpus/lab/fixtures/import-mini/policy.json --out /tmp/lab-work/import-mini
law ingest: IIM-PARTIAL: bundle has blocked records; use plan or explicitly --allow-partial
```

With the flag the supported slice builds, and the bundle records that
the compiler ran: `checked` against the plan's `not_run`. The
correspondence maps the kept declaration to its new rule and the
blocked one to nothing. **(I)**

```text
$ ./law ingest build docs/corpus/lab/fixtures/import-mini/recipe.json --policy docs/corpus/lab/fixtures/import-mini/policy.json --out /tmp/lab-work/import-mini --allow-partial | python3 -c "import json,sys; r=json.load(sys.stdin); print('compiler_check:',r['compiler_check'],'| allow_partial:',r['allow_partial']); p=r['packages']['labparcels.glossary']; print('package:',p['version'],p['content_hash']); [print('decl',c['item']['source'],'->',c['target']) for c in r['correspondence'] if c['item']['kind']=='declaration']"
compiler_check: checked | allow_partial: True
package: 0.1.0 sha256:6b2108127c41e22e00021065858724f05749c8538f4d1a44615696ba3298ffb5
decl registered-when-held -> urn:law:lab:parcels:glossary#Import_Rule_9a6cdfd2b483af29b7e6e4de03a05f362d132d8ee78a499f1cb3cb44fa8b0231
decl remote-proof-case -> None
```

The check form reruns the same verification without writing a directory: **(I)**

```text
$ ./law ingest check docs/corpus/lab/fixtures/import-mini/recipe.json --policy docs/corpus/lab/fixtures/import-mini/policy.json --allow-partial | python3 -c "import json,sys; r=json.load(sys.stdin); print('compiler_check:',r['compiler_check'],'| allow_partial:',r['allow_partial'])"
compiler_check: checked | allow_partial: True
```

The bundle directory keeps the inputs beside the outputs, so a later
reader can rebuild it:

```text
$ ls -R /tmp/lab-work/import-mini
bundle-report.json
input.json
mapping.json
package-plan.json
packages
policy.json
recipe.json
world.lawir.json

/tmp/lab-work/import-mini/packages:
labparcels.glossary

/tmp/lab-work/import-mini/packages/labparcels.glossary:
law.lock
law.toml
package.law
package.lawir.json
sources
sources.law

/tmp/lab-work/import-mini/packages/labparcels.glossary/sources:
Import_Document_41cf6794ba4200b839c53531555f0f3998df4cbb01a4d5cb0b94e3ca5e23947d.txt
```

The generated package holds the lowered rule with its conditions kept:

```law
@source(Import_Fragment_b111c6e1d318f203063e5c16bab43c108326af0aa2f7b65760c95547a43dbe52)
rule Import_Rule_9a6cdfd2b483af29b7e6e4de03a05f362d132d8ee78a499f1cb3cb44fa8b0231(
    v0: Parcel,
) strict {
    label ru unofficial "Registration from holding and kind";
    when owns(v0) and kind_of(v0);
    then registered(v0);
}
```

A second recipe beside the first changes both the source text and one
mapping label. The diff between them names exactly those two changes
and the two records a rebuild would revisit: **(I)**

```text
$ ./law ingest diff docs/corpus/lab/fixtures/import-mini/recipe.json docs/corpus/lab/fixtures/import-mini/recipe-after.json | python3 -c "import json,sys; r=json.load(sys.stdin); print('input changed:',r['before']['input_hash']!=r['after']['input_hash']); print('mapping changed:',r['before']['mapping_hash']!=r['after']['mapping_hash']); print('documents:',{k:v['kind'] for k,v in r['documents'].items()}); print('mapping:',{k:(v['kind'],v['fields']) for k,v in r['mapping'].items()}); print('rebuild records:',r['rebuild']['records'])"
input changed: True
mapping changed: True
documents: {'source': 'changed'}
mapping: {'predicates/registered': ('changed', {'label': {'after': 'Parcel is registered (refined wording)', 'before': 'Parcel is registered'}})}
rebuild records: ['registered-when-held', 'remote-proof-case']
```

## Every declaration gets an outcome

The import report assigns each produced declaration exactly one outcome,
quoted here from the report format:

```text
"rule", "fact", "catalogue", "blocked"
```

A `rule` becomes executable corpus content, a `fact` becomes pinned data, a
`catalogue` entry becomes a discovery record without semantics, and a
`blocked` entry names content the policy refused with its reason. Nothing
lands silently: the report journal records what each input became. **(I)**

## The pipeline

The stages run in order: survey the upstream source, extract a working set,
inspect it, build packages, and check the result. A separate diff form
compares two recipes or reports, and a plan form previews the package split
before anything is built.

The engine behind these stages is a pure transformation: recipes and source
snapshots in, packages and reports out, with no network access during the
build itself. **(I)**

## Command reference

The observed command surface (error-stream output) of the stages:

```text
$ ./law ingest --help
law ingest: law ingest survey|extract|inspect|build|check <recipe.json> [--out <new dir>] [--allow-partial] [--stream] [--cache <dir>] [--compile-cache <dir>] [--json]
law ingest diff <before-recipe-or-report> <after-recipe-or-report> [--jobs <1..32>] [--before-policy <policy.json>] [--after-policy <policy.json>] [--packages] [--compile-cache <dir>] [--scenarios <files>] [--allow-partial] [--json]
law ingest plan <recipe.json> --policy <package-policy.json> [--json]
law ingest build|check <recipe.json> --policy <policy.json> [--jobs <1..32>] [--plan <expected-plan.json>] [--compile-cache <dir>] [--out <dir>] [--allow-partial] [--json]
```

The top-level help shows the shorter everyday forms of the same stages:

```text
$ ./law --help
law ingest survey|extract|inspect|build|check <recipe.json> [--out <dir>] [--allow-partial] [--stream] [--cache <dir>]
law ingest diff <before-recipe-or-report> <after-recipe-or-report> [--packages] [--scenarios <files>] [--allow-partial] [--json]
```

## The eleven schemas

Recipe, inventory, coverage, intermediate form, mapping, adapter, bundle,
package plan, package policy, diff, and report each have their own format.
Observed schema files:

```text
$ ls spec/schema/ | grep -i import
import-adapter.schema.json
import-bundle.schema.json
import-coverage.schema.json
import-diff.schema.json
import-inventory.schema.json
import-ir.schema.json
import-mapping.schema.json
import-package-plan.schema.json
import-package-policy.schema.json
import-recipe.schema.json
import-report.schema.json
```

The recipe and adapter formats are consumed directly by the command-line
stages; the rest are the contracts between stages and between the pipeline
and review tooling. **(O for the formats as contracts; S where the stages
consume them.)**

## Checks run in the full profile only

The import contract, survey freshness, alignment, and bundle checks execute
as part of the full corpus profile, not the ordinary one: routine package
work never waits on upstream-source verification. Survey snapshots refresh
explicitly, and import releases publish through a staged manifest with file
ownership and a stage graph. The checks are a **full-profile CI check**
(G); the release tooling **requires a source checkout** (I).

## The alignment boundary in the report format

Imported rules sometimes mirror source concepts under a mapping. The
alignment report format draws one hard line around such mirrors: a
decision may record a declared assumption, never a proved equivalence.
Six fields of the shipped format carry that line: **(O)**

```law
$ python3 - <<'EOF'
import json
s = json.load(open('spec/schema/concept-rule-alignment-report.schema.json'))
d = s['properties']['decisions']['items']['properties']
print('direction:', json.dumps(d['direction']))
print('relation:', json.dumps(d['relation']))
print('status:', json.dumps(d['status']))
print('conditions.interpretation_basis:', json.dumps(d['conditions']['properties']['interpretation_basis']))
print('all_source_conditions_retained:', json.dumps(d['conditions']['properties']['all_source_conditions_retained']))
print('semantic_equivalence_proved:', json.dumps(d['conditions']['properties']['semantic_equivalence_proved']))
EOF
direction: {"const": "source_to_target_under_interpretation"}
relation: {"enum": ["conditional_rule_implementation", "definition_equivalence"]}
status: {"enum": ["accepted", "review", "revoked"]}
conditions.interpretation_basis: {"const": "declared_mapping_assumption"}
all_source_conditions_retained: {"const": true}
semantic_equivalence_proved: {"const": false}
```

Every decision runs one way, from source to target under the declared
interpretation; every decision retains all source conditions; and every
decision states that equivalence is unproved. A probe against the
shipped format shows the boundary holding: the entry that states
unproved equivalence validates,
while an entry claiming proved equivalence — or renaming the basis to
one — is refused: **(O)**

```law
$ python3 - <<'EOF'
import json
from jsonschema import Draft202012Validator
schema = json.load(open('spec/schema/concept-rule-alignment-report.schema.json'))
check = Draft202012Validator(schema['properties']['decisions']['items']).is_valid
H = 'sha256:' + '1' * 64
honest = {'id': H, 'source': 'Glossary: holding plus recorded kind',
 'target': 'labparcels.glossary#Import_Rule',
 'relation': 'conditional_rule_implementation',
 'direction': 'source_to_target_under_interpretation', 'output': None,
 'parameters': [{'id': 'x', 'type_symbol': 'Parcel'}],
 'reasons': ['positive structure matches under the pinned mapping'],
 'status': 'accepted',
 'conditions': {'interpretation_basis': 'declared_mapping_assumption',
  'interpretation_hash': H, 'source_shape': {'types': ['Parcel'],
   'premises': [['owns', [0]], ['kind_of', [0]]], 'head': ['registered', [0]]},
  'all_source_conditions_retained': True, 'semantic_equivalence_proved': False},
 'alternatives': [], 'evidence': {'source': [], 'target': []}}
print('declared assumption, equivalence unproved:', 'VALID' if check(honest) else 'REFUSED')
claimed = dict(honest, conditions=dict(honest['conditions'], semantic_equivalence_proved=True))
print('claimed proved equivalence:', 'VALID' if check(claimed) else 'REFUSED')
renamed = dict(honest, conditions=dict(honest['conditions'], interpretation_basis='proved_equivalence'))
print('renamed interpretation basis:', 'VALID' if check(renamed) else 'REFUSED')
EOF
declared assumption, equivalence unproved: VALID
claimed proved equivalence: REFUSED
renamed interpretation basis: REFUSED
```

## What to read next

- [Command-line reference](/cli/) for the ingest stage details.
- [Schema catalog](/protocols/schemas/) for the eleven import formats.
- [LawQL reference](/lawql/) for querying imported packages once built.
- [Alignment and concept bridges](/corpus/alignment/) for the full
  alignment picture this boundary belongs to.