diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index 78374037..6427acda 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -114,8 +114,8 @@ jobs:
       - name: 🐫🐪🐫 Get dependencies
         run: |
           opam exec -- make opam-deps
-          opam pin add js_of_ocaml-compiler https://github.com/ejgallego/js_of_ocaml.git#fix_build_fs_target -y
-          opam pin add js_of_ocaml https://github.com/ejgallego/js_of_ocaml.git#fix_build_fs_target -y
+          opam pin add js_of_ocaml-compiler --dev -y
+          opam pin add js_of_ocaml --dev -y
           opam install zarith_stubs_js js_of_ocaml-ppx -y
 
       - name: 💉💉💉 Patch Coq
diff --git a/CHANGES.md b/CHANGES.md
index de4884e1..02225c39 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,5 +1,12 @@
-# unreleased
-------------
+# coq-lsp 0.2.2: To Virtual or not To Virtual
+---------------------------------------------
+
+ - [vscode] Expand selectors to include `vscode-vfs://` URIs used in
+   `github.dev`, document limited virtual workspace support in
+   `package.json` (@ejgallego, #849)
+
+# coq-lsp 0.2.1: Click !
+------------------------
 
  - [deps] Bump toolchain so minimal `ppxlib` is 0.26, in order to fix
    some `ppx_import` oddities. This means our lower bound for the Jane
@@ -34,6 +41,18 @@
    info that is needed is at hand. It could also be tried to set the
    build target for immediate requests to the view hint, but we should
    see some motivation for that (@ejgallego, #841)
+ - [lsp] [diagnostics] (! breaking change) change type of diagnostics
+   extra data from list to named record (@ejgallego, #843)
+ - [lsp] Implement support for `textDocument/codeAction`. For now, we
+   support Coq's 8.21 `quickFix` data (@ejgallego, #840, #843, #845)
+ - [petanque] Fix bug for detection of proof finished in deep stacks
+   (@ejgallego, @gbdrt, #847)
+ - [goals request] allow multiple Coq sentences in `command`. This is
+   backwards compatible in the case that commands do not error, and
+   users were sending just one command. (@ejgallego, #823, thanks to
+   CoqPilot devs and G. Baudart for feedback)
+ - [goals request] (! breaking) fail the request if the commands in
+   `command` fail (@ejgallego, #823)
 
 # coq-lsp 0.2.0: From Green to Blue
 -----------------------------------
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index 8255adc7..908bf9cc 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -411,7 +411,7 @@ The checklist for the release as of today is the following:
 
 The above can be done with:
 ```
-export COQLSPV=0.2.0
+export COQLSPV=0.2.1
 git checkout main  && make                    && dune-release tag ${COQLSPV}
 git checkout v8.20 && git merge main  && make && dune-release tag ${COQLSPV}+8.20 && dune-release
 git checkout v8.19 && git merge v8.20  && make && dune-release tag ${COQLSPV}+8.19 && dune-release
diff --git a/Makefile b/Makefile
index 1f0e683b..3c65443c 100644
--- a/Makefile
+++ b/Makefile
@@ -160,6 +160,9 @@ _LIBROOT=$(shell opam var lib)
 ifdef VENDORED_SETUP
 _CCROOT=_build/install/default/lib/coq-core
 else
+# We could use `opam var lib` as well here, as the idea to rely on
+# coqc was to avoid having a VENDORED_SETUP variable, which we now
+# have anyways.
 _CCROOT=$(shell coqc -where)/../coq-core
 endif
 
@@ -170,8 +173,8 @@ controller-js/coq-fs-core.js: coq_boot
 	for i in $$(find $(_CCROOT)/plugins -name *.cma); do js_of_ocaml --dynlink $$i; done
 	for i in $$(find _build/install/default/lib/coq-lsp/serlib -wholename */*.cma); do js_of_ocaml --dynlink $$i; done
 	js_of_ocaml build-fs -o controller-js/coq-fs-core.js \
-	    $$(find $(_CCROOT)/                          \( -wholename '*/plugins/*/*.js' -or -wholename '*/META' \) -printf "%p:/static/lib/%p ") \
-	    $$(find _build/install/default/lib/coq-lsp/  \( -wholename '*/serlib/*/*.js'  -or -wholename '*/META' \) -printf "%p:/static/lib/%p ") \
+	    $$(find $(_CCROOT)/                          \( -wholename '*/plugins/*/*.js' -or -wholename '*/META' \) -printf "%p:/static/lib/coq-core/%P ") \
+	    $$(find _build/install/default/lib/coq-lsp/  \( -wholename '*/serlib/*/*.js'  -or -wholename '*/META' \) -printf "%p:/static/lib/coq-lsp/%P ") \
 	    ./etc/META.threads:/static/lib/threads/META \
 	    $$(find $(_LIBROOT) -wholename '*/str/META'                 -printf "%p:/static/lib/%P ") \
 	    $$(find $(_LIBROOT) -wholename '*/seq/META'                 -printf "%p:/static/lib/%P ") \
@@ -198,6 +201,11 @@ controller-js/coq-fs-core.js: coq_boot
 	    # These libs are actually linked, so no cma is needed.
 	    # $$(find $(_LIBROOT) -wholename '*/zarith/*.cma'         -printf "%p:/static/lib/%P " -or -wholename '*/zarith/META'         -printf "%p:/static/lib/%P ")
 
+.PHONY: check-js-fs-sanity
+check-js-fs-sanity: controller-js/coq-fs-core.js js
+	cat _build/default/controller-js/coq-fs.js | grep '/static/'
+	cat controller-js/coq-fs-core.js | grep '/static/'
+
 # Serlib plugins require:
 #   ppx_compare.runtime-lib
 #   ppx_deriving.runtime
diff --git a/controller-js/README.md b/controller-js/README.md
index 244cc00c..885b76f6 100644
--- a/controller-js/README.md
+++ b/controller-js/README.md
@@ -62,7 +62,7 @@ extension + Coq build.
 As of Feb 2023, due to security restrictions, you may need to either:
 
  - pass `--enable-coi` to `code`
- - use ``?enable-coi=` in the vscode dev setup
+ - append `?vscode-coi` in the vscode dev setup URL
 
 in order to have interruptions (`SharedBufferArray`) working.
 
diff --git a/controller-js/coq_lsp_worker.ml b/controller-js/coq_lsp_worker.ml
index 57d82577..d1595486 100644
--- a/controller-js/coq_lsp_worker.ml
+++ b/controller-js/coq_lsp_worker.ml
@@ -14,42 +14,6 @@ module LSP = Lsp.Base
 open Js_of_ocaml
 open Controller
 
-let rec obj_to_json (cobj : < .. > Js.t) : Yojson.Safe.t =
-  let open Js in
-  let open Js.Unsafe in
-  let typeof_cobj = to_string (typeof cobj) in
-  match typeof_cobj with
-  | "string" -> `String (to_string @@ coerce cobj)
-  | "boolean" -> `Bool (to_bool @@ coerce cobj)
-  | "number" -> `Int (int_of_float @@ float_of_number @@ coerce cobj)
-  | _ ->
-    if instanceof cobj array_empty then
-      `List Array.(to_list @@ map obj_to_json @@ to_array @@ coerce cobj)
-    else if instanceof cobj Typed_array.arrayBuffer then
-      `String (Typed_array.String.of_arrayBuffer @@ coerce cobj)
-    else if instanceof cobj Typed_array.uint8Array then
-      `String (Typed_array.String.of_uint8Array @@ coerce cobj)
-    else
-      let json_string = Js.to_string (Json.output cobj) in
-      Yojson.Safe.from_string json_string
-
-let rec json_to_obj (cobj : < .. > Js.t) (json : Yojson.Safe.t) : < .. > Js.t =
-  let open Js.Unsafe in
-  let ofresh j = json_to_obj (obj [||]) j in
-  match json with
-  | `Bool b -> coerce @@ Js.bool b
-  | `Null -> pure_js_expr "null"
-  | `Assoc l ->
-    List.iter (fun (p, js) -> set cobj p (ofresh js)) l;
-    cobj
-  | `List l -> Array.(Js.array @@ map ofresh (of_list l))
-  | `Float f -> coerce @@ Js.number_of_float f
-  | `String s -> coerce @@ Js.string s
-  | `Int m -> coerce @@ Js.number_of_float (float_of_int m)
-  | `Intlit s -> coerce @@ Js.number_of_float (float_of_string s)
-  | `Tuple t -> Array.(Js.array @@ map ofresh (of_list t))
-  | `Variant (_, _) -> pure_js_expr "undefined"
-
 let findlib_conf = "\ndestdir=\"/static/lib\"path=\"/static/lib\""
 let findlib_path = "/static/lib/findlib.conf"
 
@@ -65,7 +29,7 @@ let setup_std_printers () =
 
 let post_message (msg : Lsp.Base.Message.t) =
   let json = Lsp.Base.Message.to_yojson msg in
-  let js = json_to_obj (Js.Unsafe.obj [||]) json in
+  let js = Jsso.json_to_obj json in
   Worker.post_message js
 
 type opaque
@@ -74,20 +38,29 @@ external interrupt_setup : opaque (* Uint32Array *) -> unit = "interrupt_setup"
 
 let interrupt_is_setup = ref false
 
+let log_interrupt () =
+  let lvl, message =
+    if not !interrupt_is_setup then
+      (* Maybe set one step mode, but usually that's done in the client. *)
+      (Lsp.Io.Lvl.Error, "Interrupt is not setup: Functionality will suffer")
+    else (Lsp.Io.Lvl.Info, "Interrupt setup: [Control.interrupt] backend")
+  in
+  Lsp.Io.logMessage ~lvl ~message
+
 let parse_msg msg =
-  if Js.instanceof msg Js.array_length then (
+  if Js.instanceof msg Js.array_empty then (
     let _method_ = Js.array_get msg 0 in
     let handle = Js.array_get msg 1 |> Obj.magic in
     interrupt_setup handle;
     interrupt_is_setup := true;
     Error "processed interrupt_setup")
-  else obj_to_json msg |> Lsp.Base.Message.of_yojson
+  else Jsso.obj_to_json msg |> Lsp.Base.Message.of_yojson
 
 let on_msg msg =
   match parse_msg msg with
   | Error _ ->
-    Lsp.Io.logMessage ~lvl:Lsp.Io.Lvl.Error
-      ~message:"Error in JSON RPC Message Parsing"
+    let message = "Error in JSON RPC Message Parsing" in
+    Lsp.Io.logMessage ~lvl:Lsp.Io.Lvl.Error ~message
   | Ok msg ->
     (* Lsp.Io.trace "interrupt_setup" (string_of_bool !interrupt_is_setup); *)
     Lsp_core.enqueue_message msg
@@ -112,7 +85,9 @@ let rec process_queue ~state () =
 
 let on_init ~io ~root_state ~cmdline ~debug msg =
   match parse_msg msg with
-  | Error _ -> ()
+  | Error _ ->
+    (* This is called one for interrupt setup *)
+    ()
   | Ok msg -> (
     match
       Lsp_core.lsp_init_process ~ofn:post_message ~io ~cmdline ~debug msg
@@ -120,6 +95,7 @@ let on_init ~io ~root_state ~cmdline ~debug msg =
     | Lsp_core.Init_effect.Exit -> (* XXX: bind to worker.close () *) ()
     | Lsp_core.Init_effect.Loop -> ()
     | Lsp_core.Init_effect.Success workspaces ->
+      log_interrupt ();
       Worker.set_onmessage on_msg;
       let default_workspace = Coq.Workspace.default ~debug ~cmdline in
       let state =
diff --git a/controller-js/jsso.ml b/controller-js/jsso.ml
new file mode 100644
index 00000000..ec653d43
--- /dev/null
+++ b/controller-js/jsso.ml
@@ -0,0 +1,57 @@
+open Js_of_ocaml
+
+let rec obj_to_json (cobj : < .. > Js.t) : Yojson.Safe.t =
+  let open Js in
+  let open Js.Unsafe in
+  let typeof_cobj = to_string (typeof cobj) in
+  match typeof_cobj with
+  | "string" -> `String (to_string @@ coerce cobj)
+  | "boolean" -> `Bool (to_bool @@ coerce cobj)
+  | "number" -> `Int (int_of_float @@ float_of_number @@ coerce cobj)
+  | _ ->
+    if instanceof cobj array_empty then
+      `List Array.(to_list @@ map obj_to_json @@ to_array @@ coerce cobj)
+    else if instanceof cobj Typed_array.arrayBuffer then
+      `String (Typed_array.String.of_arrayBuffer @@ coerce cobj)
+    else if instanceof cobj Typed_array.uint8Array then
+      `String (Typed_array.String.of_uint8Array @@ coerce cobj)
+      (* Careful in case we miss cases here, what about '{}' for example, we
+         should also stop on functions? *)
+    else if instanceof cobj Unsafe.global##._Object then
+      Js.array_map
+        (fun key -> (Js.to_string key, obj_to_json (Js.Unsafe.get cobj key)))
+        (Js.object_keys cobj)
+      |> Js.to_array |> Array.to_list
+      |> fun al -> `Assoc al
+    else if Js.Opt.(strict_equals (some cobj) null) then `Null
+    else if Js.Optdef.(strict_equals (def cobj) undefined) then (
+      Firebug.console##info "undefined branch!!!!";
+      `Null)
+    else (
+      Firebug.console##error "failure in coq_lsp_worker:obj_to_json";
+      Firebug.console##error cobj;
+      Firebug.console##error (Json.output cobj);
+      raise (Failure "coq_lsp_worker:obj_to_json"))
+
+(* Old code, which is only useful for debug *)
+(* let json_string = Js.to_string (Json.output cobj) in *)
+(* Yojson.Safe.from_string json_string *)
+
+let rec json_to_obj (cobj : < .. > Js.t) (json : Yojson.Safe.t) : < .. > Js.t =
+  let open Js.Unsafe in
+  let ofresh j = json_to_obj (obj [||]) j in
+  match json with
+  | `Bool b -> coerce @@ Js.bool b
+  | `Null -> pure_js_expr "null"
+  | `Assoc l ->
+    List.iter (fun (p, js) -> set cobj p (ofresh js)) l;
+    coerce @@ cobj
+  | `List l -> coerce @@ Array.(Js.array @@ map ofresh (of_list l))
+  | `Float f -> coerce @@ Js.number_of_float f
+  | `String s -> coerce @@ Js.string s
+  | `Int m -> coerce @@ Js.number_of_float (float_of_int m)
+  | `Intlit s -> coerce @@ Js.number_of_float (float_of_string s)
+  | `Tuple t -> coerce @@ Array.(Js.array @@ map ofresh (of_list t))
+  | `Variant (_, _) -> pure_js_expr "undefined"
+
+let json_to_obj json = json_to_obj (Js.Unsafe.obj [||]) json
diff --git a/controller-js/jsso.mli b/controller-js/jsso.mli
new file mode 100644
index 00000000..f7620fef
--- /dev/null
+++ b/controller-js/jsso.mli
@@ -0,0 +1,5 @@
+open Js_of_ocaml
+
+(* Object to Yojson converter *)
+val obj_to_json : < .. > Js.t -> Yojson.Safe.t
+val json_to_obj : Yojson.Safe.t -> < .. > Js.t
diff --git a/controller/lsp_core.ml b/controller/lsp_core.ml
index eb33483e..5479d96e 100644
--- a/controller/lsp_core.ml
+++ b/controller/lsp_core.ml
@@ -416,6 +416,20 @@ let do_document = do_document_request_maybe ~handler:Rq_document.request
 let do_save_vo = do_document_request_maybe ~handler:Rq_save.request
 let do_lens = do_document_request_maybe ~handler:Rq_lens.request
 
+(* could be smarter *)
+let do_action ~params =
+  let range = field "range" params in
+  match Lsp.JLang.Diagnostic.Range.of_yojson range with
+  | Ok range ->
+    let range = Lsp.JLang.Diagnostic.Range.vnoc range in
+    do_immediate ~params ~handler:(Rq_action.request ~range)
+  | Error err ->
+    (* XXX: We really need to fix the parsing error handling in lsp_core, we got
+       it right in petanque haha *)
+    (* JSON-RPC Parse error (EJGA: is this the right code) *)
+    let code = -32700 in
+    Rq.Action.error (code, err)
+
 let do_cancel ~ofn_rq ~params =
   let id = int_field "id" params in
   let code = -32800 in
@@ -584,6 +598,7 @@ let dispatch_request ~token ~method_ ~params : Rq.Action.t =
   | "textDocument/hover" -> do_hover ~params
   | "textDocument/codeLens" -> do_lens ~params
   | "textDocument/selectionRange" -> do_selectionRange ~params
+  | "textDocument/codeAction" -> do_action ~params
   (* Proof-specific stuff *)
   | "proof/goals" -> do_goals ~params
   (* Proof-specific stuff *)
diff --git a/controller/request.ml b/controller/request.ml
index 3ea2fac4..27abf50e 100644
--- a/controller/request.ml
+++ b/controller/request.ml
@@ -26,7 +26,7 @@ module R = struct
 
   let print_err ~name e =
     match e with
-    | Coq.Protect.Error.Anomaly (_loc, msg) | User (_loc, msg) ->
+    | Coq.Protect.Error.Anomaly { msg; _ } | User { msg; _ } ->
       Format.asprintf "Error in %s request: %a" name Pp.pp_with msg
 
   let of_execution ~name ~f x : t =
diff --git a/controller/rq_action.ml b/controller/rq_action.ml
new file mode 100644
index 00000000..8e956399
--- /dev/null
+++ b/controller/rq_action.ml
@@ -0,0 +1,65 @@
+let point_lt { Lang.Point.line = l1; Lang.Point.character = c1; offset = _ }
+    { Lang.Point.line = l2; Lang.Point.character = c2; offset = _ } =
+  l1 < l2 || (l1 = l2 && c1 < c2)
+
+let point_gt { Lang.Point.line = l1; Lang.Point.character = c1; offset = _ }
+    { Lang.Point.line = l2; Lang.Point.character = c2; offset = _ } =
+  l1 > l2 || (l1 = l2 && c1 > c2)
+
+(* To move to doc.ml *)
+let filter_map_range ~range ~nodes ~f =
+  let rec aux (nodes : Fleche.Doc.Node.t list) acc =
+    match nodes with
+    | [] -> List.rev acc
+    | node :: nodes -> (
+      let open Lang.Range in
+      let nrange = node.range in
+      if point_lt nrange.end_ range.start then aux nodes acc
+      else if point_gt nrange.start range.end_ then List.rev acc
+      else
+        (* Node in scope *)
+        match f node with
+        | Some res -> aux nodes (res :: acc)
+        | None -> aux nodes acc)
+  in
+  aux nodes []
+
+(* util *)
+let filter_map_cut f l =
+  match List.filter_map f l with
+  | [] -> None
+  | res -> Some res
+
+(* Return list of pairs of diags, qf *)
+let get_qf (d : Lang.Diagnostic.t) : _ option =
+  Option.bind d.data (function
+    | { Lang.Diagnostic.Data.quickFix = Some qf; _ } -> Some (d, qf)
+    | _ -> None)
+
+let get_qfs ~range (doc : Fleche.Doc.t) =
+  let f { Fleche.Doc.Node.diags; _ } = filter_map_cut get_qf diags in
+  filter_map_range ~range ~nodes:doc.nodes ~f |> List.concat
+
+let request ~range ~token:_ ~(doc : Fleche.Doc.t) =
+  let kind = Some "quickfix" in
+  let isPreferred = Some true in
+  let qf = get_qfs ~range doc in
+  let bf (d, qf) =
+    List.map
+      (fun { Lang.Qf.range; newText } ->
+        let oldText =
+          Fleche.Contents.extract_raw ~contents:doc.contents ~range
+        in
+        let title = Format.asprintf "Replace `%s` by `%s`" oldText newText in
+        let diagnostics = [ d ] in
+        let qf = [ Lsp.Workspace.TextEdit.{ range; newText } ] in
+        let changes = [ (doc.uri, qf) ] in
+        let edit = Some Lsp.Workspace.WorkspaceEdit.{ changes } in
+        Lsp.Core.CodeAction.{ title; kind; diagnostics; isPreferred; edit })
+      qf
+  in
+  List.concat_map bf qf
+
+let request ~range ~token ~(doc : Fleche.Doc.t) =
+  let res = request ~range ~token ~doc in
+  Ok (`List (List.map Lsp.Core.CodeAction.to_yojson res))
diff --git a/controller/rq_action.mli b/controller/rq_action.mli
new file mode 100644
index 00000000..959b0a03
--- /dev/null
+++ b/controller/rq_action.mli
@@ -0,0 +1 @@
+val request : range:Lang.Range.t -> Request.document
diff --git a/controller/rq_goals.ml b/controller/rq_goals.ml
index 2299de66..e6b5a93c 100644
--- a/controller/rq_goals.ml
+++ b/controller/rq_goals.ml
@@ -6,9 +6,8 @@
 (************************************************************************)
 
 (* Replace by ppx when we can print goals properly in the client *)
-let mk_message (range, level, text) =
-  let level = Lang.Diagnostic.Severity.to_int level in
-  Lsp.JFleche.Message.{ range; level; text }
+let mk_message (level, { Coq.Message.Payload.range; msg; quickFix = _ }) =
+  Lsp.JFleche.Message.{ range; level; text = msg }
 
 let mk_messages node =
   Option.map Fleche.Doc.Node.messages node
@@ -32,25 +31,10 @@ let pp ~pp_format pp =
   | Pp -> Lsp.JCoq.Pp.to_yojson pp
   | Str -> `String (Pp.string_of_ppcmds pp)
 
-let parse ~token ~loc tac st =
-  let str = Gramlib.Stream.of_string tac in
-  let str = Coq.Parsing.Parsable.make ?loc str in
-  Coq.Parsing.parse ~token ~st str
-
-let parse_and_execute_in ~token ~loc tac st =
-  let open Coq.Protect.E.O in
-  let* ast = parse ~token ~loc tac st in
-  match ast with
-  | Some ast -> Fleche.Memo.Interp.eval ~token (st, ast)
-  (* On EOF we return the previous state, the command was the empty string or a
-     comment *)
-  | None -> Coq.Protect.E.ok st
-
 let run_pretac ~token ~loc ~st pretac =
   match pretac with
   | None -> Coq.Protect.E.ok st
-  | Some tac ->
-    Coq.State.in_stateM ~token ~st ~f:(parse_and_execute_in ~token ~loc tac) st
+  | Some tac -> Fleche.Doc.run ~token ?loc ~st tac
 
 let get_goal_info ~token ~doc ~point ~mode ~pretac () =
   let open Fleche in
diff --git a/controller/rq_init.ml b/controller/rq_init.ml
index 3b008cd6..b5f7bd9a 100644
--- a/controller/rq_init.ml
+++ b/controller/rq_init.ml
@@ -117,7 +117,7 @@ let do_initialize ~io ~params =
     [ ("textDocumentSync", `Int 1)
     ; ("documentSymbolProvider", `Bool true)
     ; ("hoverProvider", `Bool true)
-    ; ("codeActionProvider", `Bool false)
+    ; ("codeActionProvider", `Bool true)
     ; ( "completionProvider"
       , `Assoc
           [ ("triggerCharacters", `List [ `String "\\" ])
diff --git a/coq/init.ml b/coq/init.ml
index 8d9358c9..2bee2303 100644
--- a/coq/init.ml
+++ b/coq/init.ml
@@ -36,13 +36,19 @@ let coq_lvl_to_severity (lvl : Feedback.level) =
   | Feedback.Warning -> warning
   | Feedback.Error -> error
 
-let add_message lvl loc msg q =
+(* let qf_of_coq qf = let range = Quickfix.loc qf in let newText = Quickfix.pp
+   qf |> Pp.string_of_ppcmds in { Lang.Qf.range; newText } *)
+
+let add_message lvl range _qf msg q =
   let lvl = coq_lvl_to_severity lvl in
-  q := (loc, lvl, msg) :: !q
+  (* let quickFix = if qf = [] then None else Some (List.map qf_of_coq qf) in *)
+  let quickFix = None in
+  let payload = Message.Payload.make ?range ?quickFix msg in
+  q := (lvl, payload) :: !q
 
 let mk_fb_handler q Feedback.{ contents; _ } =
   match contents with
-  | Message (lvl, loc, msg) -> add_message lvl loc msg q
+  | Message (lvl, loc, msg) -> add_message lvl loc None msg q
   | _ -> ()
 
 let coq_init opts =
diff --git a/coq/message.ml b/coq/message.ml
index dfba4ccd..71557391 100644
--- a/coq/message.ml
+++ b/coq/message.ml
@@ -1,2 +1,18 @@
 (** Messages from Coq *)
-type 'l t = 'l option * Lang.Diagnostic.Severity.t * Pp.t
+module Payload = struct
+  type 'l t =
+    { range : 'l option
+    ; quickFix : 'l Lang.Qf.t list option
+    ; msg : Pp.t
+    }
+
+  let make ?range ?quickFix msg = { range; quickFix; msg }
+
+  let map ~f { range; quickFix; msg } =
+    let quickFix = Option.map (List.map (Lang.Qf.map ~f)) quickFix in
+    { range = Option.map f range; quickFix; msg }
+end
+
+type 'l t = Lang.Diagnostic.Severity.t * 'l Payload.t
+
+let map ~f (lvl, pl) = (lvl, Payload.map ~f pl)
diff --git a/coq/message.mli b/coq/message.mli
index dfba4ccd..f6bc0957 100644
--- a/coq/message.mli
+++ b/coq/message.mli
@@ -1,2 +1,23 @@
 (** Messages from Coq *)
-type 'l t = 'l option * Lang.Diagnostic.Severity.t * Pp.t
+
+(** Coq provides payload to our layer via two different mechanisms:
+    - feedback messages
+    - error exceptions
+
+    In both cases, the payload is the same, and it comes via different ways due
+    to historical reasons. We abstract the payload as to better handle the
+    common paths. *)
+module Payload : sig
+  type 'l t =
+    { range : 'l option
+    ; quickFix : 'l Lang.Qf.t list option
+    ; msg : Pp.t
+    }
+
+  val make : ?range:'l -> ?quickFix:'l Lang.Qf.t list -> Pp.t -> 'l t
+  val map : f:('l -> 'm) -> 'l t -> 'm t
+end
+
+type 'l t = Lang.Diagnostic.Severity.t * 'l Payload.t
+
+val map : f:('l -> 'm) -> 'l t -> 'm t
diff --git a/coq/protect.ml b/coq/protect.ml
index c768e1e9..03122490 100644
--- a/coq/protect.ml
+++ b/coq/protect.ml
@@ -1,9 +1,7 @@
 module Error = struct
-  type 'l payload = 'l option * Pp.t
-
   type 'l t =
-    | User of 'l payload
-    | Anomaly of 'l payload
+    | User of 'l Message.Payload.t
+    | Anomaly of 'l Message.Payload.t
 
   let map ~f = function
     | User e -> User (f e)
@@ -15,7 +13,9 @@ module R = struct
     | Completed of ('a, 'l Error.t) result
     | Interrupted (* signal sent, eval didn't complete *)
 
-  let error e = Completed (Error (Error.User (None, e)))
+  let error msg =
+    let payload = Message.Payload.make msg in
+    Completed (Error (Error.User payload))
 
   let map ~f = function
     | Completed (Result.Ok r) -> Completed (Result.Ok (f r))
@@ -27,11 +27,22 @@ module R = struct
     | Completed (Ok r) -> Completed (Ok r)
     | Interrupted -> Interrupted
 
+  (* Similar to Message.map, but missing the priority field, this is due to Coq
+     having to sources of feedback, an async one, and the exn sync one.
+     Ultimately both carry the same [payload].
+
+     See coq/coq#5479 for some information about this, among some other relevant
+     issues. AFAICT, the STM tried to use a full async error reporting however
+     due to problems the more "legacy" exn is the actuall error mechanism in
+     use *)
   let map_loc ~f =
-    let f (loc, msg) = (Option.map f loc, msg) in
+    let f = Message.Payload.map ~f in
     map_error ~f
 end
 
+(* let qf_of_coq qf = let range = Quickfix.loc qf in let newText = Quickfix.pp
+   qf |> Pp.string_of_ppcmds in { Lang.Qf.range; newText } *)
+
 (* Eval and reify exceptions *)
 let eval_exn ~token ~f x =
   match Limits.limit ~token ~f x with
@@ -41,11 +52,15 @@ let eval_exn ~token ~f x =
     R.Interrupted
   | exception exn ->
     let e, info = Exninfo.capture exn in
-    let loc = Loc.(get_loc info) in
+    let range = Loc.(get_loc info) in
     let msg = CErrors.iprint (e, info) in
+    let quickFix = None in
+    (* match Quickfix.from_exception exn with | Ok [] | Error _ -> None | Ok qf
+       -> Some (List.map qf_of_coq qf) in *)
+    let payload = Message.Payload.make ?range ?quickFix msg in
     Vernacstate.Interp.invalidate_cache ();
-    if CErrors.is_anomaly e then R.Completed (Error (Anomaly (loc, msg)))
-    else R.Completed (Error (User (loc, msg)))
+    if CErrors.is_anomaly e then R.Completed (Error (Anomaly payload))
+    else R.Completed (Error (User payload))
 
 let _bind_exn ~f x =
   match x with
@@ -68,10 +83,9 @@ module E = struct
     { r; feedback }
 
   let map ~f { r; feedback } = { r = R.map ~f r; feedback }
-  let map_message ~f (loc, lvl, msg) = (Option.map f loc, lvl, msg)
 
   let map_loc ~f { r; feedback } =
-    { r = R.map_loc ~f r; feedback = List.map (map_message ~f) feedback }
+    { r = R.map_loc ~f r; feedback = List.map (Message.map ~f) feedback }
 
   let bind ~f { r; feedback } =
     match r with
diff --git a/coq/protect.mli b/coq/protect.mli
index c0c2fe73..6868a6ad 100644
--- a/coq/protect.mli
+++ b/coq/protect.mli
@@ -4,11 +4,9 @@
 
     As of today this includes feedback and exceptions. *)
 module Error : sig
-  type 'l payload = 'l option * Pp.t
-
   type 'l t = private
-    | User of 'l payload
-    | Anomaly of 'l payload
+    | User of 'l Message.Payload.t
+    | Anomaly of 'l Message.Payload.t
 end
 
 (** This "monad" could be related to "Runners in action" (Ahman, Bauer), thanks
@@ -22,7 +20,7 @@ module R : sig
   val map : f:('a -> 'b) -> ('a, 'l) t -> ('b, 'l) t
 
   val map_error :
-    f:('l Error.payload -> 'm Error.payload) -> ('a, 'l) t -> ('a, 'm) t
+    f:('l Message.Payload.t -> 'm Message.Payload.t) -> ('a, 'l) t -> ('a, 'm) t
 
   (** Update the loc stored in the result, this is used by our cache-aware
       location *)
@@ -30,7 +28,7 @@ module R : sig
 end
 
 module E : sig
-  type ('a, 'l) t =
+  type ('a, 'l) t = private
     { r : ('a, 'l) R.t
     ; feedback : 'l Message.t list
     }
diff --git a/coq/workspace.ml b/coq/workspace.ml
index 3466e14c..222ccbb6 100644
--- a/coq/workspace.ml
+++ b/coq/workspace.ml
@@ -387,8 +387,8 @@ let guess ~token ~debug ~cmdline ~dir =
   ignore feedback;
   match r with
   | Protect.R.Interrupted -> Error "Workspace Scanning Interrupted"
-  | Protect.R.Completed (Error (User (_, msg)))
-  | Protect.R.Completed (Error (Anomaly (_, msg))) ->
+  | Protect.R.Completed (Error (User { msg; _ }))
+  | Protect.R.Completed (Error (Anomaly { msg; _ })) ->
     Error (Format.asprintf "Workspace Scanning Errored: %a" Pp.pp_with msg)
   | Protect.R.Completed (Ok workspace) -> Ok workspace
 
diff --git a/editor/code/CHANGELOG.md b/editor/code/CHANGELOG.md
index a85e940a..0eab4ec0 100644
--- a/editor/code/CHANGELOG.md
+++ b/editor/code/CHANGELOG.md
@@ -1,3 +1,65 @@
+# coq-lsp 0.2.2: To Virtual or not To Virtual
+---------------------------------------------
+
+ - [vscode] Expand selectors to include `vscode-vfs://` URIs used in
+   `github.dev`, document limited virtual workspace support in
+   `package.json` (@ejgallego, #849)
+
+# coq-lsp 0.2.1: Click !
+------------------------
+
+ This release brings full Web Extension support for coq-lsp!
+
+ You can now run Coq from your browser using https://vscode.dev or
+ https://github.dev .
+
+ Some other highlights is `codeAction` support (for Coq quick fixes),
+ `Restart.` support, better API for our extension users, and many
+ bugfixes and improvements, in particular for `hover`.
+
+ The detailed list of server and client changes is below:
+
+ - [workspace] [coq] Support _CoqProject arguments `-type-in-type` and
+   `-allow-rewrite-rules` (for 8.20) (@ejgallego, #819)
+ - [serlib] Fix Ltac2 AST piercing bug, add test case that should help
+   in the future (@ejgallego, @jim-portegies, #821)
+ - [fleche] [8.20] understand rewrite rules and symbols on document
+   outline (@ejgallego, @Alizter, #825, fixes #824)
+ - [fleche] [coq] support `Restart` meta command (@ejgallego,
+   @Alizter, #828, fixes #827)
+ - [fleche] [plugins] New plugin example `explain_errors`, that will
+   print all errors on a file, with their goal context (@ejgallego,
+   #829, thanks to @gmalecha for the idea, c.f. Coq issue 19601)
+ - [fleche] Highlight the full first line of the document on
+   initialization error (@ejgallego, #832)
+ - [fleche] [jscoq] [js] Build worker version of `coq-lsp`. This
+   provides a full working Coq enviroment in `vscode.dev`. The web
+   worker version is build as an artifact on CI (@ejgallego
+   @corwin-of-amber, #433)
+ - [hover] Fix universe and level printing in hover (#839, fixes #835
+   , @ejgallego , @Alizter)
+ - [fleche] New immediate request serving mode. In this mode, requests
+   are served with whatever document state we have. This is very
+   useful when we are not in continuous mode, and we don't have a good
+   reference as to what to build, for example in
+   `documentSymbols`. The mode actually works pretty well in practice
+   as often language requests will come after goals requests, so the
+   info that is needed is at hand. It could also be tried to set the
+   build target for immediate requests to the view hint, but we should
+   see some motivation for that (@ejgallego, #841)
+ - [lsp] [diagnostics] (! breaking change) change type of diagnostics
+   extra data from list to named record (@ejgallego, #843)
+ - [lsp] Implement support for `textDocument/codeAction`. For now, we
+   support Coq's 8.21 `quickFix` data (@ejgallego, #840, #843, #845)
+ - [petanque] Fix bug for detection of proof finished in deep stacks
+   (@ejgallego, @gbdrt, #847)
+ - [goals request] allow multiple Coq sentences in `command`. This is
+   backwards compatible in the case that commands do not error, and
+   users were sending just one command. (@ejgallego, #823, thanks to
+   CoqPilot devs and G. Baudart for feedback)
+ - [goals request] (! breaking) fail the request if the commands in
+   `command` fail (@ejgallego, #823)
+
 # coq-lsp 0.2.0: From Green to Blue
 -----------------------------------
 
diff --git a/editor/code/package-lock.json b/editor/code/package-lock.json
index ba496c85..833da9cd 100644
--- a/editor/code/package-lock.json
+++ b/editor/code/package-lock.json
@@ -1,12 +1,12 @@
 {
   "name": "coq-lsp",
-  "version": "0.2.0",
+  "version": "0.2.2",
   "lockfileVersion": 3,
   "requires": true,
   "packages": {
     "": {
       "name": "coq-lsp",
-      "version": "0.2.0",
+      "version": "0.2.2",
       "dependencies": {
         "@vscode/webview-ui-toolkit": "^1.2.2",
         "jquery": "^3.7.1",
diff --git a/editor/code/package.json b/editor/code/package.json
index 9db5b692..de6ce5c0 100644
--- a/editor/code/package.json
+++ b/editor/code/package.json
@@ -2,7 +2,7 @@
   "name": "coq-lsp",
   "displayName": "Coq LSP",
   "description": "Coq LSP provides native vsCode support for checking Coq proof documents",
-  "version": "0.2.0",
+  "version": "0.2.2",
   "contributors": [
     "Emilio Jesús Gallego Arias <e@x80.org>",
     "Ali Caglayan <alizter@gmail.com>",
@@ -32,6 +32,12 @@
     "onLanguage:markdown",
     "onLanguage:latex"
   ],
+  "capabilities": {
+    "virtualWorkspaces": {
+      "supported": "limited",
+      "description": "File operations such as jump to definition are not supported in virtual workspaces. While almost fully functional, coq-lsp remains experiemental as a Web Extension."
+    }
+  },
   "contributes": {
     "languages": [
       {
@@ -209,6 +215,11 @@
             "type": "boolean",
             "default": false,
             "description": "Send extra diagnostics data, usually on error"
+          },
+          "coq-lsp.send_perf_data": {
+            "type": "boolean",
+            "default": true,
+            "description": "Update Perf Data Coq Panel"
           }
         }
       },
diff --git a/editor/code/src/client.ts b/editor/code/src/client.ts
index d8dbf352..29faaf89 100644
--- a/editor/code/src/client.ts
+++ b/editor/code/src/client.ts
@@ -210,7 +210,7 @@ export function activateCoqLSP(
     const initializationOptions: CoqLspServerConfig = configDidChange(wsConfig);
 
     const clientOptions: LanguageClientOptions = {
-      documentSelector: CoqSelector.local,
+      documentSelector: CoqSelector.owned,
       outputChannelName: "Coq LSP Server Events",
       revealOutputChannelOn: RevealOutputChannelOn.Info,
       initializationOptions,
@@ -335,7 +335,7 @@ export function activateCoqLSP(
       let textDocument = { uri, version };
       infoPanel.notifyLackOfVSLS(textDocument, position);
       return;
-    } else if (languages.match(CoqSelector.local, textEditor.document) < 1)
+    } else if (languages.match(CoqSelector.owned, textEditor.document) < 1)
       return;
 
     const kind =
@@ -373,7 +373,7 @@ export function activateCoqLSP(
       if (
         config.check_on_scroll &&
         serverConfig.check_only_on_request &&
-        languages.match(CoqSelector.local, evt.textEditor.document) > 0 &&
+        languages.match(CoqSelector.owned, evt.textEditor.document) > 0 &&
         evt.visibleRanges[0]
       ) {
         let uri = evt.textEditor.document.uri.toString();
diff --git a/editor/code/src/config.ts b/editor/code/src/config.ts
index a55320fc..b72deada 100644
--- a/editor/code/src/config.ts
+++ b/editor/code/src/config.ts
@@ -96,4 +96,12 @@ export namespace CoqSelector {
   export const vsls: TextDocumentFilter[] = all.map((selector) => {
     return { ...selector, scheme: "vsls" };
   });
+
+  // Virtual workspaces such as github.dev
+  export const virtual: TextDocumentFilter[] = all.map((selector) => {
+    return { ...selector, scheme: "vscode-vfs" };
+  });
+
+  // Files that are owned by our server, local + virtual
+  export const owned: TextDocumentFilter[] = local.concat(virtual);
 }
diff --git a/etc/doc/PROTOCOL.md b/etc/doc/PROTOCOL.md
index a9d3322b..4a77e4bf 100644
--- a/etc/doc/PROTOCOL.md
+++ b/etc/doc/PROTOCOL.md
@@ -164,6 +164,20 @@ today we offer two kinds of extra information on errors:
 - range of the full sentence that displayed the error,
 - if the error was on a Require, information about the library that failed.
 
+As of today, this extra data is passed via member parameters
+```typescript
+// From `prefix` Require `refs`
+type failedRequire = {
+    prefix ?: qualid
+    refs : qualid list
+}
+
+type DiagnosticsData = {
+    sentenceRange ?: Range;
+    failedRequire ?: FailedRequire
+}
+```
+
 ### Goal Display
 
 In order to display proof goals and information at point, `coq-lsp` supports the `proof/goals` request, parameters are:
@@ -173,12 +187,19 @@ interface GoalRequest {
     textDocument: VersionedTextDocumentIdentifier;
     position: Position;
     pp_format?: 'Pp' | 'Str';
-    pretac?: string;
     command?: string;
     mode?: 'Prev' | 'After';
 }
 ```
 
+The first parameters are standard, `pp_format` controls the pretty
+printing format used in the results.
+
+The `command` parameter (experimental), is a list of Coq commands that
+will be run just _after_ `position` in `textDocument`, but _before_
+goals are sent to the user. This is often useful for ephemeral
+post-processing.
+
 Answer to the request is a `Goal[]` object, where
 
 ```typescript
diff --git a/examples/Pff.v b/examples/Pff.v
index 252b89f3..3db572bd 100644
--- a/examples/Pff.v
+++ b/examples/Pff.v
@@ -14,7 +14,7 @@ Require Import Psatz.
 Set Warnings "-deprecated".
 
 (* Compatibility workaround, remove once requiring Coq >= 8.16 *)
-Module Import Compat.
+Module Import Compat816.
 
 Lemma Even_0 : Nat.Even 0.
 Proof. exists 0; reflexivity. Qed.
@@ -67,7 +67,21 @@ Proof proj1 (proj1 (Even_Odd_double n)).
 Definition Odd_double n : Nat.Odd n -> n = S (Nat.double (Nat.div2 n)).
 Proof proj1 (proj2 (Even_Odd_double n)).
 
-End Compat.
+Definition Rinv_mult_distr := Rinv_mult_distr.
+Definition Rabs_Rinv := Rabs_Rinv.
+Definition Rinv_pow := Rinv_pow.
+Definition Rinv_involutive := Rinv_involutive.
+Definition Rlt_Rminus := Rlt_Rminus.
+Definition powerRZ_inv := powerRZ_inv.
+Definition powerRZ_neg := powerRZ_neg.
+
+End Compat816.
+
+Module Import Compat819.
+
+Definition IZR_neq := IZR_neq.
+
+End Compat819.
 
 (*** was file sTactic.v  ***)
 
@@ -17553,7 +17567,7 @@ apply Z.le_trans with  (Nat.double (Nat.div2 t)).
 unfold Nat.double; rewrite inj_plus; auto with zarith.
 rewrite <- Even_double; auto with zarith.
 apply Z.le_trans with (-1+(S ( Nat.double (Nat.div2 t))))%Z.
-rewrite inj_S; unfold Z.succ; auto with zarith.
+rewrite inj_S; unfold Z.succ; auto with zarith;
 unfold Nat.double; rewrite inj_plus; auto with zarith.
 rewrite <- Odd_double by easy. lia.
 Qed.
@@ -17568,9 +17582,9 @@ case (Nat.Even_or_Odd t); intros I.
 apply Z.le_trans with  ((Nat.double (Nat.div2 t)+1))%Z.
 2:unfold Nat.double; rewrite inj_plus; auto with zarith.
 rewrite <- Even_double; auto with zarith.
-apply Z.le_trans with ((S ( Nat.double (Nat.div2 t))))%Z; auto with zarith.
-2: rewrite inj_S; unfold Z.succ; auto with zarith.
-2: unfold Nat.double; rewrite inj_plus; auto with zarith.
+apply Z.le_trans with ((S ( Nat.double (Nat.div2 t))))%Z; auto with zarith;
+try solve [rewrite inj_S; unfold Z.succ; auto with zarith;
+  unfold Nat.double; rewrite inj_plus; auto with zarith].
 rewrite <- Odd_double; auto with zarith.
 Qed.
 
diff --git a/examples/codeAction.v b/examples/codeAction.v
new file mode 100644
index 00000000..e56fd402
--- /dev/null
+++ b/examples/codeAction.v
@@ -0,0 +1,54 @@
+(* Test for Coq's QF for Coq to Stdlib PRs *)
+
+Require Import Coq.ssr.ssrbool.
+From Coq Require Import ssreflect ssrbool.
+
+(* Note: this tests the two different lookup modes *)
+About Coq.Init.Nat.add.
+Check Coq.Init.Nat.add.
+
+(* Example codeAction, from Coq's test suite *)
+
+Module M. Definition y := 4. End M.
+Import M.
+
+#[deprecated(use=y)]
+Definition x := 3.
+
+Module N. Definition y := 5. End N.
+Import N.
+
+Definition d1 := x = 3.
+
+Module M1.
+Notation w := x.
+End M1.
+Import M1.
+
+#[deprecated(use=w)]
+Notation v := 3.
+
+Module M2.
+Notation w := 5.
+End M2.
+Import M2.
+
+Definition d2 := v = 3.
+
+Fail #[deprecated(use=w)]
+Notation "a +++ b" := (a + b) (at level 2).
+
+Fail #[deprecated(use=nonexisting)]
+Definition y := 2.
+
+(***********************************************)
+Module A.
+End B.
+
+(***********************************************)
+Require Import Extraction.
+
+Module nat. End nat.
+
+Extraction nat.
+
diff --git a/fleche/doc.ml b/fleche/doc.ml
index fbde2b1e..1e3d7fce 100644
--- a/fleche/doc.ml
+++ b/fleche/doc.ml
@@ -116,8 +116,9 @@ module Node = struct
   module Message = struct
     type t = Lang.Range.t Coq.Message.t
 
-    let feedback_to_message ~lines (loc, lvl, msg) =
-      (Coq.Utils.to_orange ~lines loc, lvl, msg)
+    let feedback_to_message ~lines message =
+      let f = Coq.Utils.to_range ~lines in
+      Coq.Message.map ~f message
   end
 
   type t =
@@ -145,7 +146,7 @@ module Diags : sig
 
   (** Build simple diagnostic *)
   val make :
-       ?data:Lang.Diagnostic.Data.t list
+       ?data:Lang.Diagnostic.Data.t
     -> Lang.Range.t
     -> Lang.Diagnostic.Severity.t
     -> Pp.t
@@ -154,6 +155,7 @@ module Diags : sig
   (** Build advanced diagnostic with AST analysis *)
   val error :
        err_range:Lang.Range.t
+    -> quickFix:Lang.Range.t Lang.Qf.t list option
     -> msg:Pp.t
     -> stm_range:Lang.Range.t (* range for the sentence *)
     -> ?ast:Node.Ast.t
@@ -174,31 +176,41 @@ end = struct
     Lang.Diagnostic.{ range; severity; message; data }
 
   (* ast-dependent error diagnostic generation *)
-  let extra_diagnostics_of_ast stm_range ast =
-    let stm_range = Lang.Diagnostic.Data.SentenceRange stm_range in
-    match
-      Option.bind ast (fun (ast : Node.Ast.t) -> Coq.Ast.Require.extract ast.v)
-    with
-    | Some { Coq.Ast.Require.from; mods; _ } ->
-      let refs = List.map fst mods in
-      Some
-        [ stm_range
-        ; Lang.Diagnostic.Data.FailedRequire { prefix = from; refs }
-        ]
-    | _ -> Some [ stm_range ]
-
-  let extra_diagnostics_of_ast stm_range ast =
+  let extra_diagnostics_of_ast quickFix stm_range ast =
+    let sentenceRange = Some stm_range in
+    let failedRequire =
+      match
+        Option.bind ast (fun (ast : Node.Ast.t) ->
+            Coq.Ast.Require.extract ast.v)
+      with
+      | Some { Coq.Ast.Require.from; mods; _ } ->
+        let refs = List.map fst mods in
+        Some [ { Lang.Diagnostic.FailedRequire.prefix = from; refs } ]
+      | _ -> None
+    in
+    Some { Lang.Diagnostic.Data.sentenceRange; failedRequire; quickFix }
+
+  let extra_diagnostics_of_ast qf stm_range ast =
     if !Config.v.send_diags_extra_data then
-      extra_diagnostics_of_ast stm_range ast
+      extra_diagnostics_of_ast qf stm_range ast
     else None
 
-  let error ~err_range ~msg ~stm_range ?ast () =
-    let data = extra_diagnostics_of_ast stm_range ast in
+  let error ~err_range ~quickFix ~msg ~stm_range ?ast () =
+    let data = extra_diagnostics_of_ast quickFix stm_range ast in
     make ?data err_range Lang.Diagnostic.Severity.error msg
 
-  let of_feed ~drange (range, severity, message) =
+  let of_feed ~drange (severity, payload) =
+    let { Coq.Message.Payload.range; quickFix; msg } = payload in
     let range = Option.default drange range in
-    make range severity message
+    (* Be careful to avoid defining data if quickFix = None *)
+    let data =
+      Option.map
+        (fun qf ->
+          let sentenceRange, failedRequire, quickFix = (None, None, Some qf) in
+          Lang.Diagnostic.Data.{ sentenceRange; failedRequire; quickFix })
+        quickFix
+    in
+    make ?data range severity msg
 
   type partition_kind =
     | Left
@@ -223,9 +235,11 @@ end = struct
       else if !Config.v.show_notices_as_diagnostics then 4
       else 3
     in
-    let f (_, lvl, _) =
-      let lvl = Lang.Diagnostic.Severity.to_int lvl in
-      if lvl = 2 then Both else if lvl < cutoff then Left else Right
+    let f (lvl, _) =
+      (* warning = 2 *)
+      if lvl = Lang.Diagnostic.Severity.warning then Both
+      else if lvl < cutoff then Left
+      else Right
     in
     let diags, messages = partition ~f fbs in
     (List.map (of_feed ~drange) diags, messages)
@@ -351,8 +365,9 @@ let empty_doc ~uri ~contents ~version ~env ~root ~nodes ~completed =
   let completed = completed init_range in
   { uri; contents; toc; version; env; root; nodes; diags_dirty; completed }
 
-let error_doc ~loc ~message ~uri ~contents ~version ~env =
-  let feedback = [ (loc, Diags.err, Pp.str message) ] in
+let error_doc ~range ~message ~uri ~contents ~version ~env =
+  let payload = Coq.Message.Payload.make ?range (Pp.str message) in
+  let feedback = [ (Diags.err, payload) ] in
   let root = env.Env.init in
   let nodes = [] in
   let completed range = Completion.Failed range in
@@ -362,7 +377,8 @@ let conv_error_doc ~raw ~uri ~version ~env ~root err =
   let contents = Contents.make_raw ~raw in
   let lines = contents.lines in
   let err =
-    (None, Diags.err, Pp.(str "Error in document conversion: " ++ str err))
+    let msg = Pp.(str "Error in document conversion: " ++ str err) in
+    (Diags.err, Coq.Message.Payload.make msg)
   in
   (* No execution to add *)
   let stats = None in
@@ -391,14 +407,14 @@ let handle_doc_creation_exec ~token ~env ~uri ~version ~contents =
     match r with
     | Interrupted ->
       let message = "Document Creation Interrupted!" in
-      let loc = None in
-      error_doc ~loc ~message ~uri ~version ~contents ~env
-    | Completed (Error (User (loc, err_msg)))
-    | Completed (Error (Anomaly (loc, err_msg))) ->
+      let range = None in
+      error_doc ~range ~message ~uri ~version ~contents ~env
+    | Completed (Error (User { range; msg = err_msg; quickFix = _ }))
+    | Completed (Error (Anomaly { range; msg = err_msg; quickFix = _ })) ->
       let message =
         Format.asprintf "Doc.create, internal error: @[%a@]" Pp.pp_with err_msg
       in
-      error_doc ~loc ~message ~uri ~version ~contents ~env
+      error_doc ~range ~message ~uri ~version ~contents ~env
     | Completed (Ok doc) -> (doc, [])
   in
   let state = doc.root in
@@ -656,6 +672,7 @@ end = struct
     | Completed (Ok st) -> st
     | Completed (Error _) -> st
 end
+(* end [module Recovery = struct...] *)
 
 let interp_and_info ~token ~st ~files ast =
   match Coq.Ast.Require.extract ast with
@@ -669,16 +686,17 @@ let search_node ~command ~doc ~st =
       (fun (node : Node.t) -> Option.default Memo.Stats.zero node.info.stats)
       Memo.Stats.zero node
   in
+  let back_overflow num =
+    let ll = List.length doc.nodes in
+    Pp.(
+      str "not enough nodes: [" ++ int num ++ str " > " ++ int ll
+      ++ str "] available document nodes")
+  in
   match command with
   | Coq.Ast.Meta.Command.Back num -> (
     match Base.List.nth doc.nodes num with
     | None ->
-      let ll = List.length doc.nodes in
-      let message =
-        Pp.(
-          str "not enough nodes: [" ++ int num ++ str " > " ++ int ll
-          ++ str "] available document nodes")
-      in
+      let message = back_overflow num in
       (Coq.Protect.E.error message, nstats None)
     | Some node -> (Coq.Protect.E.ok node.state, nstats (Some node)))
   | Restart -> (
@@ -745,22 +763,23 @@ let parse_action ~token ~lines ~st last_tok doc_handle =
     | Ok (Some ast) ->
       let () = if Debug.parsing then DDebug.parsed_sentence ~ast in
       (Process ast, [], feedback, time)
-    | Error (Anomaly (_, msg)) | Error (User (None, msg)) ->
+    | Error (Anomaly { range = _; quickFix; msg })
+    | Error (User { range = None; quickFix; msg }) ->
       (* We don't have a better alternative :(, usually missing error loc here
          means an anomaly, so we stop *)
       let err_range = last_tok in
       let parse_diags =
-        [ Diags.error ~err_range ~msg ~stm_range:err_range () ]
+        [ Diags.error ~err_range ~quickFix ~msg ~stm_range:err_range () ]
       in
       (EOF (Failed last_tok), parse_diags, feedback, time)
-    | Error (User (Some err_range, msg)) ->
+    | Error (User { range = Some err_range; quickFix; msg }) ->
       Coq.Parsing.discard_to_dot doc_handle;
       let last_tok = Coq.Parsing.Parsable.loc doc_handle in
       let last_tok_range = Coq.Utils.to_range ~lines last_tok in
       let span_loc = Util.build_span start_loc last_tok in
       let span_range = Coq.Utils.to_range ~lines span_loc in
       let parse_diags =
-        [ Diags.error ~err_range ~msg ~stm_range:span_range () ]
+        [ Diags.error ~err_range ~quickFix ~msg ~stm_range:span_range () ]
       in
       (Skip (span_range, last_tok_range), parse_diags, feedback, time))
 
@@ -812,10 +831,13 @@ let node_of_coq_result ~token ~doc ~range ~prev ~ast ~st ~parsing_diags
         ~diags:[] ~feedback ~info
     in
     Continue { state; last_tok; node }
-  | Error (Coq.Protect.Error.Anomaly (err_range, msg) as coq_err)
-  | Error (User (err_range, msg) as coq_err) ->
+  | Error
+      (Coq.Protect.Error.Anomaly { range = err_range; quickFix; msg } as coq_err)
+  | Error (User { range = err_range; quickFix; msg } as coq_err) ->
     let err_range = Option.default range err_range in
-    let err_diags = [ Diags.error ~err_range ~msg ~stm_range:range ~ast () ] in
+    let err_diags =
+      [ Diags.error ~err_range ~quickFix ~msg ~stm_range:range ~ast () ]
+    in
     let contents, nodes = (doc.contents, doc.nodes) in
     let context =
       Recovery_context.make ~contents ~last_tok ~nodes ~ast:ast.v ()
@@ -1072,3 +1094,34 @@ let save ~token ~doc =
   | _ ->
     let error = Pp.(str "Can't save document that failed to check") in
     Coq.Protect.E.error error
+
+(* run api, experimental *)
+
+(* Adaptor, should be supported in memo directly *)
+let eval_no_memo ~token (st, cmd) =
+  Coq.Interp.interp ~token ~intern:Vernacinterp.fs_intern ~st cmd
+
+(* TODO, what to do with feedback, what to do with errors *)
+let rec parse_execute_loop ~token ~memo pa st =
+  let open Coq.Protect.E.O in
+  let eval = if memo then Memo.Interp.eval else eval_no_memo in
+  let* ast = Coq.Parsing.parse ~token ~st pa in
+  match ast with
+  | Some ast -> (
+    match eval ~token (st, ast) with
+    | Coq.Protect.E.{ r = Coq.Protect.R.Completed (Ok st); feedback = _ } ->
+      parse_execute_loop ~token ~memo pa st
+    | res -> res)
+  (* On EOF we return the previous state, the command was the empty string or a
+     comment *)
+  | None -> Coq.Protect.E.ok st
+
+let parse_and_execute_in ~token ~loc tac st =
+  let str = Gramlib.Stream.of_string tac in
+  let pa = Coq.Parsing.Parsable.make ?loc str in
+  parse_execute_loop ~token pa st
+
+let run ~token ?loc ?(memo = true) ~st cmds =
+  Coq.State.in_stateM ~token ~st
+    ~f:(parse_and_execute_in ~token ~loc ~memo cmds)
+    st
diff --git a/fleche/doc.mli b/fleche/doc.mli
index f309d9bc..540ea890 100644
--- a/fleche/doc.mli
+++ b/fleche/doc.mli
@@ -24,7 +24,7 @@ module Node : sig
   end
 
   module Message : sig
-    type t = Lang.Range.t option * Lang.Diagnostic.Severity.t * Pp.t
+    type t = Lang.Range.t Coq.Message.t
   end
 
   type t = private
@@ -137,3 +137,21 @@ val check :
 (** [save ~doc] will save [doc] .vo file. It will fail if proofs are open, or if
     the document completion status is not [Yes] *)
 val save : token:Coq.Limits.Token.t -> doc:t -> (unit, Loc.t) Coq.Protect.E.t
+
+(** [run ~token ?loc ?memo ~st cmds] run commands [cmds] starting on state [st],
+    without commiting changes to the document. [loc] can be used to seed an
+    initial location if desired, if not the locations will be considered
+    relative to the initial location. [memo] controls if the execution is
+    memoized, by default [true].
+
+    This API is experimental, used for speculative execution
+    [petanque
+    and goals], the API is expected to change as to better adapt
+    to users. *)
+val run :
+     token:Coq.Limits.Token.t
+  -> ?loc:Loc.t
+  -> ?memo:bool
+  -> st:Coq.State.t
+  -> string
+  -> (Coq.State.t, Loc.t) Coq.Protect.E.t
diff --git a/fleche/version.ml b/fleche/version.ml
index 93c56887..2b22f1f7 100644
--- a/fleche/version.ml
+++ b/fleche/version.ml
@@ -12,6 +12,6 @@ type t = string
 
 (************************************************************************)
 (*                        UPDATE VERSION HERE                           *)
-let server = "0.2.0"
+let server = "0.2.2"
 (*                        UPDATE VERSION HERE                           *)
 (************************************************************************)
diff --git a/lang/diagnostic.ml b/lang/diagnostic.ml
index 393b1168..f88f4902 100644
--- a/lang/diagnostic.ml
+++ b/lang/diagnostic.ml
@@ -4,13 +4,19 @@
 (* Written by: Emilio J. Gallego Arias                                  *)
 (************************************************************************)
 
+module FailedRequire = struct
+  type t =
+    { prefix : Libnames.qualid option
+    ; refs : Libnames.qualid list
+    }
+end
+
 module Data = struct
   type t =
-    | SentenceRange of Range.t
-    | FailedRequire of
-        { prefix : Libnames.qualid option
-        ; refs : Libnames.qualid list
-        }
+    { sentenceRange : Range.t option [@default None]
+    ; failedRequire : FailedRequire.t list option [@default None]
+    ; quickFix : Range.t Qf.t list option [@default None]
+    }
 end
 
 module Severity = struct
@@ -20,14 +26,13 @@ module Severity = struct
   let warning = 2
   let information = 3
   let hint = 4
-  let to_int x = x
 end
 
 type t =
   { range : Range.t
   ; severity : Severity.t
   ; message : Pp.t
-  ; data : Data.t list option [@default None]
+  ; data : Data.t option [@default None]
   }
 
 let is_error { severity; _ } = severity = 1
diff --git a/lang/diagnostic.mli b/lang/diagnostic.mli
index 220d8547..7368ab86 100644
--- a/lang/diagnostic.mli
+++ b/lang/diagnostic.mli
@@ -4,32 +4,35 @@
 (* Written by: Emilio J. Gallego Arias                                  *)
 (************************************************************************)
 
+module FailedRequire : sig
+  type t =
+    { prefix : Libnames.qualid option
+    ; refs : Libnames.qualid list
+    }
+end
+
 module Data : sig
   type t =
-    | SentenceRange of Range.t
-    | FailedRequire of
-        { prefix : Libnames.qualid option
-        ; refs : Libnames.qualid list
-        }
+    { sentenceRange : Range.t option [@default None]
+    ; failedRequire : FailedRequire.t list option [@default None]
+    ; quickFix : Range.t Qf.t list option [@default None]
+    }
 end
 
 module Severity : sig
-  type t
-
-  val error : t
-  val warning : t
-  val information : t
-  val hint : t
+  type t = int
 
-  (** Convert to LSP-like levels *)
-  val to_int : t -> int
+  val error : t (* 1 *)
+  val warning : t (* 2 *)
+  val information : t (* 3 *)
+  val hint : t (* 4 *)
 end
 
 type t =
   { range : Range.t
   ; severity : Severity.t
   ; message : Pp.t
-  ; data : Data.t list option [@default None]
+  ; data : Data.t option [@default None]
   }
 
 val is_error : t -> bool
diff --git a/lang/qf.ml b/lang/qf.ml
new file mode 100644
index 00000000..15d64593
--- /dev/null
+++ b/lang/qf.ml
@@ -0,0 +1,12 @@
+(************************************************************************)
+(* Flèche => document manager: Language Support                         *)
+(* Copyright 2019-2024 Inria      -- Dual License LGPL 2.1 / GPL3+      *)
+(* Written by: Emilio J. Gallego Arias                                  *)
+(************************************************************************)
+
+type 'l t =
+  { range : 'l
+  ; newText : string
+  }
+
+let map ~f { range; newText } = { range = f range; newText }
diff --git a/lang/qf.mli b/lang/qf.mli
new file mode 100644
index 00000000..c3965d04
--- /dev/null
+++ b/lang/qf.mli
@@ -0,0 +1,12 @@
+(************************************************************************)
+(* Flèche => document manager: Language Support                         *)
+(* Copyright 2019-2024 Inria      -- Dual License LGPL 2.1 / GPL3+      *)
+(* Written by: Emilio J. Gallego Arias                                  *)
+(************************************************************************)
+
+type 'l t =
+  { range : 'l
+  ; newText : string
+  }
+
+val map : f:('l -> 'm) -> 'l t -> 'm t
diff --git a/lsp/core.ml b/lsp/core.ml
index 7284656c..24799f4c 100644
--- a/lsp/core.ml
+++ b/lsp/core.ml
@@ -177,3 +177,33 @@ module DocumentDiagnosticReportPartialResult = struct
     }
   [@@deriving to_yojson]
 end
+
+(* CodeAction *)
+module CodeActionContext = struct
+  type t =
+    { diagnostics : Lang.Diagnostic.t list
+    ; only : string option [@default None]
+    ; triggerKind : int option [@default None]
+    }
+  [@@deriving to_yojson]
+end
+
+module CodeActionParams = struct
+  type t =
+    { textDocument : Doc.TextDocumentIdentifier.t
+    ; range : Lang.Range.t
+    ; context : CodeActionContext.t
+    }
+  [@@deriving to_yojson]
+end
+
+module CodeAction = struct
+  type t =
+    { title : string
+    ; kind : string option [@default None]
+    ; diagnostics : Lang.Diagnostic.t list [@default []]
+    ; isPreferred : bool option [@default None]
+    ; edit : Workspace.WorkspaceEdit.t option [@default None]
+    }
+  [@@deriving to_yojson]
+end
diff --git a/lsp/core.mli b/lsp/core.mli
index ae706ef8..c222d34e 100644
--- a/lsp/core.mli
+++ b/lsp/core.mli
@@ -180,3 +180,33 @@ module DocumentDiagnosticReportPartialResult : sig
     }
   [@@deriving to_yojson]
 end
+
+(* CodeAction *)
+module CodeActionContext : sig
+  type t =
+    { diagnostics : Lang.Diagnostic.t list
+    ; only : string option [@default None]
+    ; triggerKind : int option [@default None]
+    }
+  [@@deriving to_yojson]
+end
+
+module CodeActionParams : sig
+  type t =
+    { textDocument : Doc.TextDocumentIdentifier.t
+    ; range : Lang.Range.t
+    ; context : CodeActionContext.t
+    }
+  [@@deriving to_yojson]
+end
+
+module CodeAction : sig
+  type t =
+    { title : string
+    ; kind : string option [@default None]
+    ; diagnostics : Lang.Diagnostic.t list [@default []]
+    ; isPreferred : bool option [@default None]
+    ; edit : Workspace.WorkspaceEdit.t option [@default None]
+    }
+  [@@deriving to_yojson]
+end
diff --git a/lsp/jCoq.ml b/lsp/jCoq.ml
index 3497091a..fabdda66 100644
--- a/lsp/jCoq.ml
+++ b/lsp/jCoq.ml
@@ -26,6 +26,7 @@ let rec pp_opt d =
 module Pp = struct
   include Serlib.Ser_pp
 
+  let str = Pp.str
   let string_of_ppcmds = Pp.string_of_ppcmds
   let to_string = Pp.string_of_ppcmds
   let to_yojson x = to_yojson (pp_opt x)
diff --git a/lsp/jLang.ml b/lsp/jLang.ml
index e5490703..a486ac03 100644
--- a/lsp/jLang.ml
+++ b/lsp/jLang.ml
@@ -34,12 +34,22 @@ module LUri = struct
   end
 end
 
+module Qf = struct
+  type 'l t = [%import: 'l Lang.Qf.t] [@@deriving yojson]
+end
+
 module Diagnostic = struct
   module Libnames = Serlib.Ser_libnames
 
+  module FailedRequire = struct
+    type t = [%import: Lang.Diagnostic.FailedRequire.t] [@@deriving yojson]
+  end
+
   module Data = struct
     module Lang = struct
       module Range = Range
+      module Qf = Qf
+      module FailedRequire = FailedRequire
       module Diagnostic = Lang.Diagnostic
     end
 
@@ -56,6 +66,7 @@ module Diagnostic = struct
     [@@deriving yojson]
 
     let conv { Lang.Point.line; character; offset = _ } = { line; character }
+    let vnoc { line; character } = { Lang.Point.line; character; offset = -1 }
   end
 
   module Range = struct
@@ -69,6 +80,11 @@ module Diagnostic = struct
       let start = Point.conv start in
       let end_ = Point.conv end_ in
       { start; end_ }
+
+    let vnoc { start; end_ } =
+      let start = Point.vnoc start in
+      let end_ = Point.vnoc end_ in
+      { Lang.Range.start; end_ }
   end
 
   (* Current Flèche diagnostic is not LSP-standard compliant, this one is *)
@@ -78,15 +94,22 @@ module Diagnostic = struct
     { range : Range.t
     ; severity : int
     ; message : string
-    ; data : Data.t list option [@default None]
+    ; data : Data.t option [@default None]
     }
   [@@deriving yojson]
 
   let to_yojson { Lang.Diagnostic.range; severity; message; data } =
     let range = Range.conv range in
-    let severity = Lang.Diagnostic.Severity.to_int severity in
     let message = Pp.to_string message in
     _t_to_yojson { range; severity; message; data }
+
+  let of_yojson json =
+    match _t_of_yojson json with
+    | Ok { range; severity; message; data } ->
+      let range = Range.vnoc range in
+      let message = Pp.str message in
+      Ok { Lang.Diagnostic.range; severity; message; data }
+    | Error err -> Error err
 end
 
 module Stdlib = JStdlib
diff --git a/lsp/jLang.mli b/lsp/jLang.mli
index 2b59f7b8..11b624c0 100644
--- a/lsp/jLang.mli
+++ b/lsp/jLang.mli
@@ -20,7 +20,7 @@ module LUri : sig
 end
 
 module Diagnostic : sig
-  type t = Lang.Diagnostic.t [@@deriving to_yojson]
+  type t = Lang.Diagnostic.t [@@deriving yojson]
 
   module Point : sig
     type t =
@@ -36,6 +36,8 @@ module Diagnostic : sig
       ; end_ : Point.t [@key "end"]
       }
     [@@deriving yojson]
+
+    val vnoc : t -> Lang.Range.t
   end
 end
 
diff --git a/lsp/workspace.ml b/lsp/workspace.ml
index d457453f..912037ee 100644
--- a/lsp/workspace.ml
+++ b/lsp/workspace.ml
@@ -4,6 +4,7 @@
 (* Written by: Emilio J. Gallego Arias                                  *)
 (************************************************************************)
 
+module Lang_ = Lang
 module Lang = JLang
 
 module WorkspaceFolder = struct
@@ -25,3 +26,23 @@ end
 module DidChangeWorkspaceFoldersParams = struct
   type t = { event : WorkspaceFoldersChangeEvent.t } [@@deriving yojson]
 end
+
+module TextEdit = struct
+  type t =
+    { range : Lang.Range.t
+    ; newText : string
+    }
+  [@@deriving yojson]
+end
+
+module WorkspaceEdit = struct
+  type t = { changes : (Lang.LUri.File.t * TextEdit.t list) list }
+  [@@deriving of_yojson]
+
+  let tok (uri, edits) =
+    ( Lang_.LUri.File.to_string_uri uri
+    , `List (List.map TextEdit.to_yojson edits) )
+
+  let to_yojson { changes } =
+    `Assoc [ ("changes", `Assoc (List.map tok changes)) ]
+end
diff --git a/lsp/workspace.mli b/lsp/workspace.mli
index f8b85633..ae684d56 100644
--- a/lsp/workspace.mli
+++ b/lsp/workspace.mli
@@ -23,3 +23,16 @@ end
 module DidChangeWorkspaceFoldersParams : sig
   type t = { event : WorkspaceFoldersChangeEvent.t } [@@deriving yojson]
 end
+
+module TextEdit : sig
+  type t =
+    { range : Lang.Range.t
+    ; newText : string
+    }
+  [@@deriving yojson]
+end
+
+module WorkspaceEdit : sig
+  type t = { changes : (Lang.LUri.File.t * TextEdit.t list) list }
+  [@@deriving yojson]
+end
diff --git a/petanque/agent.ml b/petanque/agent.ml
index 7a74b241..58ab3b20 100644
--- a/petanque/agent.ml
+++ b/petanque/agent.ml
@@ -106,30 +106,12 @@ let find_thm ~(doc : Fleche.Doc.t) ~thm =
     (* let point = (range.start.line, range.start.character) in *)
     Ok node
 
-let parse ~loc tac st =
-  let str = Gramlib.Stream.of_string tac in
-  let str = Coq.Parsing.Parsable.make ?loc str in
-  Coq.Parsing.parse ~st str
-
-(* Adaptor, should be supported in memo directly *)
-let eval_no_memo ~token (st, cmd) =
-  Coq.Interp.interp ~token ~intern:Vernacinterp.fs_intern ~st cmd
-
-let parse_and_execute_in ~token ~loc ~memo tac st =
-  (* To improve in memo *)
-  let eval = if memo then Fleche.Memo.Interp.eval else eval_no_memo in
-  let open Coq.Protect.E.O in
-  let* ast = parse ~token ~loc tac st in
-  match ast with
-  | Some ast -> eval ~token (st, ast)
-  | None -> Coq.Protect.E.ok st
-
 let execute_precommands ~token ~memo ~pre_commands ~(node : Fleche.Doc.Node.t) =
   match (pre_commands, node.prev, node.ast) with
   | Some pre_commands, Some prev, Some ast ->
     let st = prev.state in
     let open Coq.Protect.E.O in
-    let* st = parse_and_execute_in ~token ~memo ~loc:None pre_commands st in
+    let* st = Fleche.Doc.run ~token ~memo ?loc:None ~st pre_commands in
     (* We re-interpret the lemma statement *)
     Fleche.Memo.Interp.eval ~token (st, ast.v)
   | _, _, _ -> Coq.Protect.E.ok node.state
@@ -137,14 +119,17 @@ let execute_precommands ~token ~memo ~pre_commands ~(node : Fleche.Doc.Node.t) =
 let protect_to_result (r : _ Coq.Protect.E.t) : (_, _) Result.t =
   match r with
   | { r = Interrupted; feedback = _ } -> Error Error.Interrupted
-  | { r = Completed (Error (User (_loc, msg))); feedback = _ } ->
+  | { r = Completed (Error (User { msg; _ })); feedback = _ } ->
     Error (Error.Coq (Pp.string_of_ppcmds msg))
-  | { r = Completed (Error (Anomaly (_loc, msg))); feedback = _ } ->
+  | { r = Completed (Error (Anomaly { msg; _ })); feedback = _ } ->
     Error (Error.Anomaly (Pp.string_of_ppcmds msg))
   | { r = Completed (Ok r); feedback = _ } -> Ok r
 
 let proof_finished { Coq.Goals.goals; stack; shelf; given_up; _ } =
-  List.for_all CList.is_empty [ goals; shelf; given_up ] && CList.is_empty stack
+  let check_stack stack =
+    CList.(for_all (fun (l, r) -> is_empty l && is_empty r)) stack
+  in
+  List.for_all CList.is_empty [ goals; shelf; given_up ] && check_stack stack
 
 (* At some point we want to return both hashes *)
 module Hash_kind = struct
@@ -177,32 +162,31 @@ let default_opts = function
   | None -> { Run_opts.memo = true; hash = true }
   | Some opts -> opts
 
-(* XXX: EJGA, we should not need the [Coq.State.in_stateM] here and in run *)
 let start ~token ~doc ?opts ?pre_commands ~thm () =
   let open Coq.Compat.Result.O in
   let* node = find_thm ~doc ~thm in
   (* Usually single shot, so we don't memoize *)
-  let f () =
-    let opts = default_opts opts in
-    let memo, hash = (opts.memo, opts.hash) in
+  let opts = default_opts opts in
+  let memo, hash = (opts.memo, opts.hash) in
+  let execution =
     let open Coq.Protect.E.O in
     let+ st = execute_precommands ~token ~memo ~pre_commands ~node in
+    (* Note this runs on the resulting state, anyways it is purely functional *)
     analyze_after_run ~hash st
   in
-  let st = node.state in
-  Coq.State.in_stateM ~token ~st ~f () |> protect_to_result
+  protect_to_result execution
 
 let run ~token ?opts ~st ~tac () : (_ Run_result.t, Error.t) Result.t =
   let opts = default_opts opts in
   (* Improve with thm? *)
-  let loc = None in
   let memo, hash = (opts.memo, opts.hash) in
-  let f st =
+  let execution =
     let open Coq.Protect.E.O in
-    let+ st = parse_and_execute_in ~token ~memo ~loc tac st in
+    let+ st = Fleche.Doc.run ~token ~memo ?loc:None ~st tac in
+    (* Note this runs on the resulting state, anyways it is purely functional *)
     analyze_after_run ~hash st
   in
-  Coq.State.in_stateM ~token ~st ~f st |> protect_to_result
+  protect_to_result execution
 
 let goals ~token ~st =
   let f goals =
diff --git a/petanque/json_shell/server.ml b/petanque/json_shell/server.ml
index e59172fb..4bc765db 100644
--- a/petanque/json_shell/server.ml
+++ b/petanque/json_shell/server.ml
@@ -48,6 +48,11 @@ let accept_connection ~token conn =
 let create_socket ~address ~port ~backlog =
   let open Lwt_unix in
   let sock = socket PF_INET SOCK_STREAM 0 in
+  (* It is sometimes more convenient to allow pet-server to shadow a kind of
+     crashed one, so we allow to rebind the socket. It could be convenient at
+     some point to guard this over a command-line flag *)
+  let () = setsockopt sock SO_REUSEADDR true in
+  let () = setsockopt sock SO_REUSEPORT true in
   ( bind sock @@ ADDR_INET (Unix.inet_addr_of_string address, port) |> fun x ->
     ignore x );
   listen sock backlog;
diff --git a/petanque/test/basic_api.ml b/petanque/test/basic_api.ml
index a54eb6f2..debbe7e7 100644
--- a/petanque/test/basic_api.ml
+++ b/petanque/test/basic_api.ml
@@ -17,7 +17,7 @@ let trace hdr ?extra:_ msg =
 let message ~lvl:_ ~message = msgs := message :: !msgs
 let dump_msgs () = List.iter (Format.eprintf "%s@\n") (List.rev !msgs)
 
-let start ~token =
+let init ~token =
   let debug = false in
   Shell.trace_ref := trace;
   Shell.message_ref := message;
@@ -30,19 +30,17 @@ let start ~token =
   let* () = Shell.set_workspace ~token ~debug ~root in
   (* Careful to call [build_doc] before we have set an environment! [pet] and
      [pet-server] are careful to always set a default one *)
-  let* doc = Shell.build_doc ~token ~uri in
-  Agent.start ~token ~doc ~thm:"rev_snoc_cons" ()
+  Shell.build_doc ~token ~uri
 
 let extract_st { Agent.Run_result.st; _ } = st
 
-let main () =
+let snoc_test ~token ~doc =
   let open Coq.Compat.Result.O in
-  let token = Coq.Limits.create_atomic () in
   let r ~st ~tac =
     let st = extract_st st in
     Agent.run ~token ~st ~tac ()
   in
-  let* { st; _ } = start ~token in
+  let* { st; _ } = Agent.start ~token ~doc ~thm:"rev_snoc_cons" () in
   let* _premises = Agent.premises ~token ~st in
   let* st = Agent.run ~token ~st ~tac:"induction l." () in
   let h1 = Agent.State.hash st.st in
@@ -58,15 +56,62 @@ let main () =
   let* st = r ~st ~tac:"Qed." in
   Agent.goals ~token ~st:(extract_st st)
 
+let finished_stack_test ~token ~doc =
+  let open Coq.Compat.Result.O in
+  let r ~st ~tac =
+    let st = extract_st st in
+    Agent.run ~token ~st ~tac ()
+  in
+  let* { st; _ } = Agent.start ~token ~doc ~thm:"deepBullet" () in
+  let* st = Agent.run ~token ~st ~tac:"split." () in
+  let* st = r ~st ~tac:"-" in
+  let* st = r ~st ~tac:"now reflexivity." in
+  let* st = r ~st ~tac:"-" in
+  let* st = r ~st ~tac:"split." in
+  let* st = r ~st ~tac:"+" in
+  let* st = r ~st ~tac:"now reflexivity." in
+  let* st = r ~st ~tac:"+" in
+  let* { st; proof_finished; _ } = r ~st ~tac:"now reflexivity." in
+  (* Check that we properly detect no goals with deep stacks. *)
+  assert proof_finished;
+  let* st = Agent.run ~token ~st ~tac:"Qed." () in
+  Agent.goals ~token ~st:(extract_st st)
+
+let multi_shot_test ~token ~doc =
+  let open Coq.Compat.Result.O in
+  let* { st; _ } = Agent.start ~token ~doc ~thm:"rev_snoc_cons" () in
+  let* st =
+    Agent.run ~token ~st
+      ~tac:"induction l. idtac. - reflexivity. - now simpl; rewrite IHl. Qed."
+      ()
+  in
+  Agent.goals ~token ~st:(extract_st st)
+
+let main () =
+  let open Coq.Compat.Result.O in
+  let token = Coq.Limits.create_atomic () in
+  let* doc = init ~token in
+  let* g1 = snoc_test ~token ~doc in
+  let* g2 = finished_stack_test ~token ~doc in
+  let* g3 = multi_shot_test ~token ~doc in
+  Ok [ g1; g2; g3 ]
+
+let max = List.fold_left max min_int
+
 let check_no_goals = function
   | Error err ->
     Format.eprintf "error: in execution: %s@\n%!" (Agent.Error.to_string err);
     dump_msgs ();
     129
-  | Ok None -> 0
-  | Ok (Some _goals) ->
-    dump_msgs ();
-    Format.eprintf "error: goals remaining@\n%!";
-    1
+  | Ok glist ->
+    List.map
+      (function
+        | None -> 0
+        | Some _goals ->
+          dump_msgs ();
+          Format.eprintf "error: goals remaining@\n%!";
+          1)
+      glist
+    |> max
 
 let () = main () |> check_no_goals |> exit
diff --git a/petanque/test/test.v b/petanque/test/test.v
index cf5ed828..068876eb 100644
--- a/petanque/test/test.v
+++ b/petanque/test/test.v
@@ -8,3 +8,13 @@ Proof.
   - reflexivity.
   - simpl. rewrite IHl. simpl. reflexivity.
 Qed.
+
+(* This is for testing proof finished *)
+Lemma deepBullet : (1 = 1) /\ (21 = 21 /\ 22 = 22).
+Proof.
+split.
+- now reflexivity.
+- split.
+  + now reflexivity.
+  + now reflexivity.
+Qed.
diff --git a/plugins/explain_errors/main.ml b/plugins/explain_errors/main.ml
index 599a856e..fb72c4ba 100644
--- a/plugins/explain_errors/main.ml
+++ b/plugins/explain_errors/main.ml
@@ -10,8 +10,10 @@ let pp_goals ~token ~st =
   | Some proof -> (
     match Coq.Print.pr_goals ~token ~proof with
     | { Coq.Protect.E.r = Completed (Ok goals); _ } -> goals
-    | { Coq.Protect.E.r = Completed (Error (User msg | Anomaly msg)); _ } ->
-      Pp.(str "error when printing goals: " ++ snd msg)
+    | { Coq.Protect.E.r =
+          Completed (Error (User { msg; _ } | Anomaly { msg; _ }))
+      ; _
+      } -> Pp.(str "error when printing goals: " ++ msg)
     | { Coq.Protect.E.r = Interrupted; _ } ->
       Pp.str "goal printing was interrupted")
 
diff --git a/plugins/goaldump/main.ml b/plugins/goaldump/main.ml
index 4f753945..474e1fac 100644
--- a/plugins/goaldump/main.ml
+++ b/plugins/goaldump/main.ml
@@ -6,11 +6,10 @@ let of_execution ~io ~what (v : (_, _) Coq.Protect.E.t) =
   | { r; feedback = _ } -> (
     match r with
     | Coq.Protect.R.Completed (Ok goals) -> goals
-    | Coq.Protect.R.Completed (Error (Anomaly err))
-    | Coq.Protect.R.Completed (Error (User err)) ->
+    | Coq.Protect.R.Completed (Error (Anomaly { msg; _ }))
+    | Coq.Protect.R.Completed (Error (User { msg; _ })) ->
       let lvl = Io.Level.Error in
-      Io.Report.msg ~io ~lvl "error when retrieving %s: %a" what Pp.pp_with
-        (snd err);
+      Io.Report.msg ~io ~lvl "error when retrieving %s: %a" what Pp.pp_with msg;
       None
     | Coq.Protect.R.Interrupted -> None)
 
diff --git a/serlib/plugins/ltac2/ser_tac2expr.ml b/serlib/plugins/ltac2/ser_tac2expr.ml
index dd25268c..9671ffa5 100644
--- a/serlib/plugins/ltac2/ser_tac2expr.ml
+++ b/serlib/plugins/ltac2/ser_tac2expr.ml
@@ -12,6 +12,7 @@ module Loc = Ser_loc
 module CAst = Ser_cAst
 module Names = Ser_names
 module Libnames = Ser_libnames
+module Attributes = Ser_attributes
 
 open Sexplib.Std
 open Ppx_hash_lib.Std.Hash.Builtin