Struct LeanHostService 

pub struct LeanHostService { /* private fields */ }

Implementations

impl LeanHostService

pub fn new(broker: Arc<ProjectBroker>, config: ToolConfig) -> Self

impl LeanHostService

pub fn inspect_declaration_tool_attr() -> Tool

Generated tool metadata function for inspect_declaration

pub fn search_for_proof_tool_attr() -> Tool

Generated tool metadata function for search_for_proof

pub fn try_proof_step_tool_attr() -> Tool

Generated tool metadata function for try_proof_step

pub fn verify_declaration_tool_attr() -> Tool

Generated tool metadata function for verify_declaration

pub fn proof_state_tool_attr() -> Tool

Generated tool metadata function for proof_state

pub fn find_references_tool_attr() -> Tool

Generated tool metadata function for find_references

Trait Implementations

impl Clone for LeanHostService

fn clone(&self) -> LeanHostService

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for LeanHostService

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl ServerHandler for LeanHostService

fn get_info(&self) -> ServerInfo

async fn call_tool( &self, request: CallToolRequestParams, context: RequestContext<RoleServer>, ) -> Result<CallToolResult, ErrorData>

async fn list_tools( &self, _request: Option<PaginatedRequestParams>, _context: RequestContext<RoleServer>, ) -> Result<ListToolsResult, ErrorData>

fn get_tool(&self, name: &str) -> Option<Tool>

Get a tool definition by name.

fn enqueue_task( &self, _request: CallToolRequestParams, _context: RequestContext<RoleServer>, ) -> impl Future<Output = Result<CreateTaskResult, ErrorData>> + MaybeSendFuture

fn ping( &self, context: RequestContext<RoleServer>, ) -> impl Future<Output = Result<(), ErrorData>> + MaybeSendFuture

fn initialize( &self, request: InitializeRequestParams, context: RequestContext<RoleServer>, ) -> impl Future<Output = Result<InitializeResult, ErrorData>> + MaybeSendFuture

fn complete( &self, request: CompleteRequestParams, context: RequestContext<RoleServer>, ) -> impl Future<Output = Result<CompleteResult, ErrorData>> + MaybeSendFuture

fn set_level( &self, request: SetLevelRequestParams, context: RequestContext<RoleServer>, ) -> impl Future<Output = Result<(), ErrorData>> + MaybeSendFuture

fn get_prompt( &self, request: GetPromptRequestParams, context: RequestContext<RoleServer>, ) -> impl Future<Output = Result<GetPromptResult, ErrorData>> + MaybeSendFuture

fn list_prompts( &self, request: Option<PaginatedRequestParams>, context: RequestContext<RoleServer>, ) -> impl Future<Output = Result<ListPromptsResult, ErrorData>> + MaybeSendFuture

fn list_resources( &self, request: Option<PaginatedRequestParams>, context: RequestContext<RoleServer>, ) -> impl Future<Output = Result<ListResourcesResult, ErrorData>> + MaybeSendFuture

fn list_resource_templates( &self, request: Option<PaginatedRequestParams>, context: RequestContext<RoleServer>, ) -> impl Future<Output = Result<ListResourceTemplatesResult, ErrorData>> + MaybeSendFuture

fn read_resource( &self, request: ReadResourceRequestParams, context: RequestContext<RoleServer>, ) -> impl Future<Output = Result<ReadResourceResult, ErrorData>> + MaybeSendFuture

fn subscribe( &self, request: SubscribeRequestParams, context: RequestContext<RoleServer>, ) -> impl Future<Output = Result<(), ErrorData>> + MaybeSendFuture

fn unsubscribe( &self, request: UnsubscribeRequestParams, context: RequestContext<RoleServer>, ) -> impl Future<Output = Result<(), ErrorData>> + MaybeSendFuture

fn on_custom_request( &self, request: CustomRequest, context: RequestContext<RoleServer>, ) -> impl Future<Output = Result<CustomResult, ErrorData>> + MaybeSendFuture

fn on_cancelled( &self, notification: CancelledNotificationParam, context: NotificationContext<RoleServer>, ) -> impl Future<Output = ()> + MaybeSendFuture

fn on_progress( &self, notification: ProgressNotificationParam, context: NotificationContext<RoleServer>, ) -> impl Future<Output = ()> + MaybeSendFuture

fn on_initialized( &self, context: NotificationContext<RoleServer>, ) -> impl Future<Output = ()> + MaybeSendFuture

fn on_roots_list_changed( &self, context: NotificationContext<RoleServer>, ) -> impl Future<Output = ()> + MaybeSendFuture

fn on_custom_notification( &self, notification: CustomNotification, context: NotificationContext<RoleServer>, ) -> impl Future<Output = ()> + MaybeSendFuture

fn list_tasks( &self, request: Option<PaginatedRequestParams>, context: RequestContext<RoleServer>, ) -> impl Future<Output = Result<ListTasksResult, ErrorData>> + MaybeSendFuture

fn get_task_info( &self, request: GetTaskInfoParams, context: RequestContext<RoleServer>, ) -> impl Future<Output = Result<GetTaskResult, ErrorData>> + MaybeSendFuture

fn get_task_result( &self, request: GetTaskResultParams, context: RequestContext<RoleServer>, ) -> impl Future<Output = Result<GetTaskPayloadResult, ErrorData>> + MaybeSendFuture

fn cancel_task( &self, request: CancelTaskParams, context: RequestContext<RoleServer>, ) -> impl Future<Output = Result<CancelTaskResult, ErrorData>> + MaybeSendFuture