Add basic MCP support on the client side#1150
Conversation
…e used simultaneously with user commands
|
Thanks! |
rtetley
left a comment
rtetley
left a comment
There was a problem hiding this comment.
Apart from those two questions, I think this is great work ! I don't have a real opinion about where the MCP server should live ! Your assessment sounds good !
Thanks a lot !
| @@ -0,0 +1,22 @@ | |||
| import { PpString } from '../protocol/types'; | |||
|
|
|||
| export const stringOfPpString = (pp:PpString) : string => { | |||
There was a problem hiding this comment.
Why not use the function exposed in the pp-display library ?
| | SendProofView None -> | ||
| let params = Notification.Server.ProofViewParams.{ proof=None; pp_proof=None; messages=[]; pp_messages=[]; range=Range.top() } in | ||
| | SendProofView (None, req_id_opt) -> | ||
| let params = Notification.Server.ProofViewParams.{ proof=None; pp_proof=None; messages=[]; pp_messages=[]; range=Range.top(); request_id = req_id_opt } in |
There was a problem hiding this comment.
It seems these ProofView events are still Notifications, but you just add an Id to have them functioning like requests ? Is there a reason for not using a Request type ? This is a naive question btw !
|
Closing in favor of #1194 |
|
Sorry about the long inactivity. I used it a bit and I felt that the MCP server using the same VsRocq session isn't the best design, so I was hesitant to push this forward. I feel way more confident about the new server side implementation #1194 |
3 participants
Summary
This PR makes the following changes:
Discussion