Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Interupt consecutive parsing events #937

Closed
wants to merge 4 commits into from
Closed

Interupt consecutive parsing events #937

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
3679529
feat: make parsing part of the event loop
rtetley Oct 31, 2024
fb79e31
WIP
rtetley Nov 4, 2024
5ea8a06
simplification attempt
gares Nov 5, 2024
696370c
Merge pull request #939 from coq/interrupt-parsing
rtetley Nov 6, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
75 changes: 66 additions & 9 deletions language-server/dm/documentManager.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -44,6 +44,13 @@ type state = {
observe_id : observe_id option;
}

type parse_event = {
started: float;
state: state;
background: bool;
block_on_error: bool;
}

type event =
| Execute of { (* we split the computation to help interruptibility *)
id : Types.sentence_id; (* sentence of interest *)
Expand All @@ -55,11 +62,16 @@ type event =
background: bool; (* Just to re-set execution priorities later down the loop *)
}
| ExecutionManagerEvent of ExecutionManager.event
| ParseEvent of parse_event

let pp_event fmt = function
| Execute { id; todo; started; _ } ->
let time = Unix.gettimeofday () -. started in
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"
| ParseEvent { started; _} ->
let time = Unix.gettimeofday () -. started in
Stdlib.Format.fprintf fmt "ParseEvent (started %2.3f ago)" time

let inject_em_event x = Sel.Event.map (fun e -> ExecutionManagerEvent e) x
let inject_em_events events = List.map inject_em_event events
Expand Down Expand Up @@ -435,7 +447,7 @@ let dirpath_of_top = Coqargs.dirpath_of_top
let dirpath_of_top = Coqinit.dirpath_of_top
[%%endif]

let init init_vs ~opts uri ~text observe_id =
let init init_vs ~opts uri ~text ~background ~block_on_error observe_id =
Vernacstate.unfreeze_full_state init_vs;
let top = try (dirpath_of_top (TopPhysical (DocumentUri.to_path uri))) with
e -> raise e
Expand All @@ -444,20 +456,26 @@ let init init_vs ~opts uri ~text observe_id =
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 st = { uri; opts; init_vs; document; execution_state; observe_id } in
validate_document st, [inject_em_event feedback]
let state = { uri; opts; init_vs; document; execution_state; observe_id } in
let started = Unix.gettimeofday () in
let priority = Some PriorityManager.parsing in
let event = [Sel.now ?priority (ParseEvent {started; state; background; block_on_error})] in
state, event @ [inject_em_event feedback]

let reset { uri; opts; init_vs; document; execution_state; observe_id } =
let reset { uri; opts; init_vs; document; execution_state; observe_id } ~background ~block_on_error =
let text = RawDocument.text @@ Document.raw_document document in
Vernacstate.unfreeze_full_state init_vs;
let document = Document.create_document init_vs.synterp text in
ExecutionManager.destroy execution_state;
let execution_state, feedback = ExecutionManager.init init_vs in
let observe_id = if observe_id = None then None else (Some Top) in
let st = { uri; opts; init_vs; document; execution_state; observe_id } in
validate_document st, [inject_em_event feedback]
let state = { uri; opts; init_vs; document; execution_state; observe_id } in
let started = Unix.gettimeofday () in
let priority = Some PriorityManager.parsing in
let event = [Sel.now ?priority (ParseEvent {started; state; background; block_on_error})] in
state, event @ [inject_em_event feedback]

let apply_text_edits state edits =
let apply_text_edits state edits ~background ~block_on_error =
let apply_edit_and_shift_diagnostics_locs_and_overview state (range, new_text as edit) =
let document = Document.apply_text_edit state.document edit in
let exec_st = state.execution_state in
Expand All @@ -470,7 +488,9 @@ let apply_text_edits state edits =
{state with execution_state; document}
in
let state = List.fold_left apply_edit_and_shift_diagnostics_locs_and_overview state edits in
validate_document state
let priority = Some PriorityManager.parsing in
let started = Unix.gettimeofday () in
[Sel.now ?priority (ParseEvent {started; state; background; block_on_error})]

let execution_finished st id started =
let time = Unix.gettimeofday () -. started in
Expand Down Expand Up @@ -540,6 +560,21 @@ let handle_execution_manager_event st ev =
in
(st, inject_em_events events, None)

let rec most_recent_parsing_event acc = function
| [] -> acc
| ParseEvent { started } :: rest -> most_recent_parsing_event (Float.max acc started) rest
| _ :: rest -> most_recent_parsing_event acc rest

let prune_outdated el =
(* remove old parsing events *)
let ts = most_recent_parsing_event 0.0 el in
let most_recent_pe = function
| ParseEvent {started; } -> Float.equal ts started
| _ -> true in
let el = List.filter most_recent_pe el in
(* TODO: filter old exec events *)
el

let handle_event ev st block =
match ev with
| Execute { id; todo = []; started } -> (* the vst_for_next_todo is also in st.execution_state *)
Expand All @@ -548,7 +583,29 @@ let handle_event ev st block =
execute st id vst_for_next_todo started task todo background block
| ExecutionManagerEvent ev ->
handle_execution_manager_event st ev

| ParseEvent { state; background; block_on_error } ->
let st = validate_document state in
if background then
let (st, events, blocking_error) = interpret_in_background st ~should_block_on_error:block_on_error in
(Some st), events, blocking_error
else
(Some st), [], None


let handle_events el st0 block =
let el = prune_outdated el in
let rec handle st new_events el =
match el with
| [] -> st, [], None
| e :: el ->
let st = Option.default st0 st in
let st, more_new_events, stop = handle_event e st block in
let new_events = new_events @ more_new_events in
if Option.is_empty stop then handle st new_events el
else st, new_events, stop (* BUG: do something with el *)
in
handle None [] el

let get_proof st diff_mode pos =
let previous_st id =
let oid = fst @@ Scheduler.task_for_sentence (Document.schedule st.document) id in
Expand Down
17 changes: 10 additions & 7 deletions language-server/dm/documentManager.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -38,14 +38,17 @@ val pp_event : Format.formatter -> event -> unit

type events = event Sel.Event.t list

val init : Vernacstate.t -> opts:Coqargs.injection_command list -> DocumentUri.t -> text:string -> observe_id option -> state * events
val init : Vernacstate.t -> opts:Coqargs.injection_command list -> DocumentUri.t -> text:string -> background:bool -> block_on_error:bool -> observe_id option -> state * events
(** [init st opts uri text] initializes the document manager with initial vernac state
[st] on which command line opts will be set. *)
[st] on which command line opts will be set. [background] indicates if the document should
be executed in the background once it is parsed. *)

val apply_text_edits : state -> text_edit list -> state
(** [apply_text_edits doc edits] updates the text of [doc] with [edits]. The new
val apply_text_edits : state -> text_edit list -> background:bool -> block_on_error:bool -> events
(** [apply_text_edits doc edits] updates the text of [doc] with [edits].
A ParseEvent is triggered, once processed: the new
document is parsed, outdated executions states are invalidated, and the observe
id is updated. *)
id is updated. Finally if [background] is set to true, an execution is launched in
the background *)

val clear_observe_id : state -> state
(** [clear_observe_id state] updates the state to make the observe_id None *)
Expand Down Expand Up @@ -83,7 +86,7 @@ val interpret_in_background : state -> should_block_on_error:bool -> (state * ev
(** [interpret_in_background doc] same as [interpret_to_end] but computation
is done in background (with lower priority) *)

val reset : state -> state * events
val reset : state -> background:bool -> block_on_error:bool -> state * events
(** resets Coq *)

val executed_ranges : state -> exec_overview
Expand All @@ -109,7 +112,7 @@ val get_proof : state -> Settings.Goals.Diff.Mode.t -> Position.t option -> Proo

val get_completions : state -> Position.t -> (completion_item list, string) Result.t

val handle_event : event -> state -> bool -> (state option * events * blocking_error option)
val handle_events : event list -> state -> bool -> (state option * events * blocking_error option)
(** handles events and returns a new state if it was updated *)

val search : state -> id:string -> Position.t -> string -> notification Sel.Event.t list
Expand Down
7 changes: 4 additions & 3 deletions language-server/dm/priorityManager.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,8 @@
(* This filecontains the global views of priorities *)

let lsp_message = -3
let feedback = -4
let lsp_message = -5
let feedback = -6
let parsing = -4
let execution = -3
let proof_view = -2
let move_cursor = -5
let move_cursor = -7
Loading
Loading