Add Semi-Continuous mode for larger and slower files

client/package.json

@@ -145,11 +145,13 @@
             "type": "number",
             "enum": [
               0,
-              1
+              1,
+              2
             ],
             "enumItemLabels": [
               "Manual",
-              "Continuous"
+              "Continuous",
+              "SemiContinuous"
             ],
             "default": 1,
             "description": "Configures the proof checking mode for Coq."

client/src/Decorations.ts

@@ -9,6 +9,7 @@ interface Decorations {
 }
 
 export let decorationsContinuous : Decorations;
+export let decorationsSemiContinuous : Decorations;
 export let decorationsManual : Decorations;
 
 export function initializeDecorations(context: vscode.ExtensionContext) {
@@ -34,6 +35,23 @@ export function initializeDecorations(context: vscode.ExtensionContext) {
         }),
     };
 
+    decorationsSemiContinuous = {
+        parsed: create({
+            overviewRulerColor: 'cyan', 
+            overviewRulerLane: vscode.OverviewRulerLane.Right,
+        }),
+        processing: create({
+            overviewRulerColor: 'blue', 
+            overviewRulerLane: vscode.OverviewRulerLane.Center,
+        }),
+        processed: create({
+            overviewRulerColor: '#20b2aa', 
+            overviewRulerLane: vscode.OverviewRulerLane.Left,
+            light: {backgroundColor: 'rgba(0,150,0,0.2)'},
+            dark: {backgroundColor: 'rgba(0,150,0,0.2)'},
+        }),
+    };
+
     decorationsManual = {
         parsed: create({
             outlineWidth: '1px',

client/src/client.ts

@@ -7,7 +7,7 @@ import {
   integer
 } from 'vscode-languageclient/node';
 
-import {decorationsManual, decorationsContinuous} from './Decorations';
+import {decorationsManual, decorationsContinuous, decorationsSemiContinuous} from './Decorations';
 
 export default class Client extends LanguageClient {
 
@@ -62,6 +62,7 @@ export default class Client extends LanguageClient {
         editors.map(editor => {
             editor.setDecorations(decorationsManual.processed, []);
             editor.setDecorations(decorationsContinuous.processed, []);
+            editor.setDecorations(decorationsSemiContinuous.processed, []);
         });
     }
 
@@ -71,8 +72,10 @@ export default class Client extends LanguageClient {
         editors.map(editor => {
             if(config.mode === 0) {
                 editor.setDecorations(decorationsManual.processed, ranges);
-            } else {
+            } else if (config.mode === 1) {
                 editor.setDecorations(decorationsContinuous.processed, ranges);
+            } else {
+                editor.setDecorations(decorationsSemiContinuous.processed, ranges);
             }
         });
     }

client/src/extension.ts

@@ -267,7 +267,7 @@ Path: \`${coqTM.getVsCoqTopPath()}\`
             let goalsHook = window.onDidChangeTextEditorSelection(
                 (evt: TextEditorSelectionChangeEvent) => {                    
                     if (evt.textEditor.document.languageId === "coq"
-                        && workspace.getConfiguration('vscoq.proof').mode === 1)
+                        && (workspace.getConfiguration('vscoq.proof').mode === 1 || workspace.getConfiguration('vscoq.proof').mode === 2))
                     {
                         sendInterpretToPoint(evt.textEditor, client);
                     }

language-server/dm/documentManager.ml

@@ -155,25 +155,25 @@ let get_messages st pos =
     | Some (_oloc,msg) -> (DiagnosticSeverity.Error, pp_of_coqpp msg) :: feedback
     | None -> feedback
 
-let interpret_to ~stateful ~background state id : (state * event Sel.Event.t list) =
+let interpret_to ~skip_proofs ~stateful ~background state id : (state * event Sel.Event.t list) =
   match Document.get_sentence state.document id with
   | None -> (state, []) (* TODO error? *)
   | Some { id } ->
     let state = if stateful then { state with observe_id = Some id } else state in
-    let vst_for_next_todo, todo = ExecutionManager.build_tasks_for (Document.schedule state.document) state.execution_state id in
+    let vst_for_next_todo, todo = ExecutionManager.build_tasks_for ~skip_proofs (Document.schedule state.document) state.execution_state id in
     if CList.is_empty todo then
       (state, [])
     else
       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 =
+let interpret_to_position ~skip_proofs ~stateful st pos =
   match id_of_pos st pos with
   | None -> (st, []) (* document is empty *)
-  | Some id -> interpret_to ~stateful ~background:false st id
+  | Some id -> interpret_to ~skip_proofs ~stateful ~background:false st id
 
-let interpret_to_previous st =
+let interpret_to_previous ~skip_proofs st =
   match st.observe_id with
   | None -> (st, [])
   | Some oid ->
@@ -184,32 +184,32 @@ let interpret_to_previous st =
       | None -> 
         Vernacstate.unfreeze_full_state st.init_vs; 
         { st with observe_id=None}, []
-      | Some { id } -> interpret_to ~stateful:true ~background:false st id 
+      | Some { id } -> interpret_to ~skip_proofs ~stateful:true ~background:false st id 
 
-let interpret_to_next st =
+let interpret_to_next ~skip_proofs st =
   match st.observe_id with
   | None -> 
     begin match Document.get_first_sentence st.document with
     | None -> (st, []) (*The document is empty*)
-    | Some {id} -> interpret_to ~stateful:true ~background:false st id
+    | Some {id} -> interpret_to ~skip_proofs ~stateful:true ~background:false st id
     end
   | Some id ->
     match Document.get_sentence st.document id with
     | None -> (st, []) (* TODO error? *)
     | Some { stop } ->
       match Document.find_sentence_after st.document (stop+1) with
       | None -> (st, [])
-      | Some {id } -> interpret_to ~stateful:true ~background:false st id
+      | Some {id } -> interpret_to ~skip_proofs ~stateful:true ~background:false st id
 
-let interpret_to_end st =
+let interpret_to_end ~skip_proofs st =
   match Document.get_last_sentence st.document with 
   | None -> (st, [])
-  | Some {id} -> log ("interpret_to_end id = " ^ Stateid.to_string id); interpret_to ~stateful:true ~background:false st id
+  | Some {id} -> log ("interpret_to_end id = " ^ Stateid.to_string id); interpret_to ~skip_proofs ~stateful:true ~background:false st id
 
 let interpret_in_background st =
   match Document.get_last_sentence st.document with 
   | None -> (st, [])
-  | Some {id} -> log ("interpret_to_end id = " ^ Stateid.to_string id); interpret_to ~stateful:true ~background:true st id
+  | Some {id} -> log ("interpret_to_end id = " ^ Stateid.to_string id); interpret_to ~skip_proofs:false ~stateful:true ~background:true st id
 
 let validate_document state =
   let unchanged_id, invalid_ids, document = Document.validate_document state.document in

language-server/dm/documentManager.mli

@@ -40,20 +40,20 @@ val apply_text_edits : state -> text_edit list -> state
     document is parsed, outdated executions states are invalidated, and the observe
     id is updated. *)
 
-val interpret_to_position : stateful:bool -> state -> Position.t -> (state * events)
+val interpret_to_position : skip_proofs:bool -> stateful:bool -> state -> Position.t -> (state * events)
 (** [interpret_to_position stateful doc pos] navigates to the last sentence ending
     before or at [pos] and returns the resulting state. The [stateful] flag 
     determines if we record the resulting position in the state. *)
 
-val interpret_to_previous : state -> (state * events)
+val interpret_to_previous : skip_proofs:bool -> state -> (state * events)
 (** [interpret_to_previous doc] navigates to the previous sentence in [doc]
     and returns the resulting state. *)
 
-val interpret_to_next : state -> (state * events)
+val interpret_to_next : skip_proofs:bool -> state -> (state * events)
 (** [interpret_to_next doc] navigates to the next sentence in [doc]
     and returns the resulting state. *)
 
-val interpret_to_end : state -> (state * events)
+val interpret_to_end : skip_proofs:bool -> state -> (state * events)
 (** [interpret_to_end doc] navigates to the last sentence in [doc]
     and returns the resulting state. *)
 

language-server/dm/executionManager.ml

@@ -309,24 +309,38 @@ let destroy st =
 
 let last_opt l = try Some (CList.last l).id with Failure _ -> None
 
-let prepare_task task : prepared_task list =
+let prepare_task skip_proofs task : prepared_task list =
   match task with
   | Skip { id; error } -> [PSkip { id; error }]
   | Exec e -> [PExec e]
   | Query e -> [PQuery e]
   | OpaqueProof { terminator; opener_id; tasks; proof_using} ->
-      match !options.delegation_mode with
-      | DelegateProofsToWorkers _ ->
-          log "delegating proofs to workers";
-          let last_step_id = last_opt tasks in
-          let tasks = List.map (fun x -> PExec x) tasks in
-          [PDelegate {terminator_id = terminator.id; opener_id; last_step_id; tasks; proof_using}]
-      | CheckProofsInMaster ->
-          log "running the proof in master as per config";
-          List.map (fun x -> PExec x) tasks @ [PExec terminator]
-      | SkipProofs ->
+      if skip_proofs then
+        [PExec terminator]
+      else
+        (match !options.delegation_mode with
+        | DelegateProofsToWorkers _ ->
+            log "delegating proofs to workers";
+            let last_step_id = last_opt tasks in
+            let tasks = List.map (fun x -> PExec x) tasks in
+            [PDelegate {terminator_id = terminator.id; opener_id; last_step_id; tasks; proof_using}]
+        | CheckProofsInMaster ->
+            log "running the proof in master as per config";
+            List.map (fun x -> PExec x) tasks @ [PExec terminator]
+        | SkipProofs ->
+            log (Printf.sprintf "skipping proof made of %d tasks" (List.length tasks));
+            [PExec terminator])
+  | NonOpaqueProof { terminator; tasks} ->
+    if skip_proofs then
+      [PExec terminator]
+    else
+      (match !options.delegation_mode with
+        | SkipProofs ->
           log (Printf.sprintf "skipping proof made of %d tasks" (List.length tasks));
           [PExec terminator]
+        | _ ->
+            log "running the proof in master as per config";
+            List.map (fun x -> PExec x) tasks @ [PExec terminator])
 
 let id_of_prepared_task = function
   | PSkip { id } -> id
@@ -460,7 +474,7 @@ let execute st (vs, events, interrupted) task =
       let st = update st (id_of_prepared_task task) (Error ((None,Pp.str "interrupted"),None)) in
       (st, vs, events, true)
 
-let build_tasks_for sch st id =
+let build_tasks_for ~skip_proofs sch st id =
   let rec build_tasks id tasks =
     begin match find_fulfilled_opt id st.of_sentence with
     | Some (Success (Some vs)) ->
@@ -483,7 +497,7 @@ let build_tasks_for sch st id =
     end
   in
   let vs, tasks = build_tasks id [] in
-  vs, List.concat_map prepare_task tasks
+  vs, List.concat_map (prepare_task skip_proofs) tasks
 
 let all_errors st =
   List.fold_left (fun acc (id, (p,_)) ->

language-server/dm/executionManager.mli

@@ -71,7 +71,7 @@ val handle_event : event -> state -> (state option * events)
 (** Execution happens in two steps. In particular the event one takes only
     one task at a time to ease checking for interruption *)
 type prepared_task
-val build_tasks_for : Scheduler.schedule -> state -> sentence_id -> Vernacstate.t * prepared_task list
+val build_tasks_for : skip_proofs:bool -> Scheduler.schedule -> state -> sentence_id -> Vernacstate.t * prepared_task list
 val execute : state -> Vernacstate.t * events * bool -> prepared_task -> (state * Vernacstate.t * events * bool)
 
 (** Coq toplevels for delegation without fork *)

language-server/dm/scheduler.ml

@@ -38,6 +38,10 @@ type task =
                      proof_using: Vernacexpr.section_subset_expr;
                      tasks : executable_sentence list; (* non empty list *)
                    }
+  | NonOpaqueProof of { terminator: executable_sentence;
+                        opener_id: sentence_id;
+                        tasks : executable_sentence list; (* non empty list *)
+                      }
   | Query of executable_sentence
 
 (*
@@ -107,17 +111,6 @@ let extrude_side_effect ex_sentence st =
   let proof_blocks = List.map (push_executable_proof_sentence ex_sentence) st.proof_blocks in
   { st with document_scope; proof_blocks }
 
-let flatten_proof_block st =
-  match st.proof_blocks with
-  | [] -> st
-  | [block] ->
-    let document_scope = CList.uniquize @@ List.map (fun x -> x.id) block.proof_sentences @ st.document_scope in
-    { st with document_scope; proof_blocks = [] }
-  | block1 :: block2 :: tl -> (* Nested proofs. TODO check if we want to extrude one level or directly to document scope *)
-    let proof_sentences = CList.uniquize @@ block1.proof_sentences @ block2.proof_sentences in
-    let block2 = { block2 with proof_sentences } in
-    { st with proof_blocks = block2 :: tl }
-
 (*
 [1] Lemma foo : XX.
 [2] Proof.
@@ -193,9 +186,10 @@ let push_state id ast synterp classif st =
         let st = { st with proof_blocks = pop } in
         base_id st, push_ex_sentence ex_sentence st, OpaqueProof { terminator; opener_id = block.opener_id; tasks; proof_using }
       | None ->
-        log "not an opaque proof";
-        let st = flatten_proof_block st in
-        base_id st, push_ex_sentence ex_sentence st, Exec ex_sentence
+        let terminator = { ex_sentence with error_recovery = RAdmitted } in
+        let tasks = List.rev block.proof_sentences in
+        let st = { st with proof_blocks = pop } in
+        base_id st, push_ex_sentence ex_sentence st, NonOpaqueProof { terminator; opener_id = block.opener_id; tasks }
     end
   | VtQuery -> (* queries have no impact, we don't push them *)
     base_id st, st, Query ex_sentence
@@ -211,6 +205,7 @@ let string_of_task (task_id,(base_id,task)) =
   | Skip { id } -> Format.sprintf "Skip %s" (Stateid.to_string id)
   | Exec { id } -> Format.sprintf "Exec %s" (Stateid.to_string id)
   | OpaqueProof { terminator; tasks } -> Format.sprintf "OpaqueProof [%s | %s]" (Stateid.to_string terminator.id) (String.concat "," (List.map (fun task -> Stateid.to_string task.id) tasks))
+  | NonOpaqueProof { terminator; tasks } -> Format.sprintf "NonOpaqueProof [%s | %s]" (Stateid.to_string terminator.id) (String.concat "," (List.map (fun task -> Stateid.to_string task.id) tasks))
   | Query { id } -> Format.sprintf "Query %s" (Stateid.to_string id)
   in
   Format.sprintf "[%s] : [%s] -> %s" (Stateid.to_string task_id) (Option.cata Stateid.to_string "init" base_id) s

language-server/dm/scheduler.mli

@@ -43,6 +43,10 @@ type task =
                      proof_using: Vernacexpr.section_subset_expr;
                      tasks : executable_sentence list; (* non empty list *)
                    }
+  | NonOpaqueProof of { terminator: executable_sentence;
+                        opener_id: sentence_id;
+                        tasks : executable_sentence list; (* non empty list *)
+                      }
   | Query of executable_sentence
 
 type schedule

language-server/protocol/settings.ml

@@ -37,15 +37,18 @@ module Mode = struct
   type t =
   | Continuous 
   | Manual
+  | SemiContinuous
   [@@deriving yojson]
 
   let yojson_of_t = function
   | Manual -> `Int 0
   | Continuous -> `Int 1
+  | SemiContinuous -> `Int 2
 
   let t_of_yojson = function
   | `Int 0 -> Manual
   | `Int 1 -> Continuous
+  | `Int 2 -> SemiContinuous
   | _ -> Yojson.json_error @@ "invalid value "
 
 end