From 2ae6ba548c8aa54852da1fa4796582e003f9408d Mon Sep 17 00:00:00 2001 From: Romain Tetley Date: Wed, 26 Jun 2024 11:21:56 +0200 Subject: [PATCH] Adapt to new API --- flake.lock | 10 ++++---- language-server/dm/delegationManager.ml | 10 ++++---- language-server/dm/delegationManager.mli | 2 +- language-server/dm/document.ml | 18 +++++++------- language-server/dm/documentManager.ml | 21 +++++++++-------- language-server/dm/executionManager.ml | 30 ++++++++++++------------ language-server/dm/executionManager.mli | 2 +- language-server/dm/parTactic.ml | 2 +- language-server/protocol/lspWrapper.ml | 4 ++-- 9 files changed, 50 insertions(+), 49 deletions(-) diff --git a/flake.lock b/flake.lock index 37a65e938..e94a7faae 100644 --- a/flake.lock +++ b/flake.lock @@ -8,17 +8,17 @@ ] }, "locked": { - "lastModified": 1717586410, - "narHash": "sha256-LGzKrJkT8YSVxwvoC1zD4KFqqj3a8HIVBB5LCqxsxlU=", + "lastModified": 1719227091, + "narHash": "sha256-E+umUAkUuyLyK7L4b1vCddqZRKGZw6bL18IaOrJHsjo=", "owner": "coq", "repo": "coq", - "rev": "72b053e90e23c7085316fff809a60d5e195c3c32", + "rev": "e139cf972cf2a876583ebbf5a19ffd419828116b", "type": "github" }, "original": { - "owner": "gares", + "owner": "coq", "repo": "coq", - "rev": "72b053e90e23c7085316fff809a60d5e195c3c32", + "rev": "e139cf972cf2a876583ebbf5a19ffd419828116b", "type": "github" } }, diff --git a/language-server/dm/delegationManager.ml b/language-server/dm/delegationManager.ml index 67e513603..ebe9f868b 100644 --- a/language-server/dm/delegationManager.ml +++ b/language-server/dm/delegationManager.ml @@ -49,7 +49,7 @@ module type Job = sig val binary_name : string val initial_pool_size : int type update_request - val appendFeedback : Feedback.route_id * sentence_id -> (Feedback.level * Loc.t option * Pp.t) -> update_request + val appendFeedback : Feedback.route_id * sentence_id -> (Feedback.level * Loc.t option * Quickfix.t list * Pp.t) -> update_request end (* One typically created a job id way before the worker is spawned, so we @@ -66,8 +66,8 @@ let cancel_job (_,id) = keep here the conversion (STM) feedback -> (LSP) feedback *) let install_feedback send = - Log.feedback_add_feeder_on_Message (fun route span _ lvl loc _ msg -> - send (route,span,(lvl,loc,msg))) + Log.feedback_add_feeder_on_Message (fun route span _ lvl loc qf msg -> + send (route,span,(lvl,loc, qf, msg))) module type Worker = sig type job_t @@ -297,7 +297,7 @@ let handle_event = function exit 0 | Error(msg, cleanup_events) -> log @@ "worker did not spawn: " ^ msg; - (Some(Job.appendFeedback feedback_route (Feedback.Error,None,Pp.str msg)), cleanup_events) + (Some(Job.appendFeedback feedback_route (Feedback.Error,None,[],Pp.str msg)), cleanup_events) else match create_process_worker procname cancellation_handle job with | Ok events -> @@ -305,7 +305,7 @@ let handle_event = function (None, events) | Error(msg, cleanup_events) -> log @@ "worker did not spawn: " ^ msg; - (Some(Job.appendFeedback feedback_route (Feedback.Error,None,Pp.str msg)), cleanup_events) + (Some(Job.appendFeedback feedback_route (Feedback.Error,None,[],Pp.str msg)), cleanup_events) (* the only option is the socket port *) diff --git a/language-server/dm/delegationManager.mli b/language-server/dm/delegationManager.mli index 64c9b4031..9b0856bb1 100644 --- a/language-server/dm/delegationManager.mli +++ b/language-server/dm/delegationManager.mli @@ -42,7 +42,7 @@ module type Job = sig type update_request (** Called to handle feedback sent by the worker process *) - val appendFeedback : Feedback.route_id * sentence_id -> (Feedback.level * Loc.t option * Pp.t) -> update_request + val appendFeedback : Feedback.route_id * sentence_id -> (Feedback.level * Loc.t option * Quickfix.t list * Pp.t) -> update_request end type job_handle diff --git a/language-server/dm/document.ml b/language-server/dm/document.ml index 7d3424152..0dd9a9310 100644 --- a/language-server/dm/document.ml +++ b/language-server/dm/document.ml @@ -330,7 +330,7 @@ let get_loc_from_info_or_exn e info = let get_loc_from_info_or_exn _ info = Loc.get_loc info -let get_qf_from_info info = Quickfix.get_qf info +(* let get_qf_from_info info = Quickfix.get_qf info *) [%%endif] [%%if coq = "8.18" || coq = "8.19"] @@ -381,25 +381,25 @@ let rec parse_more synterp_state stream raw parsed parsed_comments errors = with exn -> let e, info = Exninfo.capture exn in let loc = get_loc_from_info_or_exn e info in - let qf = get_qf_from_info info in - handle_parse_error start (loc, Pp.string_of_ppcmds @@ CErrors.iprint_no_report (e,info)) qf + let qf = Result.value ~default:[] @@ Quickfix.from_exception e in + handle_parse_error start (loc, Pp.string_of_ppcmds @@ CErrors.iprint_no_report (e,info)) (Some qf) end | exception (E msg as exn) -> let loc = Loc.get_loc @@ Exninfo.info exn in - let qf = Quickfix.get_qf @@ Exninfo.info exn in + let qf = Result.value ~default:[] @@ Quickfix.from_exception exn in junk_sentence_end stream; - handle_parse_error start (loc,msg) qf + handle_parse_error start (loc,msg) (Some qf) | exception (CLexer.Error.E e as exn) -> (* May be more problematic to handle for the diff *) let loc = Loc.get_loc @@ Exninfo.info exn in - let qf = Quickfix.get_qf @@ Exninfo.info exn in + let qf = Result.value ~default:[] @@ Quickfix.from_exception exn in junk_sentence_end stream; - handle_parse_error start (loc,CLexer.Error.to_string e) qf + handle_parse_error start (loc,CLexer.Error.to_string e) (Some qf) | exception exn -> let e, info = Exninfo.capture exn in let loc = Loc.get_loc @@ info in - let qf = Quickfix.get_qf @@ Exninfo.info exn in + let qf = Result.value ~default:[] @@ Quickfix.from_exception exn in junk_sentence_end stream; - handle_parse_error start (loc, "Unexpected parse error: " ^ Pp.string_of_ppcmds @@ CErrors.iprint_no_report (e,info)) qf + handle_parse_error start (loc, "Unexpected parse error: " ^ Pp.string_of_ppcmds @@ CErrors.iprint_no_report (e,info)) (Some qf) end let parse_more synterp_state stream raw = diff --git a/language-server/dm/documentManager.ml b/language-server/dm/documentManager.ml index 887410448..e6f127fa0 100644 --- a/language-server/dm/documentManager.ml +++ b/language-server/dm/documentManager.ml @@ -127,15 +127,16 @@ let make_diagnostic doc range oloc message severity code = | Some (x,z) -> Some x, Some z in Diagnostic.create ?code ?data ~range ~message ~severity () -let mk_diag st (id,(lvl,oloc,msg)) = - let code = - match lvl with - | Feedback.Warning quickfixes -> +let mk_diag st (id,(lvl,oloc,qf,msg)) = + let code = + match qf with + | [] -> None + | qf -> let code : Jsonrpc.Id.t * Lsp.Import.Json.t = let open Lsp.Import.Json in (`String "quickfix-replace", - quickfixes |> yojson_of_list - (fun qf -> + qf |> yojson_of_list + (fun qf -> let s = Pp.string_of_ppcmds @@ Quickfix.pp qf in let loc = Quickfix.loc qf in let range = RawDocument.range_of_loc (Document.raw_document st.document) loc in @@ -143,9 +144,9 @@ let mk_diag st (id,(lvl,oloc,msg)) = )) in Some code - | _ -> None in - let lvl = DiagnosticSeverity.of_feedback_level lvl in - make_diagnostic st.document (Document.range_of_id st.document id) oloc (Pp.string_of_ppcmds msg) lvl code + in + let lvl = DiagnosticSeverity.of_feedback_level lvl in + make_diagnostic st.document (Document.range_of_id st.document id) oloc (Pp.string_of_ppcmds msg) lvl code let mk_error_diag st (id,(oloc,msg,qf)) = (* mk_diag st (id,(Feedback.Error,oloc, msg)) *) let code = @@ -222,7 +223,7 @@ let get_messages st pos = | Some id -> log "get_messages: Found id"; let error = ExecutionManager.error st.execution_state id in let feedback = ExecutionManager.feedback st.execution_state id in - let feedback = List.map (fun (lvl,_oloc,msg) -> DiagnosticSeverity.of_feedback_level lvl, pp_of_coqpp msg) feedback in + let feedback = List.map (fun (lvl,_oloc,_,msg) -> DiagnosticSeverity.of_feedback_level lvl, pp_of_coqpp msg) feedback in match error with | Some (_oloc,msg) -> (DiagnosticSeverity.Error, pp_of_coqpp msg) :: feedback | None -> feedback diff --git a/language-server/dm/executionManager.ml b/language-server/dm/executionManager.ml index 0537eb017..99f23d2e5 100644 --- a/language-server/dm/executionManager.ml +++ b/language-server/dm/executionManager.ml @@ -19,6 +19,8 @@ open Types let Log log = Log.mk_log "executionManager" +type feedback_message = Feedback.level * Loc.t option * Quickfix.t list * Pp.t + type execution_status = | Success of Vernacstate.t option | Error of Pp.t Loc.located * Quickfix.t list option * Vernacstate.t option (* State to use for resiliency *) @@ -30,8 +32,6 @@ type sentence_id = Stateid.t module SM = Map.Make (Stateid) -type feedback_message = Feedback.level * Loc.t option * Pp.t - type sentence_state = | Done of execution_status | Delegated of DelegationManager.job_handle * (execution_status -> unit) option @@ -73,7 +73,7 @@ type state = { (* ugly stuff to correctly dispatch Coq feedback *) doc_id : document_id; (* unique number used to interface with Coq's Feedback *) coq_feeder : coq_feedback_listener; - sel_feedback_queue : (Feedback.route_id * sentence_id * (Feedback.level * Loc.t option * Pp.t)) Queue.t; + sel_feedback_queue : (Feedback.route_id * sentence_id * feedback_message) Queue.t; sel_cancellation_handle : Sel.Event.cancellation_handle; overview: exec_overview; } @@ -113,7 +113,7 @@ type prepared_task = module ProofJob = struct type update_request = | UpdateExecStatus of sentence_id * execution_status - | AppendFeedback of Feedback.route_id * Types.sentence_id * (Feedback.level * Loc.t option * Pp.t) + | AppendFeedback of Feedback.route_id * Types.sentence_id * (Feedback.level * Loc.t option * Quickfix.t list * Pp.t) let appendFeedback (rid,sid) fb = AppendFeedback(rid,sid,fb) type t = { @@ -131,7 +131,7 @@ end module ProofWorker = DelegationManager.MakeWorker(ProofJob) type event = - | LocalFeedback of (Feedback.route_id * sentence_id * (Feedback.level * Loc.t option * Pp.t)) Queue.t * Feedback.route_id * sentence_id * (Feedback.level * Loc.t option * Pp.t) + | LocalFeedback of (Feedback.route_id * sentence_id * (Feedback.level * Loc.t option * Quickfix.t list * Pp.t)) Queue.t * Feedback.route_id * sentence_id * (Feedback.level * Loc.t option * Quickfix.t list * Pp.t) | ProofWorkerEvent of ProofWorker.delegation type events = event Sel.Event.t list let pr_event = function @@ -191,9 +191,9 @@ let interp_ast ~doc_id ~state_id ~st ~error_recovery ast = log @@ "Failed to execute: " ^ Stateid.to_string state_id ^ " " ^ (Pp.string_of_ppcmds @@ Ppvernac.pr_vernac ast); *) let loc = Loc.get_loc info in - let qf = Quickfix.get_qf info in + let qf = Result.value ~default:[] @@ Quickfix.from_exception e in let msg = CErrors.iprint (e, info) in - let status = error loc qf msg st in + let status = error loc (Some qf) msg st in let st = interp_error_recovery error_recovery st in st, status, [] @@ -457,8 +457,8 @@ let local_feedback feedback_queue : event Sel.Event.t = Sel.On.queue ~name:"feedback" ~priority:PriorityManager.feedback feedback_queue (fun (rid,sid,msg) -> LocalFeedback(feedback_queue,rid,sid,msg)) let install_feedback_listener doc_id send = - Log.feedback_add_feeder_on_Message (fun route span doc lvl loc _ msg -> - if lvl != Feedback.Debug && doc = doc_id then send (route,span,(lvl,loc,msg))) + Log.feedback_add_feeder_on_Message (fun route span doc lvl loc qf msg -> + if lvl != Feedback.Debug && doc = doc_id then send (route,span,(lvl,loc, qf, msg))) let init vernac_state = let doc_id = fresh_doc_id () in @@ -486,8 +486,8 @@ let feedback_cleanup { coq_feeder; sel_feedback_queue; sel_cancellation_handle } let handle_feedback id fb state = match fb with - | (Feedback.Info, _, _) -> state - | (_, _, msg) -> + | (Feedback.Info, _, _, _) -> state + | (_, _, _, msg) -> begin match SM.find id state.of_sentence with | (s,fl) -> update_all id s (fb::fl) state | exception Not_found -> @@ -602,9 +602,9 @@ let worker_ensure_proof_is_over vs send_back terminator_id = with e -> let e, info = Exninfo.capture e in let loc = Loc.get_loc info in - let qf = Quickfix.get_qf info in + let qf = Result.value ~default:[] @@ Quickfix.from_exception e in let msg = CErrors.iprint (e, info) in - let status = error loc qf msg vs in + let status = error loc (Some qf) msg vs in send_back (ProofJob.UpdateExecStatus (terminator_id,status)) let worker_main { ProofJob.tasks; initial_vernac_state = vs; doc_id; terminator_id } ~send_back = @@ -752,12 +752,12 @@ let shift_diagnostics_locs st ~start ~offset = else if loc_stop > start then Loc.shift_loc 0 offset loc else loc in - let shift_feedback (level, oloc, msg as feedback) = + let shift_feedback (level, oloc, qf, msg as feedback) = match oloc with | None -> feedback | Some loc -> let loc' = shift_loc loc in - if loc' == loc then feedback else (level, Some loc', msg) + if loc' == loc then feedback else (level, Some loc', qf, msg) in let shift_error (sentence_state, feedbacks as orig) = let sentence_state' = match sentence_state with diff --git a/language-server/dm/executionManager.mli b/language-server/dm/executionManager.mli index 6be32d6e4..67842673c 100644 --- a/language-server/dm/executionManager.mli +++ b/language-server/dm/executionManager.mli @@ -37,7 +37,7 @@ type state type event type events = event Sel.Event.t list -type feedback_message = Feedback.level * Loc.t option * Pp.t +type feedback_message = Feedback.level * Loc.t option * Quickfix.t list * Pp.t val pr_event : event -> Pp.t diff --git a/language-server/dm/parTactic.ml b/language-server/dm/parTactic.ml index 169e62bc7..8dbb0cf8f 100644 --- a/language-server/dm/parTactic.ml +++ b/language-server/dm/parTactic.ml @@ -25,7 +25,7 @@ module TacticJob = struct | Error of Pp.t type update_request = | UpdateSolution of Evar.t * solution - | AppendFeedback of Feedback.route_id * sentence_id * (Feedback.level * Loc.t option * Pp.t) + | AppendFeedback of Feedback.route_id * sentence_id * (Feedback.level * Loc.t option * Quickfix.t list * Pp.t) let appendFeedback (rid,id) fb = AppendFeedback(rid,id,fb) type t = { diff --git a/language-server/protocol/lspWrapper.ml b/language-server/protocol/lspWrapper.ml index c15af6c36..d642f62da 100644 --- a/language-server/protocol/lspWrapper.ml +++ b/language-server/protocol/lspWrapper.ml @@ -79,7 +79,7 @@ module DiagnosticSeverity = struct let of_feedback_level = let open DiagnosticSeverity in function | Feedback.Error -> Error - | Feedback.Warning _ -> Warning + | Feedback.Warning -> Warning | Feedback.(Info | Debug | Notice) -> Information end @@ -101,7 +101,7 @@ module FeedbackChannel = struct | Feedback.Debug -> Some Debug | Feedback.Info -> Some Info | Feedback.Notice -> Some Notice - | Feedback.(Error | Warning _) -> None + | Feedback.(Error | Warning) -> None end