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.

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

[fleche] Support Abort All. #774

Merged
merged 1 commit into from
Jun 8, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
2 changes: 2 additions & 0 deletions CHANGES.md
Original file line number Diff line number Diff line change
Expand Up @@ -49,6 +49,8 @@
(@ejgallego, Diego Rivera, #772)
- [hover] New option `show_universes_on_hover` that will display
universe data on hover (@ejgallego, @SkySkimmer, #666)
- [fleche] Support meta-command `Abort All` (@ejgallego, #, fixes
#550)

# coq-lsp 0.1.10: Hasta el 40 de Mayo _en effect_...
----------------------------------------------------
Expand Down
6 changes: 6 additions & 0 deletions coq/ast.ml
Original file line number Diff line number Diff line change
Expand Up @@ -77,6 +77,9 @@ module Meta = struct
| Back of int
| ResetName of Names.lident
| ResetInitial
| AbortAll
(* Not supported, but actually easy if we want | VernacRestart | VernacUndo
_ | VernacUndoTo _ *)
[@@deriving hash, compare]
end

Expand Down Expand Up @@ -104,6 +107,9 @@ module Meta = struct
| { expr = VernacSynPure (VernacBack num); control; attrs } ->
let command = Command.Back num in
Some { command; loc; attrs; control }
| { expr = VernacSynPure VernacAbortAll; control; attrs } ->
let command = Command.AbortAll in
Some { command; loc; attrs; control }
| _ -> None)
end

Expand Down
1 change: 1 addition & 0 deletions coq/ast.mli
Original file line number Diff line number Diff line change
Expand Up @@ -40,6 +40,7 @@ module Meta : sig
| Back of int
| ResetName of Names.lident
| ResetInitial
| AbortAll
end

type t =
Expand Down
7 changes: 6 additions & 1 deletion coq/state.ml
Original file line number Diff line number Diff line change
Expand Up @@ -87,7 +87,7 @@ let lemmas ~st = st.Vernacstate.interp.lemmas
let program ~st =
NeList.head st.Vernacstate.interp.program |> Declare.OblState.view

let drop_proofs ~st =
let drop_proof ~st =
let open Vernacstate in
let interp =
{ st.interp with
Expand All @@ -99,6 +99,11 @@ let drop_proofs ~st =
in
{ st with interp }

let drop_all_proofs ~st =
let open Vernacstate in
let interp = { st.interp with lemmas = None } in
{ st with interp }

let in_state ~token ~st ~f a =
let f a =
Vernacstate.unfreeze_full_state st;
Expand Down
7 changes: 5 additions & 2 deletions coq/state.mli
Original file line number Diff line number Diff line change
Expand Up @@ -29,8 +29,11 @@ val in_stateM :
-> 'a
-> ('b, Loc.t) Protect.E.t

(** Drop the proofs from the state *)
val drop_proofs : st:t -> t
(** Drop the top proof from the state *)
val drop_proof : st:t -> t

(** Drop all proofs from the state *)
val drop_all_proofs : st:t -> t

(** Fully admit an ongoing proof *)
val admit : token:Limits.Token.t -> st:t -> (t, Loc.t) Protect.E.t
Expand Down
8 changes: 8 additions & 0 deletions examples/MetaCommands.v
Original file line number Diff line number Diff line change
Expand Up @@ -34,5 +34,13 @@ About muu.
About foo.
About bar.

Lemma foo : True.
Lemma bar : False.
Abort All.

Lemma foo : True. now auto. Qed.

Print foo.



7 changes: 5 additions & 2 deletions fleche/doc.ml
Original file line number Diff line number Diff line change
Expand Up @@ -660,7 +660,7 @@ let interp_and_info ~token ~st ~files ast =
| Some ast -> Memo.Require.evalS ~token (st, files, ast)

(* Support for meta-commands, a bit messy, but cool in itself *)
let search_node ~command ~doc =
let search_node ~command ~doc ~st =
let nstats (node : Node.t option) =
Option.cata
(fun (node : Node.t) -> Option.default Memo.Stats.zero node.info.stats)
Expand Down Expand Up @@ -689,6 +689,9 @@ let search_node ~command ~doc =
let node = Option.default node node.prev in
(Coq.Protect.E.ok node.state, nstats (Some node)))
| ResetInitial -> (Coq.Protect.E.ok doc.root, nstats None)
| AbortAll ->
let st = Coq.State.drop_all_proofs ~st in
(Coq.Protect.E.ok st, nstats None)

let interp_and_info ~token ~st ~files ~doc ast =
match Coq.Ast.Meta.extract ast with
Expand All @@ -698,7 +701,7 @@ let interp_and_info ~token ~st ~files ~doc ast =
spending on error recovery and meta stuff, we should record that time
actually at some point too. In this case, maybe we could recover the
cache hit from the original node? *)
search_node ~command ~doc
search_node ~command ~doc ~st

let interp_and_info ~token ~parsing_time ~st ~files ~doc ast =
let res, stats = interp_and_info ~token ~st ~files ~doc ast in
Expand Down
Loading