From 51ad5ade5824cc674274cd3f798c8529292e443e Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 26 Sep 2024 00:33:00 +0200 Subject: [PATCH 1/2] support Restart --- language-server/dm/executionManager.ml | 39 ++++++++++++++------ language-server/dm/scheduler.ml | 41 ++++++++++++++++----- language-server/dm/scheduler.mli | 3 ++ language-server/tests/interactive/restart.v | 9 +++++ 4 files changed, 71 insertions(+), 21 deletions(-) create mode 100644 language-server/tests/interactive/restart.v diff --git a/language-server/dm/executionManager.ml b/language-server/dm/executionManager.ml index 92fdf7da..5b7fb0b8 100644 --- a/language-server/dm/executionManager.ml +++ b/language-server/dm/executionManager.ml @@ -106,6 +106,7 @@ let get_options () = !options type prepared_task = | PSkip of { id: sentence_id; error: Pp.t option } | PExec of executable_sentence + | PRestart of { id : sentence_id; to_ : sentence_id } | PQuery of executable_sentence | PDelegate of { terminator_id: sentence_id; opener_id: sentence_id; @@ -306,7 +307,7 @@ let rec cut_from_range r = function let cut_overview task state document = let range = match task with | PDelegate { terminator_id } -> Document.range_of_id_with_blank_space document terminator_id - | PSkip { id } | PExec { id } | PQuery { id } -> + | PSkip { id } | PExec { id } | PQuery { id } | PRestart {id } -> Document.range_of_id_with_blank_space document id in let {prepared; processing; processed} = state.overview in @@ -379,7 +380,7 @@ let invalidate_prepared_or_processing task state document = let processing = remove_or_truncate_range range processing in let overview = {state.overview with prepared; processing} in {state with overview} - | PSkip { id } | PExec { id } | PQuery { id } -> + | PSkip { id } | PExec { id } | PQuery { id } | PRestart {id } -> let range = Document.range_of_id_with_blank_space document id in let prepared = remove_or_truncate_range range prepared in let processing = remove_or_truncate_range range processing in @@ -400,7 +401,7 @@ let update_processing task state document = let prepared = remove_or_truncate_range range prepared in let overview = {state.overview with prepared; processing} in {state with overview} - | PSkip { id } | PExec { id } | PQuery { id } -> + | PSkip { id } | PExec { id } | PQuery { id } | PRestart {id } -> let range = Document.range_of_id_with_blank_space document id in let processing = insert_or_merge_range range processing in let prepared = remove_or_truncate_range range prepared in @@ -420,7 +421,7 @@ let update_prepared task document state = let prepared = List.append prepared [ range ] in let overview = {state.overview with prepared} in {state with overview} - | PSkip { id } | PExec { id } | PQuery { id } -> + | PSkip { id } | PExec { id } | PQuery { id } | PRestart {id } -> let range = Document.range_of_id_with_blank_space document id in let prepared = insert_or_merge_range range prepared in let overview = {state.overview with prepared} in @@ -436,7 +437,7 @@ let update_overview task todo state document = let overview = update_processed_as_Done (Success None) range state.overview in let overview = {overview with prepared} in {state with overview} - | PSkip { id } | PExec { id } | PQuery { id } -> + | PSkip { id } | PExec { id } | PQuery { id } | PRestart {id } -> update_processed id state document in match todo with @@ -568,6 +569,7 @@ let prepare_task task : prepared_task list = match task with | Skip { id; error } -> [PSkip { id; error }] | Exec e -> [PExec e] + | Restart { id; to_} -> [PRestart { id; to_}] | Query e -> [PQuery e] | OpaqueProof { terminator; opener_id; tasks; proof_using} -> match !options.delegation_mode with @@ -586,6 +588,7 @@ let id_of_prepared_task = function | PSkip { id } -> id | PExec ex -> ex.id | PQuery ex -> ex.id + | PRestart { id } -> id | PDelegate { terminator_id } -> terminator_id let purge_state = function @@ -634,6 +637,19 @@ let worker_main { ProofJob.tasks; initial_vernac_state = vs; doc_id; terminator_ Feedback.msg_debug @@ Pp.str "=========================================================="; exit 1 +let interp_Restart st id to_ = + match SM.find to_ st.of_sentence with + | (Done (Success (Some old_vs) as v), _) -> + let st = update st id v in + st, old_vs + | _ -> CErrors.anomaly ~label:"vscoq" Pp.(str"Restart: to_ is incorrect") + | exception Not_found -> assert false + +let exec_error_id_of_outcome v id = + match v with + | Success _ -> None + | Error _ -> Some id + let execute st (vs, events, interrupted) task = if interrupted then begin let st = update st (id_of_prepared_task task) (Error ((None,Pp.str "interrupted"),None,None)) in @@ -647,21 +663,20 @@ let execute st (vs, events, interrupted) task = | Some msg -> error None None msg vs in let st = update st id v in - (st, vs, events, false, None) + (st, vs, events, false, exec_error_id_of_outcome v id) | PExec { id; ast; synterp; error_recovery } -> let vs = { vs with Vernacstate.synterp } in let vs, v, ev = interp_ast ~doc_id:st.doc_id ~state_id:id ~st:vs ~error_recovery ast in - let exec_error = match v with - | Success _ -> None - | Error _ -> Some id - in let st = update st id v in - (st, vs, events @ ev, false, exec_error) + (st, vs, events @ ev, false, exec_error_id_of_outcome v id) + | PRestart { id; to_ } -> + let st, vs = interp_Restart st id to_ in + (st, vs, events, false, None) | PQuery { id; ast; synterp; error_recovery } -> let vs = { vs with Vernacstate.synterp } in let _, v, ev = interp_ast ~doc_id:st.doc_id ~state_id:id ~st:vs ~error_recovery ast in let st = update st id v in - (st, vs, events @ ev, false, None) + (st, vs, events @ ev, false, exec_error_id_of_outcome v id) | PDelegate { terminator_id; opener_id; last_step_id; tasks; proof_using } -> begin match find_fulfilled_opt opener_id st.of_sentence with | Some (Success _) -> diff --git a/language-server/dm/scheduler.ml b/language-server/dm/scheduler.ml index c8733a70..78e72f46 100644 --- a/language-server/dm/scheduler.ml +++ b/language-server/dm/scheduler.ml @@ -22,6 +22,8 @@ type error_recovery_strategy = | RSkip | RAdmitted +type restart = { id : sentence_id; to_ : sentence_id } + type executable_sentence = { id : sentence_id; ast : Synterp.vernac_control_entry; @@ -33,6 +35,7 @@ type executable_sentence = { type task = | Skip of { id: sentence_id; error: Pp.t option } | Exec of executable_sentence + | Restart of restart | OpaqueProof of { terminator: executable_sentence; opener_id: sentence_id; proof_using: Vernacexpr.section_subset_expr; @@ -45,9 +48,12 @@ type task = | ModuleWithSignature of ast list *) +type executable_sentence_or_restart = + | E of executable_sentence + | R of restart type proof_block = { - proof_sentences : executable_sentence list; + proof_sentences : executable_sentence_or_restart list; opener_id : sentence_id; } @@ -74,13 +80,19 @@ let initial_schedule = { } let push_executable_proof_sentence ex_sentence block = - { block with proof_sentences = ex_sentence :: block.proof_sentences } + { block with proof_sentences = E ex_sentence :: block.proof_sentences } let push_ex_sentence ex_sentence st = match st.proof_blocks with | [] -> { st with document_scope = ex_sentence.id :: st.document_scope } | l::q -> { st with proof_blocks = push_executable_proof_sentence ex_sentence l :: q } +let push_restart_command id to_ block = { block with proof_sentences = R { id; to_ } :: block.proof_sentences } +let push_restart id st = + match st.proof_blocks with + | [] -> st, Skip { id; error = Some (Pp.str "Restart can only be used inside a proof.")} + | l::q -> { st with proof_blocks = push_restart_command id l.opener_id l :: q }, Restart { id; to_ = l.opener_id } + (* Not sure what the base_id for nested lemmas should be, e.g. Lemma foo : X. Proof. @@ -94,7 +106,8 @@ let base_id st = | block :: l -> begin match block.proof_sentences with | [] -> aux l - | ex_sentence :: _ -> Some ex_sentence.id + | E { id } :: _ -> Some id + | R { to_ } :: _ -> Some to_ end in aux st.proof_blocks @@ -113,7 +126,7 @@ 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 + let document_scope = CList.uniquize @@ List.map (function E { id } -> id | R { id } -> 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 @@ -155,14 +168,16 @@ let find_proof_using (ast : Synterp.vernac_control_entry) = synterp, and if so where its value is stored. *) let find_proof_using_annotation { proof_sentences } = match List.rev proof_sentences with - | ex_sentence :: _ -> find_proof_using ex_sentence.ast + | E ex_sentence :: _ -> find_proof_using ex_sentence.ast | _ -> None let is_opaque_flat_proof terminator section_depth block = let open Vernacextend in - let has_side_effect { classif } = match classif with + let has_side_effect = function + | R _ -> true + | E { classif } -> match classif with | VtStartProof _ | VtSideff _ | VtQed _ | VtProofMode _ | VtMeta -> true | VtProofStep _ | VtQuery -> false in @@ -191,7 +206,7 @@ let push_state id ast synterp classif st = | Some proof_using -> log "opaque proof"; let terminator = { ex_sentence with error_recovery = RAdmitted } in - let tasks = List.rev block.proof_sentences in + let tasks = List.rev_map (function E x -> x | R _ -> assert false) block.proof_sentences in 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 -> @@ -205,20 +220,28 @@ let push_state id ast synterp classif st = base_id st, push_ex_sentence ex_sentence st, Exec ex_sentence | VtSideff _ -> base_id st, extrude_side_effect ex_sentence st, Exec ex_sentence - | VtMeta -> base_id st, push_ex_sentence ex_sentence st, Skip { id; error = Some (Pp.str "Unsupported command") } + | VtMeta -> + begin match ast.CAst.v.expr with + | Vernacexpr.(VernacSynPure VernacRestart) -> + let base = base_id st in + let st, t = push_restart ex_sentence.id st in + base, st, t (* TOOD: control *) + | _ -> base_id st, push_ex_sentence ex_sentence st, Skip { id; error = Some (Pp.str "Unsupported command") } + end | VtProofMode _ -> base_id st, push_ex_sentence ex_sentence st, Skip { id; error = Some (Pp.str "Unsupported command") } let string_of_task (task_id,(base_id,task)) = let s = match task with | Skip { id } -> Format.sprintf "Skip %s" (Stateid.to_string id) | Exec { id } -> Format.sprintf "Exec %s" (Stateid.to_string id) + | Restart { id; to_ } -> Format.sprintf "Reset %s -> %s" (Stateid.to_string id) (Stateid.to_string to_) | 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)) | 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 let _string_of_state st = - let scopes = (List.map (fun b -> List.map (fun x -> x.id) b.proof_sentences) st.proof_blocks) @ [st.document_scope] in + let scopes = (List.map (fun b -> List.map (function E { id } -> id | R { id } -> id) b.proof_sentences) st.proof_blocks) @ [st.document_scope] in String.concat "|" (List.map (fun l -> String.concat " " (List.map Stateid.to_string l)) scopes) let schedule_sentence (id, (ast, classif, synterp_st)) st schedule = diff --git a/language-server/dm/scheduler.mli b/language-server/dm/scheduler.mli index 436d9384..bc4f9611 100644 --- a/language-server/dm/scheduler.mli +++ b/language-server/dm/scheduler.mli @@ -27,6 +27,8 @@ type error_recovery_strategy = | RSkip | RAdmitted +type restart = { id : sentence_id; to_ : sentence_id } + type executable_sentence = { id : sentence_id; ast : Synterp.vernac_control_entry; @@ -38,6 +40,7 @@ type executable_sentence = { type task = | Skip of { id: sentence_id; error: Pp.t option } | Exec of executable_sentence + | Restart of restart | OpaqueProof of { terminator: executable_sentence; opener_id: sentence_id; proof_using: Vernacexpr.section_subset_expr; diff --git a/language-server/tests/interactive/restart.v b/language-server/tests/interactive/restart.v new file mode 100644 index 00000000..299826b2 --- /dev/null +++ b/language-server/tests/interactive/restart.v @@ -0,0 +1,9 @@ +Goal True. +Proof. + exact I. +Restart. + auto. +Restart. + cut False. +Restart. + \ No newline at end of file From dbe099bab10bb0659382504888e25e0124f9bf0f Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 26 Sep 2024 14:19:36 +0200 Subject: [PATCH 2/2] cleanup handling of unsupported commands (Skip) --- language-server/dm/executionManager.ml | 9 +-- language-server/dm/scheduler.ml | 103 +++++++++++++++++-------- language-server/dm/scheduler.mli | 4 +- 3 files changed, 78 insertions(+), 38 deletions(-) diff --git a/language-server/dm/executionManager.ml b/language-server/dm/executionManager.ml index 5b7fb0b8..2fe7f846 100644 --- a/language-server/dm/executionManager.ml +++ b/language-server/dm/executionManager.ml @@ -104,7 +104,7 @@ let is_diagnostics_enabled () = !options.enableDiagnostics let get_options () = !options type prepared_task = - | PSkip of { id: sentence_id; error: Pp.t option } + | PSkip of skip | PExec of executable_sentence | PRestart of { id : sentence_id; to_ : sentence_id } | PQuery of executable_sentence @@ -657,11 +657,8 @@ let execute st (vs, events, interrupted) task = end else try match task with - | PSkip { id; error = err } -> - let v = match err with - | None -> success vs - | Some msg -> error None None msg vs - in + | PSkip { id; error = e } -> + let v = error None None e vs in let st = update st id v in (st, vs, events, false, exec_error_id_of_outcome v id) | PExec { id; ast; synterp; error_recovery } -> diff --git a/language-server/dm/scheduler.ml b/language-server/dm/scheduler.ml index 78e72f46..4a50952a 100644 --- a/language-server/dm/scheduler.ml +++ b/language-server/dm/scheduler.ml @@ -24,6 +24,8 @@ type error_recovery_strategy = type restart = { id : sentence_id; to_ : sentence_id } +type skip = { id: sentence_id; error: Pp.t } + type executable_sentence = { id : sentence_id; ast : Synterp.vernac_control_entry; @@ -33,7 +35,7 @@ type executable_sentence = { } type task = - | Skip of { id: sentence_id; error: Pp.t option } + | Skip of skip | Exec of executable_sentence | Restart of restart | OpaqueProof of { terminator: executable_sentence; @@ -48,12 +50,17 @@ type task = | ModuleWithSignature of ast list *) -type executable_sentence_or_restart = +(* like a sub type of task, restricted what we can put in a proof *) +type proof_command = | E of executable_sentence | R of restart + | S of skip + +let id_of_proof_command = function + | S { id } | E { id } | R { id } -> id type proof_block = { - proof_sentences : executable_sentence_or_restart list; + proof_sentences : proof_command list; opener_id : sentence_id; } @@ -79,19 +86,29 @@ let initial_schedule = { dependencies = SM.empty; } -let push_executable_proof_sentence ex_sentence block = +let push_Exec_in_block ex_sentence block = { block with proof_sentences = E ex_sentence :: block.proof_sentences } -let push_ex_sentence ex_sentence st = +let push_Exec ex_sentence st = match st.proof_blocks with - | [] -> { st with document_scope = ex_sentence.id :: st.document_scope } - | l::q -> { st with proof_blocks = push_executable_proof_sentence ex_sentence l :: q } + | [] -> { st with document_scope = ex_sentence.id :: st.document_scope }, Exec ex_sentence + | l::q -> { st with proof_blocks = push_Exec_in_block ex_sentence l :: q }, Exec ex_sentence -let push_restart_command id to_ block = { block with proof_sentences = R { id; to_ } :: block.proof_sentences } -let push_restart id st = +let push_Restart_in_block r block = { block with proof_sentences = R r :: block.proof_sentences } +let push_Restart id st = match st.proof_blocks with - | [] -> st, Skip { id; error = Some (Pp.str "Restart can only be used inside a proof.")} - | l::q -> { st with proof_blocks = push_restart_command id l.opener_id l :: q }, Restart { id; to_ = l.opener_id } + | [] -> st, Skip { id; error = (Pp.str "Restart can only be used inside a proof.")} + | l :: q -> + let r = { id; to_ = l.opener_id } in + { st with proof_blocks = push_Restart_in_block r l :: q }, Restart r + +let push_Skip_in_block s block = { block with proof_sentences = S s :: block.proof_sentences } +let push_Skip st id error = + let v = { id; error } in + match st.proof_blocks with + | [] -> st, Skip v + | l::q -> { st with proof_blocks = push_Skip_in_block v l :: q }, Skip v + (* Not sure what the base_id for nested lemmas should be, e.g. Lemma foo : X. @@ -106,6 +123,7 @@ let base_id st = | block :: l -> begin match block.proof_sentences with | [] -> aux l + | S { id } :: _ -> Some id | E { id } :: _ -> Some id | R { to_ } :: _ -> Some to_ end @@ -113,20 +131,20 @@ let base_id st = aux st.proof_blocks let open_proof_block ex_sentence st = - let st = push_ex_sentence ex_sentence st in + let st, ex = push_Exec ex_sentence st in let block = { proof_sentences = []; opener_id = ex_sentence.id } in - { st with proof_blocks = block :: st.proof_blocks } + { st with proof_blocks = block :: st.proof_blocks }, ex let extrude_side_effect ex_sentence st = let document_scope = ex_sentence.id :: st.document_scope in - let proof_blocks = List.map (push_executable_proof_sentence ex_sentence) st.proof_blocks in - { st with document_scope; proof_blocks } + let proof_blocks = List.map (push_Exec_in_block ex_sentence) st.proof_blocks in + { st with document_scope; proof_blocks }, Exec ex_sentence let flatten_proof_block st = match st.proof_blocks with | [] -> st | [block] -> - let document_scope = CList.uniquize @@ List.map (function E { id } -> id | R { id } -> id) block.proof_sentences @ st.document_scope in + let document_scope = CList.uniquize @@ List.map id_of_proof_command 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 @@ -176,7 +194,7 @@ let find_proof_using_annotation { proof_sentences } = let is_opaque_flat_proof terminator section_depth block = let open Vernacextend in let has_side_effect = function - | R _ -> true + | R _ | S _ -> true | E { classif } -> match classif with | VtStartProof _ | VtSideff _ | VtQed _ | VtProofMode _ | VtMeta -> true | VtProofStep _ | VtQuery -> false @@ -194,41 +212,64 @@ let push_state id ast synterp classif st = let ex_sentence = { id; ast; classif; synterp; error_recovery = RSkip } in match classif with | VtStartProof _ -> - base_id st, open_proof_block ex_sentence st, Exec ex_sentence + let base = base_id st in + let st, task = open_proof_block ex_sentence st in + base, st, task | VtQed terminator_type -> log "scheduling a qed"; begin match st.proof_blocks with | [] -> (* can happen on ill-formed documents *) - base_id st, push_ex_sentence ex_sentence st, Exec ex_sentence + let base = base_id st in + let st, task = push_Exec ex_sentence st in + base, st, task | block :: pop -> (* TODO do not delegate if command with side effect inside the proof or nested lemmas *) match is_opaque_flat_proof terminator_type st.section_depth block with | Some proof_using -> log "opaque proof"; let terminator = { ex_sentence with error_recovery = RAdmitted } in - let tasks = List.rev_map (function E x -> x | R _ -> assert false) block.proof_sentences in + let tasks = List.rev_map (function E x -> x | R _ | S _ -> assert false) block.proof_sentences in 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 } + let base = base_id st in + let st, _task = push_Exec ex_sentence st in + base, 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 base = base_id st in + let st, task = push_Exec ex_sentence st in + base, st, task end | VtQuery -> (* queries have no impact, we don't push them *) base_id st, st, Query ex_sentence | VtProofStep _ -> - base_id st, push_ex_sentence ex_sentence st, Exec ex_sentence + let base = base_id st in + let st, task = push_Exec ex_sentence st in + base, st, task | VtSideff _ -> - base_id st, extrude_side_effect ex_sentence st, Exec ex_sentence + let base = base_id st in + let st, task = extrude_side_effect ex_sentence st in + base, st, task | VtMeta -> - begin match ast.CAst.v.expr with - | Vernacexpr.(VernacSynPure VernacRestart) -> + let v = ast.CAst.v in + begin match v.expr, v.control with + | Vernacexpr.(VernacSynPure VernacRestart), [] -> + let base = base_id st in + let st, task = push_Restart ex_sentence.id st in + base, st, task + | Vernacexpr.(VernacSynPure VernacRestart), _ :: _ -> + let base = base_id st in + let st, task = push_Skip st id (Pp.str "Restart cannot be decorated by controls like Time, Fail, etc...") in + base, st, task + | _ -> let base = base_id st in - let st, t = push_restart ex_sentence.id st in - base, st, t (* TOOD: control *) - | _ -> base_id st, push_ex_sentence ex_sentence st, Skip { id; error = Some (Pp.str "Unsupported command") } + let st, task = push_Skip st id (Pp.str "Unsupported navigation command") in + base, st, task end - | VtProofMode _ -> base_id st, push_ex_sentence ex_sentence st, Skip { id; error = Some (Pp.str "Unsupported command") } + | VtProofMode _ -> + let base = base_id st in + let st, task = push_Skip st id (Pp.str "Unsupported command") in + base, st, task let string_of_task (task_id,(base_id,task)) = let s = match task with @@ -241,7 +282,7 @@ let string_of_task (task_id,(base_id,task)) = Format.sprintf "[%s] : [%s] -> %s" (Stateid.to_string task_id) (Option.cata Stateid.to_string "init" base_id) s let _string_of_state st = - let scopes = (List.map (fun b -> List.map (function E { id } -> id | R { id } -> id) b.proof_sentences) st.proof_blocks) @ [st.document_scope] in + let scopes = (List.map (fun b -> List.map id_of_proof_command b.proof_sentences) st.proof_blocks) @ [st.document_scope] in String.concat "|" (List.map (fun l -> String.concat " " (List.map Stateid.to_string l)) scopes) let schedule_sentence (id, (ast, classif, synterp_st)) st schedule = diff --git a/language-server/dm/scheduler.mli b/language-server/dm/scheduler.mli index bc4f9611..617b9c14 100644 --- a/language-server/dm/scheduler.mli +++ b/language-server/dm/scheduler.mli @@ -29,6 +29,8 @@ type error_recovery_strategy = type restart = { id : sentence_id; to_ : sentence_id } +type skip = { id: sentence_id; error: Pp.t } + type executable_sentence = { id : sentence_id; ast : Synterp.vernac_control_entry; @@ -38,7 +40,7 @@ type executable_sentence = { } type task = - | Skip of { id: sentence_id; error: Pp.t option } + | Skip of skip | Exec of executable_sentence | Restart of restart | OpaqueProof of { terminator: executable_sentence;