diff --git a/client/package.json b/client/package.json index 8280b957d..d345e35c9 100644 --- a/client/package.json +++ b/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." diff --git a/client/src/Decorations.ts b/client/src/Decorations.ts index fa75f0d40..e41e6612f 100644 --- a/client/src/Decorations.ts +++ b/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', diff --git a/client/src/client.ts b/client/src/client.ts index ffd4d1e0c..8e08108a1 100644 --- a/client/src/client.ts +++ b/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); } }); } diff --git a/client/src/extension.ts b/client/src/extension.ts index e067ca784..d6296328f 100644 --- a/client/src/extension.ts +++ b/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); } diff --git a/language-server/dm/documentManager.ml b/language-server/dm/documentManager.ml index 2fc197963..c2ebbb376 100644 --- a/language-server/dm/documentManager.ml +++ b/language-server/dm/documentManager.ml @@ -155,12 +155,12 @@ 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 @@ -168,12 +168,12 @@ let interpret_to ~stateful ~background state id : (state * event Sel.Event.t lis 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,14 +184,14 @@ 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 @@ -199,17 +199,17 @@ let interpret_to_next st = | 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 diff --git a/language-server/dm/documentManager.mli b/language-server/dm/documentManager.mli index 95a351f13..5d3d4d438 100644 --- a/language-server/dm/documentManager.mli +++ b/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. *) diff --git a/language-server/dm/executionManager.ml b/language-server/dm/executionManager.ml index ce28c38ce..1c7219a04 100644 --- a/language-server/dm/executionManager.ml +++ b/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,_)) -> diff --git a/language-server/dm/executionManager.mli b/language-server/dm/executionManager.mli index ac38bab9c..1b329d732 100644 --- a/language-server/dm/executionManager.mli +++ b/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 *) diff --git a/language-server/dm/scheduler.ml b/language-server/dm/scheduler.ml index dfadadfad..0940ca809 100644 --- a/language-server/dm/scheduler.ml +++ b/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 diff --git a/language-server/dm/scheduler.mli b/language-server/dm/scheduler.mli index 436d9384f..9f381ed68 100644 --- a/language-server/dm/scheduler.mli +++ b/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 diff --git a/language-server/protocol/settings.ml b/language-server/protocol/settings.ml index 95638dcda..2e7e7ffa9 100644 --- a/language-server/protocol/settings.ml +++ b/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 diff --git a/language-server/vscoqtop/lspManager.ml b/language-server/vscoqtop/lspManager.ml index c468b22a6..970e4bec8 100644 --- a/language-server/vscoqtop/lspManager.ml +++ b/language-server/vscoqtop/lspManager.ml @@ -221,9 +221,9 @@ let textDocumentDidOpen params = let vst, opts = get_init_state () in let st, events = Dm.DocumentManager.init vst ~opts uri ~text in let (st, events') = - if !check_mode = Settings.Mode.Continuous then - Dm.DocumentManager.interpret_in_background st - else + if !check_mode <> Settings.Mode.Manual then + Dm.DocumentManager.interpret_in_background st + else (st, []) in Hashtbl.add states (DocumentUri.to_path uri) st; @@ -242,7 +242,7 @@ let textDocumentDidChange params = let text_edits = List.map mk_text_edit contentChanges in let st = Dm.DocumentManager.apply_text_edits st text_edits in let (st, events) = - if !check_mode = Settings.Mode.Continuous then + if !check_mode <> Settings.Mode.Manual then Dm.DocumentManager.interpret_in_background st else (st, []) @@ -251,6 +251,7 @@ let textDocumentDidChange params = update_view uri st; inject_dm_events (uri, events) + let textDocumentDidSave params = [] (* TODO handle properly *) @@ -285,7 +286,7 @@ let coqtopInterpretToPoint params = match Hashtbl.find_opt states (DocumentUri.to_path uri) with | None -> log @@ "[interpretToPoint] ignoring event on non existant document"; [] | Some st -> - let (st, events) = Dm.DocumentManager.interpret_to_position ~stateful:(!check_mode = Settings.Mode.Manual) st position in + let (st, events) = Dm.DocumentManager.interpret_to_position ~skip_proofs:(!check_mode = Settings.Mode.SemiContinuous) ~stateful:(!check_mode = Settings.Mode.Manual) st position in Hashtbl.replace states (DocumentUri.to_path uri) st; update_view uri st; let sel_events = inject_dm_events (uri, events) in @@ -296,7 +297,7 @@ let coqtopStepBackward params = match Hashtbl.find_opt states (DocumentUri.to_path uri) with | None -> log @@ "[stepBackward] ignoring event on non existant document"; [] | Some st -> - let (st, events) = Dm.DocumentManager.interpret_to_previous st in + let (st, events) = Dm.DocumentManager.interpret_to_previous ~skip_proofs:(!check_mode = Settings.Mode.SemiContinuous) st in let range = Dm.DocumentManager.observe_id_range st in Hashtbl.replace states (DocumentUri.to_path uri) st; update_view uri st; @@ -314,7 +315,7 @@ let coqtopStepForward params = match Hashtbl.find_opt states (DocumentUri.to_path uri) with | None -> log @@ "ignoring event on non existant document"; [] | Some st -> - let (st, events) = Dm.DocumentManager.interpret_to_next st in + let (st, events) = Dm.DocumentManager.interpret_to_next ~skip_proofs:(!check_mode = Settings.Mode.SemiContinuous) st in let range = Dm.DocumentManager.observe_id_range st in Hashtbl.replace states (DocumentUri.to_path uri) st; update_view uri st; @@ -364,7 +365,7 @@ let coqtopResetCoq id params = | Some st -> let st, events = Dm.DocumentManager.reset st in let (st, events') = - if !check_mode = Settings.Mode.Continuous then + if !check_mode <> Settings.Mode.Manual then Dm.DocumentManager.interpret_in_background st else (st, []) @@ -378,7 +379,7 @@ let coqtopInterpretToEnd params = match Hashtbl.find_opt states (DocumentUri.to_path uri) with | None -> log @@ "[interpretToEnd] ignoring event on non existant document"; [] | Some st -> - let (st, events) = Dm.DocumentManager.interpret_to_end st in + let (st, events) = Dm.DocumentManager.interpret_to_end ~skip_proofs:false st in Hashtbl.replace states (DocumentUri.to_path uri) st; update_view uri st; inject_dm_events (uri,events) @ [ mk_proof_view_event uri None] @@ -433,7 +434,7 @@ let workspaceDidChangeConfiguration params = let Lsp.Types.DidChangeConfigurationParams.{ settings } = params in let settings = Settings.t_of_yojson settings in do_configuration settings; - if !check_mode = Settings.Mode.Continuous then + if !check_mode <> Settings.Mode.Manual then run_documents () else []