From f6a4cb10eb838fccfe45ad3c4f3379b575ec98a8 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 12 Feb 2025 16:10:17 +0100 Subject: [PATCH 1/2] process feedback in batches (fix #878) --- language-server/dm/executionManager.ml | 16 ++++++++-------- language-server/vscoq-language-server.opam | 2 +- 2 files changed, 9 insertions(+), 9 deletions(-) diff --git a/language-server/dm/executionManager.ml b/language-server/dm/executionManager.ml index 8374f4ae..7379df46 100644 --- a/language-server/dm/executionManager.ml +++ b/language-server/dm/executionManager.ml @@ -141,7 +141,7 @@ end module ProofWorker = DelegationManager.MakeWorker(ProofJob) type event = - | 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) + | LocalFeedback of (Feedback.route_id * sentence_id * feedback_message) Queue.t * (Feedback.route_id * sentence_id * feedback_message) list | ProofWorkerEvent of ProofWorker.delegation type events = event Sel.Event.t list @@ -419,7 +419,7 @@ let update state id v = ;; 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)) + Sel.On.queue_all ~name:"feedback" ~priority:PriorityManager.feedback feedback_queue (fun x xs -> LocalFeedback(feedback_queue, x :: xs)) let install_feedback_listener doc_id send = Log.feedback_add_feeder_on_Message (fun route span doc lvl loc qf msg -> @@ -450,7 +450,7 @@ let feedback_cleanup { coq_feeder; sel_feedback_queue; sel_cancellation_handle } Queue.clear sel_feedback_queue; Sel.Event.cancel sel_cancellation_handle -let handle_feedback id fb state = +let handle_feedback state (_,id, fb) = match fb with | (_, _, _, msg) -> begin match SM.find id state.of_sentence with @@ -458,19 +458,19 @@ let handle_feedback id fb state = | exception Not_found -> log @@ "Received feedback on non-existing state id " ^ Stateid.to_string id ^ ": " ^ Pp.string_of_ppcmds msg; state - end + end let handle_event event state = match event with - | LocalFeedback (q,_,id,fb) -> - None, Some (handle_feedback id fb state), [local_feedback q] + | LocalFeedback (q,l) -> + None, Some (List.fold_left handle_feedback state l), [local_feedback q] | ProofWorkerEvent event -> let update, events = ProofWorker.handle_event event in let state, id = match update with | None -> None, None - | Some (ProofJob.AppendFeedback(_,id,fb)) -> - Some (handle_feedback id fb state), None + | Some (ProofJob.AppendFeedback(x,id,fb)) -> + Some (handle_feedback state (x,id,fb)), None | Some (ProofJob.UpdateExecStatus(id,v)) -> match SM.find id state.of_sentence, v with | (Delegated (_,completion), fl), _ -> diff --git a/language-server/vscoq-language-server.opam b/language-server/vscoq-language-server.opam index 46f09b35..b94178e9 100644 --- a/language-server/vscoq-language-server.opam +++ b/language-server/vscoq-language-server.opam @@ -28,7 +28,7 @@ depends: [ "ppx_optcomp" "result" { >= "1.5" } "lsp" { >= "1.15"} - "sel" {>= "0.4.0"} + "sel" {>= "0.6.0"} ] synopsis: "VSCoq language server" available: arch != "arm32" & arch != "x86_32" From 22fae6a4b4a0e44bb4e8a703ce42fb70be0920a0 Mon Sep 17 00:00:00 2001 From: Romain Tetley Date: Thu, 13 Feb 2025 16:23:20 +0100 Subject: [PATCH 2/2] fix: update flake pin --- flake.nix | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/flake.nix b/flake.nix index a293c449..9ddf404b 100644 --- a/flake.nix +++ b/flake.nix @@ -3,7 +3,7 @@ inputs = { flake-utils.url = "github:numtide/flake-utils"; - nixpkgs.url = "github:NixOS/nixpkgs?rev=4221c236f296269b5b2e2a6b733ebcd4a2e05f90"; + nixpkgs.url = "github:NixOS/nixpkgs?rev=4316480afd67ac44699314c127fdce2dea1d9937"; rocq-master = { url = "github:coq/coq/9d13cf5137c82610893241ac3c5c756f01c2aaa1"; }; # Should be kept in sync with PIN_COQ in CI workflow rocq-master.inputs.nixpkgs.follows = "nixpkgs";