Define autoformalizer REPL protocol specification#2
Open
faezs wants to merge 4 commits into
Open
Conversation
This implements the Autoformalizer REPL Protocol Specification v1.0, which enables session-typed interaction with an autoformalizer that completes partial Agda formalizations guided by source documents. Protocol components: - Types: All protocol types including identifiers, domains, task/result, priority system, and session operations - Source: Read-only operations on source documents (peek_section, grep_source, get_theorem, get_dependencies) - Bijection: Source-to-formal correspondence tracking with coverage stats - Session: Priority-based session type system ensuring deadlock freedom - Handler: Delegates target operations to agda-mcp, manages state - Protocol: Top-level API with example policies and trace recording Key properties guaranteed by the protocol: - Deadlock freedom (priority ordering) - Session fidelity (linear types) - Termination (bounded priority) Includes comprehensive test suite covering type serialization, source operations, bijection management, session invariants, and handler operations.
The flake.nix had packages.default pointing to 'example' which doesn't exist. Fixed to point to 'agda-mcp' which is the actual package name.
- Add Parser import from Data.Aeson.Types for JSON parsing in Types.hs - Fix Text/String type mismatch in Source.hs section ID generation - Fix handler type in Session.hs executeOp from generic m to IO - Disable tests and haddock in flake.nix for build configuration
Test suite for autoformalizer protocol against mathematical content: - LaTeX source document (ModularSymbols and Continued Fractions) - Agda module with postulates and holes for formalization - Comprehensive test spec covering: - Source document parsing (LaTeX sections, math extraction) - Theorem and definition extraction - Bijection workflow (source-to-formal mapping) - Formalization tasks (fill-hole, section, postulate) - Coverage tracking - Session workflow and priority management Based on themes from Marcolli-Manin paper on modular symbols and noncommutative geometry.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.