Fstar MCP

F\*MCP服务器

为F\*提供前端的MCP（模型上下文协议）服务器 --ide stdio协议。这使得AI助手能够通过MCP标准与F\*进行交互，以进行类型检查、符号查找和其他IDE功能。

特性

• 会话管理：每个文件路径一个会话，自动替换
• **全F* IDE协议支持*\*：类型检查、符号查找等
• 证明上下文：类型检查期间的访问证明义务和目标

安装

# Build the server
cargo build --release

# Run the server
./target/release/fstar-mcp

MCP工具

create_session

创建一个新的F\*会话。所有参数都是可选的，具有合理的默认值。

参数：

• file_path （string，可选）：F\*文件的路径。如果省略，则创建一个临时.fst文件。
• fstar_exe （字符串，可选）：fstar.exe的路径。在PATH中默认为“fstar.exe”。
• cwd （字符串，可选）：F\*的工作目录。默认为文件的目录。
• include_dirs （字符串数组，可选）：包括目录（--Include路径）。
• options （字符串数组，可选）：F\*命令行选项（例如。， ['--cache_dir', '.cache']).

退货：

{
  "session_id": "uuid",
  "status": "ok" | "error",
  "diagnostics": [...],
  "fragments": [...],
  "created_at": "2024-01-01T00:00:00Z"
}

list_sessions

列出所有活动的F\*会话及其状态信息。

参数： 无

退货：

{
  "sessions": [...],
  "count": 2
}

typecheck_buffer

在现有的F\*会话中键入检查代码。

参数：

• session_id （string）：会话ID来自 create_session
• code （string）：用于类型检查的F\*代码
• lax （boolean，可选）：如果为true，则使用lax模式（允许所有SMT查询）。kind='ax'的快捷方式
• kind （string，可选）：类型检查类型- "full", "lax", "cache", "reload-deps", "verify-to-position", "lax-to-position"默认值： "full"被松懈压倒=真
• to_line （整数，可选）：要进行类型检查的行（用于基于位置的类型）
• to_column （整数，可选）：要进行类型检查的列（用于基于位置的类型）

退货：

{
  "status": "ok" | "error",
  "diagnostics": [...],
  "fragments": [...]
}

update_buffer

在F\*的虚拟文件系统中添加或更新文件（vfs-Add）。

参数：

• session_id （string）：会话ID来自 create_session
• file_path （string）：虚拟文件系统中文件的路径
• contents （string）：文件内容

退货：

{
  "status": "ok" | "error"
}

lookup_symbol

查找符号的类型信息、文档和定义位置。

参数：

• session_id （string）：会话ID来自 create_session
• file_path （string）：包含符号的文件的路径
• line （整数）：行号（从1开始）
• column （整数）：列号（从0开始）
• symbol （string）：要查找的符号

退货：

{
  "kind": "symbol" | "module" | "not_found",
  "name": "FStar.List.map",
  "type_info": "('a -> 'b) -> list 'a -> list 'b",
  "documentation": "...",
  "defined_at": {
    "file": "...",
    "start_line": 1,
    "start_column": 0,
    "end_line": 1,
    "end_column": 10
  }
}

get_proof_context

在某个职位上获得证明义务和目标。返回上次类型检查期间收集的证明状态。

参数：

• session_id （string）：会话ID来自 create_session
• line （整数，可选）：获取证明状态的行号。如果省略，则返回所有证明状态。

退货：

{
  "found": true,
  "line": 10,
  "proof_state": {...}
}

或者当没有指定行时：

{
  "count": 3,
  "proof_states": [...]
}

restart_solver

重新启动会话的Z3 SMT求解器。

参数：

• session_id （string）：会话ID来自 create_session

退货：

{
  "status": "ok"
}

close_session

关闭F\*会话并清理资源。

参数：

• session_id （string）：会话ID来自 create_session

退货：

{
  "status": "ok"
}

发展

# Run tests
cargo test

# Run with debug logging
RUST_LOG=fstar_mcp=debug cargo run

许可证

麻省理工学院