Merge pull request #512 from coq-community/unvendor-sel

depend on sel 0.4.0

flake.nix

@@ -57,6 +57,7 @@
           sexplib
           ppx_yojson_conv
           lsp
+          sel
         ]);
       };
 

language-server/dm/delegationManager.ml

@@ -80,7 +80,7 @@ module type Worker = sig
   (** Event for the main loop *)
   type delegation
   val pr_event : delegation -> Pp.t
-  type events = delegation Sel.event list
+  type events = delegation Sel.Event.t list
 
   (** handling an event may require an update to a sentence in the exec state,
       e.g. when a feedback is received *)
@@ -91,10 +91,10 @@ module type Worker = sig
       - if we can fork, job is passed to fork_action
       - otherwise Job.binary_name is spawn and the job sent to it *)
   val worker_available :
-    jobs:((job_handle * Sel.cancellation_handle * job_t) Queue.t) ->
+    jobs:((job_handle * Sel.Event.cancellation_handle * job_t) Queue.t) ->
     fork_action:(job_t -> send_back:(job_update_request -> unit) -> unit) ->
     feedback_cleanup:(unit -> unit) ->
-    delegation Sel.event * Sel.cancellation_handle
+    delegation Sel.Event.t
 
   (* for worker toplevels *)
   type options
@@ -139,7 +139,7 @@ let install_debug_worker link =
   Log.worker_initialization_done
     ~fwd_event:(fun e -> write_value link (DebugMessage e))
 
-type events = delegation Sel.event list
+type events = delegation Sel.Event.t list
 
 type role = Master | Worker of link
 
@@ -161,21 +161,19 @@ let resize_pool new_pool_size =
 ;;
 
 (* In order to create a job we enqueue this event *)
-let worker_available ~jobs ~fork_action ~feedback_cleanup : delegation Sel.event * Sel.cancellation_handle =
-  Sel.on_queues jobs pool (fun (job_handle, _, job) () ->
+let worker_available ~jobs ~fork_action ~feedback_cleanup : delegation Sel.Event.t =
+  Sel.On.queues jobs pool (fun (job_handle, _, job) () ->
     WorkerStart (feedback_cleanup,job_handle,job,fork_action,Job.binary_name))
 
 (* When a worker is spawn, we enqueue this event, since eventually it will die *)
-let worker_ends pid : delegation Sel.event =
-  Sel.on_death_of ~pid (fun reason -> WorkerEnd(pid,reason))
-  |> Sel.uncancellable
+let worker_ends pid : delegation Sel.Event.t =
+  Sel.On.death_of ~pid (fun reason -> WorkerEnd(pid,reason))
 
 (* When a worker is spawn, we enqueue this event, since eventually will make progress *)
-let worker_progress link : delegation Sel.event =
-  Sel.on_ocaml_value link.read_from (function
+let worker_progress link : delegation Sel.Event.t =
+  Sel.On.ocaml_value link.read_from (function
     | Error e -> WorkerIOError e
     | Ok update_request -> WorkerProgress { link; update_request; })
-  |> Sel.uncancellable
 
 (* ************ spawning *************************************************** *)
 
@@ -326,7 +324,7 @@ let setup_plumbing port =
     let write_to = chan in
     let link = { read_from; write_to } in
     (* Unix.read_value does not exist, we use Sel *)
-    match Sel.(pop (enqueue empty [Sel.on_ocaml_value read_from (fun x -> x) |> Sel.uncancellable])) with
+    match Sel.(pop Todo.(add empty [Sel.On.ocaml_value read_from (fun x -> x)])) with
     | Ok (job : Job.t), _ -> (write_value link, job)
     | Error exn, _ ->
       log_worker @@ "error receiving job: " ^ Printexc.to_string exn;

language-server/dm/delegationManager.mli

@@ -61,7 +61,7 @@ module type Worker = sig
    (** Event for the main loop *)
    type delegation
    val pr_event : delegation -> Pp.t
-   type events = delegation Sel.event list
+   type events = delegation Sel.Event.t list
 
    (** handling an event may require an update to a sentence in the exec state,
        e.g. when a feedback is received *)
@@ -72,10 +72,10 @@ module type Worker = sig
       - if we can fork, job is passed to fork_action
       - otherwise Job.binary_name is spawn and the job sent to it *)
    val worker_available :
-     jobs:((job_handle * Sel.cancellation_handle * job_t) Queue.t) ->
+     jobs:((job_handle * Sel.Event.cancellation_handle * job_t) Queue.t) ->
      fork_action:(job_t -> send_back:(job_update_request -> unit) -> unit) ->
      feedback_cleanup:(unit -> unit) ->
-     delegation Sel.event * Sel.cancellation_handle
+     delegation Sel.Event.t
 
    (* for worker toplevels *)
    type options

language-server/dm/documentManager.ml

@@ -45,10 +45,10 @@ let pp_event fmt = function
       Stdlib.Format.fprintf fmt "ExecuteToLoc %d (%d tasks left, started %2.3f ago)" (Stateid.to_int id) (List.length todo) time
   | ExecutionManagerEvent _ -> Stdlib.Format.fprintf fmt "ExecutionManagerEvent"
 
-let inject_em_event x = Sel.map (fun e -> ExecutionManagerEvent e) x
+let inject_em_event x = Sel.Event.map (fun e -> ExecutionManagerEvent e) x
 let inject_em_events events = List.map inject_em_event events
 
-type events = event Sel.event list
+type events = event Sel.Event.t list
 
 type exec_overview = {
   parsed : Range.t list;
@@ -172,7 +172,7 @@ let reset { uri; opts; init_vs; document; execution_state } =
   let execution_state, feedback = ExecutionManager.init init_vs in
   { uri; opts; init_vs; document; execution_state; observe_id = None }, [inject_em_event feedback]
 
-let interpret_to ~stateful ~background state id : (state * event Sel.event list) =
+let interpret_to ~stateful ~background state id : (state * event Sel.Event.t list) =
   match Document.get_sentence state.document id with
   | None -> (state, []) (* TODO error? *)
   | Some { id } ->
@@ -181,8 +181,8 @@ let interpret_to ~stateful ~background state id : (state * event Sel.event list)
     if CList.is_empty todo then
       (state, [])
     else
-      let event = Sel.now (Execute {id; vst_for_next_todo; todo; started = Unix.gettimeofday (); background }) in
-      let event = if background then event else Sel.set_priority PriorityManager.execution event in
+      let priority = if background then None else Some PriorityManager.execution in
+      let event = Sel.now ?priority (Execute {id; vst_for_next_todo; todo; started = Unix.gettimeofday (); background }) in
       (state, [ event ])
 
 let interpret_to_position ~stateful st pos =
@@ -276,8 +276,8 @@ let handle_event ev st =
       ExecutionManager.execute st.execution_state (vst_for_next_todo, [], false) task in
     (* We do not update the state here because we may have received feedback while
        executing *)
-    let event = Sel.now (Execute {id; vst_for_next_todo; todo; started; background }) in
-    let event = if background then event else Sel.set_priority PriorityManager.execution @@ event in
+    let priority = if background then None else Some PriorityManager.execution in
+    let event = Sel.now ?priority (Execute {id; vst_for_next_todo; todo; started; background }) in
     (Some {st with execution_state}, inject_em_events events @ [event])
   | ExecutionManagerEvent ev ->
     let execution_state_update, events = ExecutionManager.handle_event ev st.execution_state in

language-server/dm/documentManager.mli

@@ -28,7 +28,7 @@ type state
 type event
 val pp_event : Format.formatter -> event -> unit
 
-type events = event Sel.event list
+type events = event Sel.Event.t list
 
 val init : Vernacstate.t -> opts:Coqargs.injection_command list -> DocumentUri.t -> text:string -> state * events
 (** [init st opts uri text] initializes the document manager with initial vernac state
@@ -92,7 +92,7 @@ val get_completions : state -> Position.t -> (completion_item list, string) Resu
 val handle_event : event -> state -> (state option * events)
 (** handles events and returns a new state if it was updated *)
 
-val search : state -> id:string -> Position.t -> string -> notification Sel.event list
+val search : state -> id:string -> Position.t -> string -> notification Sel.Event.t list
 
 val about : state -> Position.t -> pattern:string -> (string,string) Result.t
 

language-server/dm/executionManager.ml

@@ -73,7 +73,7 @@ type state = {
   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_cancellation_handle : Sel.cancellation_handle;
+  sel_cancellation_handle : Sel.Event.cancellation_handle;
 }
 
 let options = ref default_options
@@ -116,14 +116,14 @@ end
 module ProofWorker = DelegationManager.MakeWorker(ProofJob)
 
 type event =
-  | LocalFeedback of Feedback.route_id * sentence_id * (Feedback.level * Loc.t option * Pp.t)
+  | 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)
   | ProofWorkerEvent of ProofWorker.delegation
-type events = event Sel.event list
+type events = event Sel.Event.t list
 let pr_event = function
   | LocalFeedback _ -> Pp.str "LocalFeedback"
   | ProofWorkerEvent event -> ProofWorker.pr_event event
 
-let inject_proof_event = Sel.map (fun x -> ProofWorkerEvent x)
+let inject_proof_event = Sel.Event.map (fun x -> ProofWorkerEvent x)
 let inject_proof_events st l =
   (st, List.map inject_proof_event l)
 
@@ -221,12 +221,8 @@ let update state id v =
   update_all id (Done v) fl state
 ;;
 
-let local_feedback feedback_queue : event Sel.event * Sel.cancellation_handle =
-  let e, c = Sel.on_queue feedback_queue (fun (rid,sid,msg) -> LocalFeedback(rid,sid,msg)) in
-  e |> Sel.name "feedback"
-    |> Sel.make_recurring
-    |> Sel.set_priority PriorityManager.feedback,
-  c
+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 =
   let open Feedback in
@@ -239,7 +235,8 @@ let init vernac_state =
   let doc_id = fresh_doc_id () in
   let sel_feedback_queue = Queue.create () in
   let coq_feeder = install_feedback_listener doc_id (fun x -> Queue.push x sel_feedback_queue) in
-  let event, sel_cancellation_handle = local_feedback sel_feedback_queue in
+  let event = local_feedback sel_feedback_queue in
+  let sel_cancellation_handle = Sel.Event.get_cancellation_handle event in
   {
     initial = vernac_state;
     of_sentence = SM.empty;
@@ -255,7 +252,7 @@ let init vernac_state =
 let feedback_cleanup { coq_feeder; sel_feedback_queue; sel_cancellation_handle } =
   Feedback.del_feeder coq_feeder;
   Queue.clear sel_feedback_queue;
-  Sel.cancel sel_cancellation_handle
+  Sel.Event.cancel sel_cancellation_handle
 
 let handle_feedback id fb state =
   match fb with
@@ -270,8 +267,8 @@ let handle_feedback id fb state =
 
 let handle_event event state =
   match event with
-  | LocalFeedback (_,id,fb) ->
-      Some (handle_feedback id fb state), []
+  | LocalFeedback (q,_,id,fb) ->
+      Some (handle_feedback id fb state), [local_feedback q]
   | ProofWorkerEvent event ->
       let update, events = ProofWorker.handle_event event in
       let state =
@@ -302,12 +299,12 @@ let find_fulfilled_opt x m =
     | Delegated _ -> None
   with Not_found -> None
 
-let jobs : (DelegationManager.job_handle * Sel.cancellation_handle * ProofJob.t) Queue.t = Queue.create ()
+let jobs : (DelegationManager.job_handle * Sel.Event.cancellation_handle * ProofJob.t) Queue.t = Queue.create ()
 
 (* TODO: kill all Delegated... *)
 let destroy st =
   feedback_cleanup st;
-  Queue.iter (fun (h,c,_) -> DelegationManager.cancel_job h; Sel.cancel c) jobs
+  Queue.iter (fun (h,c,_) -> DelegationManager.cancel_job h; Sel.Event.cancel c) jobs
 
 
 let last_opt l = try Some (CList.last l).id with Failure _ -> None
@@ -447,12 +444,12 @@ let execute st (vs, events, interrupted) task =
                else
                  update_all id (Delegated (job_id,None)) [] st)
                st (List.map id_of_prepared_task tasks) in
-            let e, cancellation =
+            let e =
                 ProofWorker.worker_available ~jobs
                   ~fork_action:worker_main
                   ~feedback_cleanup:(fun () -> feedback_cleanup st)
                 in
-              Queue.push (job_id, cancellation, job) jobs;
+              Queue.push (job_id, Sel.Event.get_cancellation_handle e, job) jobs;
               (st, last_vs,events @ [inject_proof_event e] ,false)
           | _ ->
             (* If executing the proof opener failed, we skip the proof *)
@@ -564,7 +561,7 @@ let rec invalidate schedule id st =
     if terminator_id != id then
       Queue.push job jobs
     else begin
-      Sel.cancel cancellation;
+      Sel.Event.cancel cancellation;
       removed := tasks :: !removed
     end) old_jobs;
   let of_sentence = List.fold_left invalidate1 of_sentence

language-server/dm/executionManager.mli

@@ -35,10 +35,10 @@ val is_diagnostics_enabled: unit -> bool
 (** Execution state, includes the cache *)
 type state
 type event
-type events = event Sel.event list
+type events = event Sel.Event.t list
 val pr_event : event -> Pp.t
 
-val init : Vernacstate.t -> state * event Sel.event
+val init : Vernacstate.t -> state * event Sel.Event.t
 val destroy : state -> unit
 
 val get_options : unit -> options

language-server/dm/log.ml

@@ -64,7 +64,7 @@ let mk_log name =
 let logs () = List.sort String.compare !logs
 
 type event = string
-type events = event Sel.event list
+type events = event Sel.Event.t list
 
 let install_debug_feedback f =
   Feedback.add_feeder (fun fb ->
@@ -77,13 +77,9 @@ let install_debug_feedback f =
 let coq_debug_feedback_queue = Queue.create ()
 let main_debug_feeder = install_debug_feedback (fun txt -> Queue.push txt coq_debug_feedback_queue)
 
-let (debug, cancel_debug_event) : event Sel.event * Sel.cancellation_handle =
-  Sel.on_queue coq_debug_feedback_queue (fun x -> x) |>
-  fun (e, cancellation) ->
-    (e |> Sel.name "debug"
-       |> Sel.make_recurring
-       |> Sel.set_priority PriorityManager.feedback),
-    cancellation
+let debug : event Sel.Event.t =
+  Sel.On.queue ~name:"debug" ~priority:PriorityManager.feedback coq_debug_feedback_queue (fun x -> x)
+let cancel_debug_event = Sel.Event.get_cancellation_handle debug
 
 let lsp_initialization_done () =
   lsp_initialization_done := true;
@@ -93,7 +89,7 @@ let lsp_initialization_done () =
   [debug]
 
 let worker_initialization_begins () =
-  Sel.cancel cancel_debug_event;
+  Sel.Event.cancel cancel_debug_event;
   Feedback.del_feeder main_debug_feeder;
     (* We do not want to inherit master's Feedback reader (feeder), otherwise we
     would output on the worker's stderr.

language-server/dm/log.mli

@@ -18,7 +18,7 @@ val mk_log : string -> (string -> unit) log
 val logs : unit -> string list
 
 type event
-type events = event Sel.event list
+type events = event Sel.Event.t list
 
 val lsp_initialization_done : unit -> events
 val handle_event : event -> unit

language-server/dm/parTactic.ml

@@ -104,22 +104,22 @@ let interp_par ~pstate ~info ast ~abstract ~with_end_tac : Declare.Proof.t =
      (Proof.data p).Proof.goals |> CList.map_i (fun goalno goal ->
        let job = { TacticJob.state; ast; goalno = goalno + 1; goal; name = string_of_int (Evar.repr goal)} in
        let job_id = DelegationManager.mk_job_handle !feedback_id in
-       let e, cancellation =
+       let e =
          TacticWorker.worker_available ~feedback_cleanup:(fun _ -> ()) (* not really correct, since there is a cleanup to be done, but it concern a sel loop which is dead (we don't come back to it), so we can ignore the problem *)
            ~jobs:queue ~fork_action:worker_solve_one_goal in
-       Queue.push (job_id, cancellation, job) queue;
+       Queue.push (job_id, Sel.Event.get_cancellation_handle e, job) queue;
         e, job_id
       ) 0) in
   let rec wait acc evs =
-    log @@ "waiting for events: " ^ string_of_int @@ Sel.size evs;
+    log @@ "waiting for events: " ^ string_of_int @@ Sel.Todo.size evs;
     let more_ready, evs = Sel.pop_opt evs in
     match more_ready with
     | None ->
-        if Sel.nothing_left_to_do evs then (log @@ "done waiting for tactic workers"; acc)
+        if Sel.Todo.is_empty evs then (log @@ "done waiting for tactic workers"; acc)
         else wait acc evs (* should be assert false *)
     | Some ev ->
       let result, more_events = TacticWorker.handle_event ev in
-      let evs = Sel.enqueue evs more_events in
+      let evs = Sel.Todo.add evs more_events in
       match result with
       | None -> wait acc evs
       | Some(TacticJob.UpdateSolution(ev,TacticJob.Solved(c,u))) ->
@@ -135,7 +135,7 @@ let interp_par ~pstate ~info ast ~abstract ~with_end_tac : Declare.Proof.t =
           log @@ "got error for " ^ Pp.string_of_ppcmds @@ Evar.print ev;
           List.iter DelegationManager.cancel_job job_ids;
           CErrors.user_err err in
-  let results = wait [] Sel.(enqueue empty events) in
+  let results = wait [] Sel.Todo.(add empty events) in
   Declare.Proof.map pstate ~f:(fun p ->
     let p,_,() = Proof.run_tactic (Global.env()) (assign_tac ~abstract results) p in
     p)

language-server/dm/searchQuery.ml

@@ -20,9 +20,8 @@ open Pp
 vscoq process, which does not allow for real asynchronous processing of results. *)
 let query_results_queue = Queue.create ()
 
-let query_feedback : notification Sel.event =
-  Sel.on_queue query_results_queue (fun x -> QueryResultNotification x)
-  |> Sel.uncancellable
+let query_feedback : notification Sel.Event.t =
+  Sel.On.queue query_results_queue (fun x -> QueryResultNotification x)
 
 (* TODO : remove these two functions when interp_search_restriction is 
   added in the comSearch.mli in Coq (they're simply copied here for now) *)

language-server/dm/searchQuery.mli

@@ -13,12 +13,12 @@
 (**************************************************************************)
 open Protocol.LspWrapper
 
-val query_feedback : notification Sel.event
+val query_feedback : notification Sel.Event.t
 
 val interp_search :
   id:string ->
   Environ.env ->
   Evd.evar_map ->
   (bool * Vernacexpr.search_request) list ->
   Vernacexpr.search_restriction ->
-  notification Sel.event list
+  notification Sel.Event.t list