Importing external knowledge

For LLMs8 sections

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. 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.

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:

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

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

{
  "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)

$ ./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)

$ ./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)

$ ./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)

$ ./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)

$ ./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:

$ 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:

@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)

$ ./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:

"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:

$ ./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:

$ ./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:

$ 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)

$ 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)

$ 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