v0.6.6

Highlights

• IOTCM protocol parity — invisible goals (unsolved metavariables) are now structurally decoded from the real Agda NamedMeta wire format, verified against the official Haskell sources across v2.7.0.1, v2.8.0, and master.
• False ok-complete fix — agda_load / agda_load_no_metas could incorrectly report success when source holes existed inside abstract blocks (reported by the protocol as invisible goals only). A gated source-level hole scan now catches these cases.
• Strict-load enforcement — agda_load_no_metas now correctly forces type-error whenever any visible goals, invisible goals, or source-level hole markers remain.

Fixed

• agda_load / agda_load_no_metas could report ok-complete despite explicit hole markers ({!!}, ?, {! expr !}) when the Agda protocol under-reported goals (e.g. holes inside abstract blocks).
• invisibleGoalCount undercount when multiple AllGoalsWarnings display events occur during a single load — now preserved as the maximum across events.
• agda_load_no_metas strict-load enforcement: forces type-error classification whenever any holes or metas remain.

Added

• Invisible goals are now decoded into DecodedInvisibleGoal entries (name + type) in DecodedLoadDisplay, matching the official encodeTCM NamedMeta instance.
• Cross-version protocol reference (tooling/protocol/data/official-cross-version-notes.json) documenting stable JSON field mappings across Agda versions.
• 8 new Agda fixtures for protocol conformance stress testing: MixedHoleStyles, HoleInStringComment, AbstractHoleMultiple, MixedVisibleInvisible, PostulateAndHole, NestedAbstractHole, MultiPostulateComplete, AbstractComplete.

Changed

• Removed dead classifyParsedLoad() helper; consolidated into a shared classifyLoadResult() function.
• runLoadNoMetas classification simplified to "ok-complete" / "type-error" only (removed unreachable "ok-with-holes" branch).

Breaking changes

• No intentional API break.