wip: coq interruption

client/package.json

@@ -415,6 +415,12 @@
         "category": "Coq",
         "icon": "$(expand-all)",
         "enablement": "vscoq.hasSearchResults"
+      },
+      {
+        "command": "extension.coq.interrupt",
+        "title": "Interrupt",
+        "category": "Coq",
+        "icon": "$(stop-circle)"
       }
     ],
     "menus": {
@@ -424,6 +430,11 @@
           "command": "extension.coq.interpretToPoint",
           "group": "navigation@3"
         },
+        {
+          "when": "resourceLangId == coq && config.vscoq.proof.display-buttons == true",
+          "command": "extension.coq.interrupt",
+          "group": "navigation@1"
+        },
         {
           "when": "resourceLangId == coq && config.vscoq.proof.display-buttons == true",
           "command": "extension.coq.stepForward",

client/src/extension.ts

@@ -40,7 +40,8 @@ import {
     sendInterpretToPoint,
     sendInterpretToEnd,
     sendStepForward,
-    sendStepBackward
+    sendStepBackward,
+    sendInterrupt
 } from './manualChecking';
 import { 
     makeVersionedDocumentId,
@@ -207,6 +208,7 @@ export function activate(context: ExtensionContext) {
         registerVscoqTextCommand('addQueryTab', () => searchProvider.addTab());
         registerVscoqTextCommand('collapseAllQueries', () => searchProvider.collapseAll());
         registerVscoqTextCommand('expandAllQueries', () => searchProvider.expandAll());
+        registerVscoqTextCommand('interrupt', (editor) => sendInterrupt(editor, client));
         registerVscoqTextCommand('interpretToPoint', (editor) => sendInterpretToPoint(editor, client));
         registerVscoqTextCommand('interpretToEnd', (editor) => sendInterpretToEnd(editor, client));
         registerVscoqTextCommand('stepForward', (editor) => sendStepForward(editor, client));

client/src/manualChecking.ts

@@ -1,19 +1,15 @@
 import {
     TextEditor,
-    commands,
-    workspace
 } from 'vscode';
 
-import {
-    RequestType,
-    VersionedTextDocumentIdentifier,
-} from 'vscode-languageclient/node';
-
-import GoalPanel from './panels/GoalPanel';
-
 import Client from './client';
 import { makeVersionedDocumentId } from './utilities/utils';
 
+export const sendInterrupt = (editor: TextEditor, client: Client) => {
+    const textDocument = makeVersionedDocumentId(editor);
+    client.sendNotification("vscoq/interrupt", {textDocument});
+};
+
 export const sendInterpretToPoint = (editor: TextEditor, client: Client) => {
     const textDocument = makeVersionedDocumentId(editor);
     const position = editor.selection.active;

language-server/dm/documentManager.ml

@@ -48,6 +48,7 @@ type state = {
   execution_state : ExecutionManager.state;
   observe_id : observe_id;
   cancel_handle : Sel.Event.cancellation_handle option;
+  kill_handle : ExecutionManager.cancellation_handle option;
   document_state: document_state;
 }
 
@@ -60,6 +61,15 @@ type event =
       task : ExecutionManager.prepared_task;
       started : float; (* time *)
     }
+  | ExecutePromise of {
+    id : Types.sentence_id;
+    started : float;
+    result : ExecutionManager.exec_result Sel.Promise.state;
+    (* ugly *)
+    background: bool;
+    block: bool;
+    proof_view_event : event Sel.Event.t list;
+  }
   | ExecutionManagerEvent of ExecutionManager.event
   | ParseEvent
   | Observe of Types.sentence_id
@@ -78,7 +88,9 @@ type handled_event = {
 let pp_event fmt = function
   | Execute { id; started; _ } ->
       let time = Unix.gettimeofday () -. started in 
-      Stdlib.Format.fprintf fmt "ExecuteToLoc %d (started %2.3f ago)" (Stateid.to_int id) time
+      Stdlib.Format.fprintf fmt "Execute %d (started %2.3f ago)" (Stateid.to_int id) time
+  | ExecutePromise { id; _ } ->
+      Stdlib.Format.fprintf fmt "ExecutePromise %d" (Stateid.to_int id)
   | ExecutionManagerEvent _ -> Stdlib.Format.fprintf fmt "ExecutionManagerEvent"
   | ParseEvent ->
     Stdlib.Format.fprintf fmt "ParseEvent"
@@ -294,6 +306,10 @@ let create_execution_event background event =
   let priority = if background then None else Some PriorityManager.execution in
   Sel.now ?priority event
 
+let create_execution_promise_event id started background block proof_view_event p =
+  let priority = if background then None else Some (-100) in
+  Sel.On.promise ?priority p (fun result -> ExecutePromise { result; id; started; background; block; proof_view_event; })
+
 let state_before_error state error_id loc =
   match Document.get_sentence state.document error_id with
   | None -> state, None
@@ -309,11 +325,15 @@ let state_before_error state error_id loc =
       let observe_id = (Id id) in
       {state with observe_id}, Some error_range
 
+let cancel_ongoing_execution state =
+  Option.iter Sel.Event.cancel state.cancel_handle;
+  Option.iter ExecutionManager.cancel state.kill_handle
+
 let observe ~background state id ~should_block_on_error : (state * event Sel.Event.t list) =
   match Document.get_sentence state.document id with
   | None -> state, [] (* TODO error? *)
   | Some { id } ->
-    Option.iter Sel.Event.cancel state.cancel_handle;
+    cancel_ongoing_execution state;
     let vst_for_next_todo, execution_state, task, error_id = ExecutionManager.build_tasks_for state.document (Document.schedule state.document) state.execution_state id should_block_on_error in
     match task with
     | Some task -> (* task will only be Some if there is no error *)
@@ -511,7 +531,7 @@ let init init_vs ~opts uri ~text =
   let init_vs = Vernacstate.freeze_full_state () in
   let document = Document.create_document init_vs.Vernacstate.synterp text in
   let execution_state, feedback = ExecutionManager.init init_vs in
-  let state = { uri; opts; init_vs; document; execution_state; observe_id=Top; cancel_handle = None; document_state = Parsing } in
+  let state = { uri; opts; init_vs; document; execution_state; observe_id=Top; cancel_handle = None; kill_handle = None; document_state = Parsing } in
   let priority = Some PriorityManager.launch_parsing in
   let event = Sel.now ?priority ParseEvent in
   state, [event] @ [inject_em_event feedback]
@@ -523,7 +543,7 @@ let reset { uri; opts; init_vs; document; execution_state; } =
   ExecutionManager.destroy execution_state;
   let execution_state, feedback = ExecutionManager.init init_vs in
   let observe_id = Top in
-  let state = { uri; opts; init_vs; document; execution_state; observe_id; cancel_handle = None ; document_state = Parsing } in
+  let state = { uri; opts; init_vs; document; execution_state; observe_id; cancel_handle = None ; kill_handle = None; document_state = Parsing } in
   let priority = Some PriorityManager.launch_parsing in
   let event = Sel.now ?priority ParseEvent in
   state, [event] @ [inject_em_event feedback]
@@ -553,6 +573,8 @@ let execution_finished st id started =
   {state; events=[]; update_view; notification=None}
 
 let execute st id vst_for_next_todo started task background block =
+  (* block until any ongoing Coq computation is over *)
+  Option.iter ExecutionManager.cancel st.kill_handle;
   let time = Unix.gettimeofday () -. started in
   let proof_view_event = (*When in continuous mode we always check if we should update the goal view *)
     if background then begin
@@ -573,8 +595,14 @@ let execute st id vst_for_next_todo started task background block =
     {state=Some st; events=[]; update_view=true; notification=None} (* Sentences have been invalidate, probably because the user edited while executing *)
   | Some _ ->
     log (fun () -> Printf.sprintf "ExecuteToLoc %d continues after %2.3f" (Stateid.to_int id) time);
-    let (next, execution_state,vst_for_next_todo,events, exec_error) =
-      ExecutionManager.execute st.execution_state st.document (vst_for_next_todo, [], false) task block in
+    let interruptible = ExecutionManager.execute st.execution_state st.document (vst_for_next_todo, [], false) task block in
+    let st = { st with kill_handle = Some interruptible.kill_handle } in
+    {state=Some st; events=[create_execution_promise_event id started background block proof_view_event interruptible.promise]; update_view=true; notification=None}
+
+let post_execute st id started background block proof_view_event promise =
+  match promise with
+  | Sel.Promise.Rejected e -> assert false (* TODO, an error escaped *)
+  | Sel.Promise.Fulfilled (next, execution_state,vst_for_next_todo,events, exec_error) ->
     let st, block_events =
       match exec_error with
       | None -> st, []
@@ -589,7 +617,7 @@ let execute st id vst_for_next_todo started task background block =
       | _ ->
         let cancel_handle = Option.map Sel.Event.get_cancellation_handle event in
         let event = Option.cata (fun event -> [event]) [] event in
-        let state = Some {st with execution_state; cancel_handle} in
+        let state = Some {st with execution_state; cancel_handle; kill_handle = None} in
         let update_view = true in
         let events = proof_view_event @ inject_em_events events @ block_events @ event in
         {state; events; update_view; notification=None}
@@ -625,6 +653,8 @@ let handle_event ev st ~block check_mode diff_mode =
   match ev with
   | Execute { id; vst_for_next_todo; started; task } ->
     execute st id vst_for_next_todo started task background block
+  | ExecutePromise { id; started; background; block; proof_view_event; result } ->
+    post_execute st id started background block proof_view_event result
   | ExecutionManagerEvent ev ->
     handle_execution_manager_event st ev
   | Observe id ->

language-server/dm/documentManager.mli

@@ -94,6 +94,9 @@ val interpret_in_background : state -> should_block_on_error:bool -> (state * ev
 val reset : state -> state * events 
 (** resets Coq *)
 
+val cancel_ongoing_execution : state -> unit
+(** [cancel_ongoing_execution st] cancels any ongoing execution on [st]*)
+
 val executed_ranges : state -> Settings.Mode.t -> exec_overview
 (** [executes_ranges doc mode] returns the ranges corresponding to the sentences
     that have been executed. [mode] allows to send a "cut" range that only goes

language-server/dm/executionManager.ml

@@ -667,7 +667,7 @@ let execute_task st (vs, events, interrupted) task =
       let st = update st (id_of_prepared_task task) (Error ((None,Pp.str "interrupted"),None,None)) in
       (st, vs, events, true, None)
 
-let execute st document (vs, events, interrupted) task block_on_first_error =
+let execute_coq st document (vs, events, interrupted) task block_on_first_error =
   let st, vst_for_next_todo, events, _, exec_error =
     execute_task st (vs, events, interrupted) task in
   match block_on_first_error, exec_error with
@@ -682,6 +682,75 @@ let execute st document (vs, events, interrupted) task block_on_first_error =
     let st = { st with todo=[]} in
     None, st, vst_for_next_todo, events, exec_error
 
+type cancellation_handle = Thread.t option
+
+type 'a interruptible = {
+  promise : 'a Sel.Promise.t;
+  kill_handle : cancellation_handle;
+}
+type exec_result = (prepared_task option * state * Vernacstate.t * events * errored_sentence) (* TODO: turn into record *)
+
+let job = ref None
+
+let job_mutex = Mutex.create ()
+let job_condition = Condition.create ()
+
+let runner = Thread.create (fun () ->
+  while true do
+    let (st, document, acc, task, block_on_first_error, resolver) =
+      Mutex.lock job_mutex;
+      while !job = None do Condition.wait job_condition job_mutex done;
+      let rc = match !job with Some x -> x | None -> assert false in
+      Condition.signal job_condition;
+      Mutex.unlock job_mutex;
+      rc
+    in
+      begin try
+        log (fun () -> Format.asprintf "begin exec: %f\n" (Unix.gettimeofday ()));
+        Sel.Promise.fulfill resolver (execute_coq st document acc task block_on_first_error);
+        log (fun () -> Format.asprintf "end exec: %f\n" (Unix.gettimeofday ()));
+      with e ->
+        log (fun () -> "rejected!");
+        Sel.Promise.reject resolver e
+      end;
+      Mutex.lock job_mutex;
+      job := None;
+      Condition.signal job_condition;
+      Mutex.unlock job_mutex;
+
+      (* Event.send chan_out () |> Event.sync *)
+  done
+) ()
+
+let cancel t =
+  Control.interrupt := true;  
+  log (fun () -> "interrupting...");
+  Mutex.lock job_mutex;
+  while !job <> None do Condition.wait job_condition job_mutex done;
+  Mutex.unlock job_mutex;
+  log (fun () -> "interrupted!");
+  Control.interrupt := false
+
+(* TODO: Sel.Promise.run *)
+let execute_thread st document acc task block_on_first_error resolver =
+  Mutex.lock job_mutex;
+  (* while !job <> None do Condition.wait job_condition job_mutex done; *)
+  job := Some (st, document, acc, task, block_on_first_error, resolver);
+  Condition.signal job_condition;
+  Mutex.unlock job_mutex;
+  None
+
+
+let execute_nothread st document acc task block_on_first_error resolver =
+  Sel.Promise.fulfill resolver (execute_coq st document acc task block_on_first_error);
+  None
+
+let execute st document acc task block_on_first_error =
+  let promise, r = Sel.Promise.make () in
+  (* log (fun () -> Format.asprintf "promise: %a" Sel.Promise.(pp (fun _ _ -> ())) promise); *)
+  let kill_handle = execute_thread st document acc task block_on_first_error r in
+  { promise; kill_handle }
+
 
 let build_tasks_for document sch st id block =
   let rec build_tasks id tasks st =

language-server/dm/executionManager.mli

@@ -75,7 +75,16 @@ val handle_event : event -> state -> (sentence_id option * state option * events
 type prepared_task
 val get_id_of_executed_task : prepared_task -> sentence_id
 val build_tasks_for : Document.document -> Scheduler.schedule -> state -> sentence_id -> bool -> Vernacstate.t * state * prepared_task option * errored_sentence
-val execute : state -> Document.document -> Vernacstate.t * events * bool -> prepared_task -> bool -> (prepared_task option * state * Vernacstate.t * events * errored_sentence)
+
+type cancellation_handle
+val cancel : cancellation_handle -> unit
+type 'a interruptible = {
+  promise : 'a Sel.Promise.t;
+  kill_handle : cancellation_handle;
+}
+type exec_result = (prepared_task option * state * Vernacstate.t * events * errored_sentence) (* TODO: turn into record *)
+(* TODO: hide the ugly type of the accumulator *)
+val execute : state -> Document.document -> Vernacstate.t * events * bool -> prepared_task -> bool -> exec_result interruptible
 
 (* val update_overview : prepared_task -> prepared_task list -> state -> Document.document -> state
 val cut_overview : prepared_task -> state -> Document.document -> state *)

language-server/protocol/extProtocol.ml

@@ -54,12 +54,21 @@ module Notification = struct
 
     end
 
+    module InterruptParams = struct
+
+        type t = {
+          textDocument : VersionedTextDocumentIdentifier.t;
+        } [@@deriving yojson]
+
+      end
+
     type t =
     | Std of Lsp.Client_notification.t
     | InterpretToEnd of InterpretToEndParams.t
     | InterpretToPoint of InterpretToPointParams.t
     | StepForward of StepForwardParams.t
     | StepBackward of StepBackwardParams.t
+    | Interrupt of InterruptParams.t
 
     let of_jsonrpc (Jsonrpc.Notification.{ method_; params } as notif) =
       let open Lsp.Import.Result.O in
@@ -76,6 +85,9 @@ module Notification = struct
       | "vscoq/interpretToEnd" ->
         let+ params = Lsp.Import.Json.message_params params InterpretToEndParams.t_of_yojson in
         InterpretToEnd params
+      | "vscoq/interrupt" ->
+        let+ params = Lsp.Import.Json.message_params params InterruptParams.t_of_yojson in
+        Interrupt params
       | _ ->
         let+ notif = Lsp.Client_notification.of_jsonrpc notif in
         Std notif 

language-server/vscoqtop/lspManager.ml

@@ -535,6 +535,13 @@ let workspaceDidChangeConfiguration params =
   | Continuous -> run_documents ()
   | Manual -> reset_observe_ids (); ([] : events)
 
+let handle_interrupt params =
+  let Notification.Client.InterruptParams.{ textDocument } = params in
+  let uri = textDocument.uri in
+  match Hashtbl.find_opt states (DocumentUri.to_path uri) with
+  | None -> log (fun () -> "[interrupt] ignoring event on non existent document"); []
+  | Some { st } -> Dm.DocumentManager.cancel_ongoing_execution st; []
+
 let dispatch_std_request : type a. Jsonrpc.Id.t -> a Lsp.Client_request.t -> (a, error) result * events =
   fun id req ->
   match req with
@@ -590,6 +597,7 @@ let dispatch_notification =
   | InterpretToEnd params -> log (fun () -> "Received notification: vscoq/interpretToEnd"); coqtopInterpretToEnd params
   | StepBackward params -> log (fun () -> "Received notification: vscoq/stepBackward"); coqtopStepBackward params
   | StepForward params -> log (fun () -> "Received notification: vscoq/stepForward"); coqtopStepForward params
+  | Interrupt params -> log (fun () -> "Received notification: vscoq/interrupt"); handle_interrupt params
   | Std notif -> dispatch_std_notification notif
 
 let handle_lsp_event = function