Module manifest_validation 

Static, link-free validation of Lean capability manifests.

Lives in lean-toolchain so the worker parent crate can fast-fail bad manifests on the client side without re-linking libleanshared through lean-rs. The runtime preflight in lean-rs reuses the same parser and diagnostic shapes and layers symbol-table inspection on top.

Structs

CapabilityManifest

Parsed Lean capability manifest.

Functions

check_fingerprint

Validate the toolchain fingerprint against this lean-toolchain build.

check_staleness

Warn if the manifest is older than its primary dylib.

check_static

Static manifest validation: file-exists, JSON parse, schema check, toolchain fingerprint match, and primary-dylib staleness.