Skip to content

Commit

Permalink
Add support for delegated proofs.
Browse files Browse the repository at this point in the history
  • Loading branch information
@rtetley
rtetley committed May 31, 2024
1 parent f56d35a commit 02fb4bf
Show file tree
Hide file tree
Showing 3 changed files with 85 additions and 58 deletions.
17 changes: 15 additions & 2 deletions language-server/dm/documentManager.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -63,7 +63,10 @@ let inject_em_events events = List.map inject_em_event events
type events = event Sel.Event.t list

let print_exec_overview st =
let {processing; processed} = st.overview in
let {processing; processed; prepared} = st.overview in
log @@ "--------- Prepared ranges ---------";
List.iter (fun r -> log @@ Range.to_string r) prepared;
log @@ "-------------------------------------";
log @@ "--------- Processing ranges ---------";
List.iter (fun r -> log @@ Range.to_string r) processing;
log @@ "-------------------------------------";
Expand Down Expand Up @@ -362,7 +365,17 @@ let handle_event ev st =
let overview = ExecutionManager.update_overview task todo execution_state st.document st.overview in
(Some {st with execution_state; overview}, inject_em_events events @ [event])
| ExecutionManagerEvent ev ->
let execution_state_update, events = ExecutionManager.handle_event ev st.execution_state in
let id, execution_state_update, events = ExecutionManager.handle_event ev st.execution_state in
let st =
match (id, execution_state_update) with
| Some id, Some exec_st ->
let overview = ExecutionManager.update_processed id exec_st st.document st.overview in
{st with overview}
| Some id, None ->
let overview = ExecutionManager.update_processed id st.execution_state st.document st.overview in
{st with overview}
| _, _ -> st
in
(Option.map (fun execution_state -> {st with execution_state}) execution_state_update, inject_em_events events)

let get_proof st diff_mode pos =
Expand Down
123 changes: 68 additions & 55 deletions language-server/dm/executionManager.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -240,7 +240,7 @@ let rec insert_or_merge_range r = function

let rec remove_or_truncate_range r = function
| [] -> []
| r1 :: l ->
| r1 :: l -> log @@ "RANGES"; log @@ "R1: " ^ Range.to_string r1; log @@ "R: " ^ Range.to_string r;
if Position.compare r1.Range.start r.Range.start == 0 &&
Position.compare r1.Range.end_ r.Range.end_ == 0
then
Expand All @@ -251,60 +251,72 @@ let rec remove_or_truncate_range r = function
else
r1 :: (remove_or_truncate_range r l)

let update_processed task state processing processed prepared document =
match task with
| PDelegate {opener_id; terminator_id; } ->
let opener_range = Document.range_of_id_with_blank_space document opener_id in
let terminator_range = Document.range_of_id_with_blank_space document terminator_id in
let range = Range.create ~end_:terminator_range.end_ ~start:opener_range.start in
begin match SM.find terminator_id state.of_sentence with
| (s, _) ->
begin match s with
| Done s ->
begin match s with
| Success _ ->
insert_or_merge_range range processed, remove_or_truncate_range range processing, remove_or_truncate_range range prepared
| Error _ ->
processed, remove_or_truncate_range range processing, remove_or_truncate_range range prepared
end
| _ -> processed, processing, prepared
end
| exception Not_found ->
log @@ "Trying to get overview with non-existing state id " ^ Stateid.to_string terminator_id;
processed, processing, prepared
let update_processed_as_Done s range overview =
let {prepared; processing; processed} = overview in
match s with
| Success _ ->
log @@ "INSERTING TO PROCESSED";
let processed = insert_or_merge_range range processed in
log @@ "TRUNCATING FROM PROCESSING";
let processing = remove_or_truncate_range range processing in
log @@ "TRUNCATING FROM PREPARED";
let prepared = remove_or_truncate_range range prepared in
{prepared; processing; processed}
| Error _ ->
log @@ "TRUNCATING FROM PROCESSING";
let processing = remove_or_truncate_range range processing in
log @@ "TRUNCATING FROM PREPARED";
let prepared = remove_or_truncate_range range prepared in
{prepared; processing; processed}

let update_processed id state document overview =
log @@ "UPDATING PROCESSED";
let range = Document.range_of_id_with_blank_space document id in
match SM.find id state.of_sentence with
| (s, _) ->
begin match s with
| Done s -> update_processed_as_Done s range overview
| _ -> assert false (* delegated sentences born as such, cannot become it later *)
end
| PSkip { id } | PExec { id } | PQuery { id } ->
let range = Document.range_of_id_with_blank_space document id in
match SM.find id state.of_sentence with
| (s, _) ->
begin match s with
| Done s ->
begin match s with
| Success _ ->
insert_or_merge_range range processed, remove_or_truncate_range range processing, remove_or_truncate_range range prepared
| Error _ ->
processed, remove_or_truncate_range range processing, remove_or_truncate_range range prepared
end
| _ -> processed, processing, prepared
end
| exception Not_found ->
log @@ "Trying to get overview with non-existing state id " ^ Stateid.to_string id;
processed, processing, prepared
| exception Not_found ->
log @@ "Trying to get overview with non-existing state id " ^ Stateid.to_string id;
overview

let update_processing task processing prepared document =
log @@ "UPDATING PROCESSING";
match task with
| PDelegate { opener_id; terminator_id; } ->
let opener_range = Document.range_of_id_with_blank_space document opener_id in
let terminator_range = Document.range_of_id_with_blank_space document terminator_id in
let range = Range.create ~end_:terminator_range.end_ ~start:opener_range.start in
insert_or_merge_range range processing, remove_or_truncate_range range prepared
| PDelegate { opener_id; terminator_id; tasks } ->
let proof_opener_id = match tasks with
| [] -> opener_id
| (PSkip { id } | PExec { id } | PQuery { id }) :: _ -> id
| PDelegate _ :: _ -> assert false
in
let proof_closer_id = match List.rev tasks with
| [] -> terminator_id
| (PSkip { id } | PExec { id } | PQuery { id }) :: _ -> id
| PDelegate _ :: _ -> assert false
in
let proof_begin_range = Document.range_of_id_with_blank_space document proof_opener_id in
let proof_end_range = Document.range_of_id_with_blank_space document proof_closer_id in
let range = Range.create ~end_:proof_end_range.end_ ~start:proof_begin_range.start in
log @@ "DELEGATED JOB RANGE: " ^ Range.to_string range;
log @@ "TRUNCATING FROM PREPARED";
(* When a job is delegated we shouldn't merge ranges (to get the proper progress report) *)
List.append processing [ range ], remove_or_truncate_range range prepared
| PSkip { id } | PExec { id } | PQuery { id } ->
let range = Document.range_of_id_with_blank_space document id in
log @@ "TRUNCATING FROM PREPARED";
insert_or_merge_range range processing, remove_or_truncate_range range prepared

let update_overview task todo state document overview =
let { processing; processed; prepared } = overview in
let processed, processing, prepared = update_processed task state processing processed prepared document in
let {processed; processing; prepared} =
match task with
| PDelegate { terminator_id } ->
let range = Document.range_of_id_with_blank_space document terminator_id in
update_processed_as_Done (Success None) range overview
| PSkip { id } | PExec { id } | PQuery { id } ->
update_processed id state document overview
in
let processing, prepared = match todo with
| [] -> processing, prepared
| next :: _ -> update_processing next processing prepared document in
Expand Down Expand Up @@ -366,28 +378,29 @@ let handle_feedback id fb state =
let handle_event event state =
match event with
| LocalFeedback (q,_,id,fb) ->
Some (handle_feedback id fb state), [local_feedback q]
None, Some (handle_feedback id fb state), [local_feedback q]
| ProofWorkerEvent event ->
let update, events = ProofWorker.handle_event event in
let state =
let state, id =
match update with
| None -> None
| None -> None, None
| Some (ProofJob.AppendFeedback(_,id,fb)) ->
Some (handle_feedback id fb state)
Some (handle_feedback id fb state), None
| Some (ProofJob.UpdateExecStatus(id,v)) ->
match SM.find id state.of_sentence, v with
| (Delegated (_,completion), fl), _ ->
Option.default ignore completion v;
Some (update_all id (Done v) fl state)
Some (update_all id (Done v) fl state), Some id
| (Done (Success s), fl), Error (err,_) ->
(* This only happens when a Qed closing a delegated proof
receives an updated by a worker saying that the proof is
not completed *)
Some (update_all id (Done (Error (err,s))) fl state)
| (Done _, _), _ -> None
| exception Not_found -> None (* TODO: is this possible? *)
Some (update_all id (Done (Error (err,s))) fl state), Some id
| (Done _, _), _ -> None, Some id
| exception Not_found -> None, None (* TODO: is this possible? *)
in
inject_proof_events state events
let state, events = inject_proof_events state events in
id, state, events

let find_fulfilled_opt x m =
try
Expand Down
3 changes: 2 additions & 1 deletion language-server/dm/executionManager.mli
View file
Original file line number Diff line number Diff line change
Expand Up @@ -66,7 +66,7 @@ val get_initial_context : state -> Evd.evar_map * Environ.env
val get_vernac_state : state -> sentence_id -> Vernacstate.t option

(** Events for the main loop *)
val handle_event : event -> state -> (state option * events)
val handle_event : event -> state -> (sentence_id option * 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 *)
Expand All @@ -75,6 +75,7 @@ val build_tasks_for : Scheduler.schedule -> state -> sentence_id -> Vernacstate.
val execute : state -> Vernacstate.t * events * bool -> prepared_task -> (state * Vernacstate.t * events * bool)

val update_overview : prepared_task -> prepared_task list -> state -> Document.document -> exec_overview -> exec_overview
val update_processed : sentence_id -> state -> Document.document -> exec_overview -> exec_overview

(** Coq toplevels for delegation without fork *)
module ProofWorkerProcess : sig
Expand Down

0 comments on commit 02fb4bf

Please sign in to comment.