Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

process feedback in batches (fix #878) #1033

Open
wants to merge 2 commits into
base: main
Choose a base branch
from
Open

process feedback in batches (fix #878) #1033

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
f6a4cb1
process feedback in batches (fix #878)
gares Feb 12, 2025
22fae6a
fix: update flake pin
rtetley Feb 13, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion flake.nix
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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";
Expand Down
16 changes: 8 additions & 8 deletions language-server/dm/executionManager.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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 ->
Expand Down Expand Up @@ -450,27 +450,27 @@ 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
| (s,fl) -> update_all id s (fl @ [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), _ ->
Expand Down
2 changes: 1 addition & 1 deletion language-server/vscoq-language-server.opam
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down
Loading