Merge branch 'v9.1' into v9.0

Author: ejgallego

CHANGES.md

@@ -25,8 +25,8 @@
    #1050)
  - [layout-engine] Add background color for each box kind (@ejgallego,
    #1050)
- - [compiler] Fix handling of literate files (@ejgallego, #, reported
-   by @jim-portegies)
+ - [compiler] Fix handling of literate files (@ejgallego, #1056,
+   reported by @jim-portegies)
  - [rocq] Create output directory on .vo file save if it doesn't
    exists. This is very useful in the web context where we don't yet
    have a proper virtual FS setup, thus making the "Save .vo file"
@@ -40,6 +40,54 @@
    checking of Rocq's `Require`s when needed. The algorithm is not
    smart at all yet, as it invalidates all the requires for all open
    files. (@ejgallego, @helguo, #1059)
+ - [goals] New option (LSP, petanque, API) to display and retrieve
+   goals without the compacted context. See protocol docs for more
+   information. (@ejgallego, alexJ, #1065, cc #1043)
+ - [fleche] [rocq] New options and data fields to expose document
+   comments. This is experimental, pass the `--record_comments` flags
+   to `rocq-lsp`, `fcc`, or `pet-server` to enable it. Once this flag
+   is passed, comments for a document will be stored in the new
+   `doc.comments` field. (@ejgallego, alexJ, #1069, fixes #353)
+ - [hover] New debug option `show_pr_vernac_on_hover`, that will
+   re-print the sentence under point using the Rocq printer
+   (@ejgallego, alexJ, #1070)
+ - [petanque] New methods `proof_info` and `proof_info_at_pos` that
+   return information about the current proof. As of today they return
+   the proof name, text, range, ... (@DikieDick, @ejgallego, #1051)
+ - [petanque] New method `list_notations_in_statement` which returns
+   an analysis of notations appearing inside a Rocq statement
+   (@JulesViennotFranca, @ejgallego, #1017)
+ - [tools] New tool `rocq-checkdecls` for Rocq blueprints, inspired by
+   the Lean version (#785, @ejgallego, Andrej Bauer)
+ - [plugins] New demo plugin "baseline", that tries to proof existing
+   lemmas using a set of pre-fixed tactics (@ejgallego, Shachar
+   Itzhaky, Eytan Singher, #799)
+ - [tools] New tool `checkdecls` for Coq blueprint, inspired by the
+   Lean version (#785, @ejgallego, Andrej Bauer)
+ - [lsp] [rocq] Example of Ltac2 AST analysis using serlib's Analzyer
+   infra (@ejgallego, @jim-portegies, @DikieDick, #1058)
+ - [lsp controller] Log internal errors to user-facing log
+   (@ejgallego, #1074)
+ - [doc] Example typescript client connecting to the WASM-based lsp
+   server (@ejgallego, #626)
+ - [hover] When the `show_doc_on_hover` option is enabled, hover will
+   show coqdoc documentation when hovering on identifiers, using some
+   heuristics to infer it from the comment just before
+   it. Documentation is treated as Markdown. This feature is
+   experimental and limited to documentation comments on the same file.
+   (@ejgallego, #590)
+ - [plugins] New plugin to dump document data (@ejgallego, Stefania
+   Dumbrava, #1075)
+ - [fcc] New option `--trace-file` that will generate trace data for
+   visualizing with perfetto.dev (@ejgallego, AlexJ, Gaëtan Gilbert,
+   #1076)
+ - [fcc] New options `--save_vof` and `--load_vof` that can save a
+   Fleche version of a document to a `.vof` file, thus avoiding `.vo`
+   recompilation for example when calling `fcc --plugin=...` for a
+   given file (@ejgallego, Alexj, #1077)
+ - [vscode] Add config manager for handling client configuration
+   changes in the infoview. Add configuration option for number of
+   messages displayed (@Durbatuluk1701, #1067)
 
 # coq-lsp 0.2.4: (W)Activation
 ------------------------------

compiler/args.ml

@@ -1,3 +1,13 @@
+(************************************************************************)
+(* Copyright 2019 MINES ParisTech -- Dual License LGPL 2.1+ / GPL3+     *)
+(* Copyright 2019-2024 Inria      -- Dual License LGPL 2.1+ / GPL3+     *)
+(* Copyright 2024-2025 Emilio J. Gallego Arias -- LGPL 2.1+ / GPL3+     *)
+(* Copyright 2025      CNRS                    -- LGPL 2.1+ / GPL3+     *)
+(* Written by: Emilio J. Gallego Arias & coq-lsp contributors           *)
+(************************************************************************)
+(* Flèche => command-line compiler                                      *)
+(************************************************************************)
+
 module Display = struct
   type t =
     | Verbose
@@ -12,10 +22,14 @@ type t =
   ; debug : bool  (** run in debug mode *)
   ; display : Display.t  (** display level *)
   ; plugins : string list  (** Flèche plugins to load *)
+  ; trace_file : string option  (** Save flame profile to file *)
   ; max_errors : int option
         (** Maximum erros before aborting the compilation *)
   ; coq_diags_level : int
         (** Whether to include feedback messages in the diagnostics *)
+  ; record_comments : bool  (** Record comments (experimental) *)
+  ; save_vof : bool  (** Save a vof file *)
+  ; load_vof : bool  (** Load a vof file instead of compiling *)
   }
 
 let compute_default_plugins ~no_vo ~plugins =

compiler/cc.ml

@@ -5,4 +5,5 @@ type t =
   ; default : Coq.Workspace.t
   ; io : Fleche.Io.CallBack.t
   ; token : Coq.Limits.Token.t
+  ; save_vof : bool
   }

compiler/compile.ml

@@ -1,3 +1,13 @@
+(************************************************************************)
+(* Copyright 2019 MINES ParisTech -- Dual License LGPL 2.1+ / GPL3+     *)
+(* Copyright 2019-2024 Inria      -- Dual License LGPL 2.1+ / GPL3+     *)
+(* Copyright 2024-2025 Emilio J. Gallego Arias -- LGPL 2.1+ / GPL3+     *)
+(* Copyright 2025      CNRS                    -- LGPL 2.1+ / GPL3+     *)
+(* Written by: Emilio J. Gallego Arias & coq-lsp contributors           *)
+(************************************************************************)
+(* Flèche => command-line compiler                                      *)
+(************************************************************************)
+
 open Fleche
 
 let is_in_dir ~dir ~file = CString.is_prefix dir file
@@ -39,8 +49,22 @@ let guess_languageId file =
   | ".v.tex" -> "latex"
   | _ -> "rocq"
 
+let do_save_vof ~io ~token ~doc =
+  match Doc.save_vof ~token ~doc with
+  | Coq.Protect.E.{ r = Coq.Protect.R.Completed (Ok ()); feedback } ->
+    Io.Log.feedback "vof safe" feedback;
+    Io.Report.msg ~io ~lvl:Info "vof file saved"
+  | Coq.Protect.E.{ r = Completed (Error (User msg)); feedback }
+  | Coq.Protect.E.{ r = Completed (Error (Anomaly msg)); feedback } ->
+    Io.Log.feedback "vof safe" feedback;
+    Io.Report.msg ~io ~lvl:Error "error saving vof file %a" Coq.Pp_t.pp_with
+      msg.msg
+  | Coq.Protect.E.{ r = Interrupted; feedback } ->
+    Io.Log.feedback "vof safe" feedback;
+    Io.Report.msg ~io ~lvl:Error "saving vof file interrupted"
+
 let compile_file ~cc file : int =
-  let { Cc.io; root_state; workspaces; default; token } = cc in
+  let { Cc.io; root_state; workspaces; default; token; save_vof } = cc in
   Io.Report.msg ~io ~lvl:Info "compiling file %s" file;
   match Lang.LUri.(File.of_uri (of_string file)) with
   | Error _ -> 222
@@ -57,9 +81,38 @@ let compile_file ~cc file : int =
       save_diags_file ~doc;
       (* Vo file saving is now done by a plugin *)
       Theory.close ~uri;
+      if save_vof then do_save_vof ~io ~token ~doc;
       status_of_doc doc)
 
-let compile ~cc =
-  List.fold_left
-    (fun status file -> if status = 0 then compile_file ~cc file else status)
-    0
+let compile_file ~cc file : int =
+  let args () = [ ("file", `String file) ] in
+  NewProfile.profile "compile" ~args (fun () -> compile_file ~cc file) ()
+
+let oprofile = ref None
+
+let init_profile trace_file =
+  match trace_file with
+  | None -> ()
+  | Some file ->
+    let oc = Stdlib.open_out file in
+    let fmt = Format.formatter_of_out_channel oc in
+    oprofile := Some (oc, fmt);
+    NewProfile.init { output = fmt; fname = "fcc" }
+
+let finish_profile () =
+  match !oprofile with
+  | None -> ()
+  | Some (oc, fmt) ->
+    NewProfile.finish ();
+    Format.pp_print_flush fmt ();
+    Stdlib.close_out oc
+
+let compile ~cc ~trace_file files =
+  init_profile trace_file;
+  let finally = finish_profile in
+  let compile () =
+    List.fold_left
+      (fun status file -> if status = 0 then compile_file ~cc file else status)
+      0 files
+  in
+  Fun.protect ~finally compile

compiler/driver.ml

@@ -1,9 +1,10 @@
 (* Duplicated with coq_lsp *)
-let coq_init ~debug =
+let coq_init ~debug ~record_comments =
   let load_module = Dynlink.loadfile in
   let load_plugin = Coq.Loader.plugin_handler None in
   let vm, warnings = (true, None) in
-  Coq.Init.(coq_init { debug; load_module; load_plugin; vm; warnings })
+  Coq.Init.(
+    coq_init { debug; record_comments; load_module; load_plugin; vm; warnings })
 
 let replace_test_path exp message =
   let home_re = Str.regexp (exp ^ ".*$") in
@@ -42,8 +43,12 @@ let go ~int_backend args =
       ; debug
       ; files
       ; plugins
+      ; trace_file
       ; max_errors
       ; coq_diags_level
+      ; record_comments
+      ; save_vof
+      ; load_vof = _
       } =
     args
   in
@@ -52,7 +57,7 @@ let go ~int_backend args =
   let io = Output.init ~display ~perfData ~coq_diags_level in
   (* Initialize Coq *)
   let debug = debug || Fleche.Debug.backtraces || !Fleche.Config.v.debug in
-  let root_state = coq_init ~debug in
+  let root_state = coq_init ~debug ~record_comments in
   let roots = if List.length roots < 1 then [ Sys.getcwd () ] else roots in
   let default = Coq.Workspace.default ~debug ~cmdline in
   let () = Coq.Limits.select_best int_backend in
@@ -62,7 +67,44 @@ let go ~int_backend args =
   let workspaces = List.map make_ws roots in
   List.iter (log_workspace ~io) workspaces;
   let () = apply_config ~max_errors in
-  let cc = Cc.{ root_state; workspaces; default; io; token } in
+  let cc = Cc.{ root_state; workspaces; default; io; token; save_vof } in
   (* Initialize plugins *)
   plugin_init plugins;
-  Compile.compile ~cc files
+  Compile.compile ~cc ~trace_file files
+
+let go_vof args =
+  let { Args.cmdline = _
+      ; roots = _
+      ; display
+      ; debug = _
+      ; files
+      ; plugins
+      ; trace_file = _
+      ; max_errors = _
+      ; coq_diags_level
+      ; record_comments = _
+      ; save_vof = _
+      ; load_vof = _
+      } =
+    args
+  in
+  let open Fleche in
+  (* Initialize logging; we skip Rocq's init *)
+  let fb_handler = Coq.Init.mk_fb_handler Coq.Protect.fb_queue in
+  ignore (Feedback.add_feeder fb_handler);
+  plugin_init plugins;
+  let perfData = Option.is_empty fcc_test in
+  let io = Output.init ~display ~perfData ~coq_diags_level in
+  let in_file = List.nth files 0 in
+  let in_vof = Filename.(remove_extension in_file) ^ ".vof" in
+  let doc = Doc.doc_of_disk ~in_file:in_vof in
+  Io.Report.msg ~io ~lvl:Info "vof file loaded";
+  Io.Report.msg ~io ~lvl:Info "document has %d nodes" (List.length doc.nodes);
+  Io.Report.msg ~io ~lvl:Info "calling plugins for [Theory.Register.Completed]";
+  (* Call plugins for the .vof file *)
+  let token = Coq.Limits.Token.create () in
+  Theory.Register.Completed.fire ~io ~token ~doc;
+  0
+
+let go ~int_backend (args : Args.t) =
+  if args.load_vof then go_vof args else go ~int_backend args

compiler/fcc.ml

@@ -2,9 +2,9 @@
 open Cmdliner
 open Fcc_lib
 
-let fcc_main int_backend roots display debug plugins files coqlib findlib_config
-    ocamlpath rload_path load_path require_libraries no_vo max_errors
-    coq_diags_level =
+let fcc_main int_backend roots display debug plugins trace_file files coqlib
+    findlib_config ocamlpath rload_path load_path require_libraries no_vo
+    max_errors coq_diags_level record_comments save_vof load_vof =
   let vo_load_path = rload_path @ load_path in
   let args = [] in
   let cmdline =
@@ -25,8 +25,12 @@ let fcc_main int_backend roots display debug plugins files coqlib findlib_config
       ; files
       ; debug
       ; plugins
+      ; trace_file
       ; max_errors
       ; coq_diags_level
+      ; record_comments
+      ; save_vof
+      ; load_vof
       }
   in
   Driver.go ~int_backend args
@@ -51,10 +55,22 @@ let plugins : string list Term.t =
   let doc = "Compiler plugins to load" in
   Arg.(value & opt_all string [] & info [ "plugin" ] ~docv:"PLUGINS" ~doc)
 
+let trace_file : string option Term.t =
+  let doc = "Activate profiling and output a Rocq flame graph in FILE" in
+  Arg.(value & opt (some string) None & info [ "trace_file" ] ~docv:"FILE" ~doc)
+
 let no_vo : bool Term.t =
   let doc = "Don't generate .vo files at the end of compilation" in
   Arg.(value & flag & info [ "no_vo" ] ~doc)
 
+let save_vof : bool Term.t =
+  let doc = "Save a .vof file with Fleche-specific metadata" in
+  Arg.(value & flag & info [ "vof" ] ~doc)
+
+let load_vof : bool Term.t =
+  let doc = "Save a .vof file with Fleche-specific metadata" in
+  Arg.(value & flag & info [ "load_vof" ] ~doc)
+
 let max_errors : int option Term.t =
   let doc = "Maximum errors in files before aborting" in
   Arg.(
@@ -97,9 +113,10 @@ let fcc_cmd : int Cmd.t =
   let fcc_term =
     let open Coq.Args in
     Term.(
-      const fcc_main $ int_backend $ roots $ display $ debug $ plugins $ file
-      $ coqlib $ findlib_config $ ocamlpath $ rload_paths $ qload_paths
-      $ ri_from $ no_vo $ max_errors $ coq_diags_level)
+      const fcc_main $ int_backend $ roots $ display $ debug $ plugins
+      $ trace_file $ file $ coqlib $ findlib_config $ ocamlpath $ rload_paths
+      $ qload_paths $ ri_from $ no_vo $ max_errors $ coq_diags_level
+      $ record_comments $ save_vof $ load_vof)
   in
   let exits = Exit_codes.[ fatal; stopped; scheduled; uri_failed ] in
   Cmd.(v (Cmd.info "fcc" ~exits ~version ~doc ~man) fcc_term)

controller/lsp_core.ml

@@ -221,7 +221,7 @@ end = struct
       Hashtbl.remove _rtable id;
       f pr |> answer ~ofn_rq ~id
     | None ->
-      L.trace "consuem" "can't consume cancelled request: %d" id;
+      L.trace "consume" "can't consume cancelled request: %d" id;
       ()
 
   let cancel ~ofn_rq ~code ~message id : unit =
@@ -381,6 +381,8 @@ let get_pp_format params =
     get_pp_format_from_config ()
   | None -> get_pp_format_from_config ()
 
+let get_compact params = Option.default true (obool_field "compact" params)
+
 let get_pretac params =
   Option.append (ostring_field "command" params) (ostring_field "pretac" params)
 
@@ -399,9 +401,10 @@ let get_goals_mode params =
 
 let do_goals ~params =
   let pp_format = get_pp_format params in
+  let compact = get_compact params in
   let mode = get_goals_mode params in
   let pretac = get_pretac params in
-  let handler = Rq_goals.goals ~pp_format ~mode ~pretac () in
+  let handler = Rq_goals.goals ~pp_format ~compact ~mode ~pretac () in
   do_position_request ~postpone:true ~handler ~params
 
 let do_definition =
@@ -614,7 +617,7 @@ let dispatch_notification ~io ~ofn ~token ~state ~method_ ~params : unit =
   (* NOOPs *)
   | "initialized" -> ()
   (* Generic handler *)
-  | msg -> L.trace "no_handler" "%s" msg
+  | msg -> L.trace "no_handler for notification" "%s" msg
 
 let dispatch_state_notification ~io ~ofn ~token ~state ~method_ ~params :
     State.t =
@@ -781,6 +784,9 @@ let dispatch_or_resume_check ~io ~ofn ~state =
 let dispatch_or_resume_check ~io ~ofn ~state =
   try Some (dispatch_or_resume_check ~io ~ofn ~state) with
   | U.Type_error (msg, obj) ->
+    Fleche.Io.(Report.msg ~io ~lvl:Error)
+      "JSON Parsing Error when handling protocol input: %s\n\
+       see log for more details" msg;
     L.trace_object msg obj;
     Some (Yield state)
   | Lsp_exit ->
@@ -793,12 +799,17 @@ let dispatch_or_resume_check ~io ~ofn ~state =
        coq-lsp internal error and should be fixed *)
     let bt = Printexc.get_backtrace () in
     let iexn = Exninfo.capture exn in
-    L.trace "process_queue" "%s"
+    let pp_msg = CErrors.(iprint iexn) in
+    Fleche.Io.(Report.msg ~io ~lvl:Error)
+      "Internal Error when handling command: %a\n\
+       See log for more details, please report to rocq-lsp developers"
+      Coq.Pp_t.pp pp_msg;
+    L.trace "dispatch_or_resume_check" "%s"
       (if Printexc.backtrace_status () then "bt=true" else "bt=false");
     (* let method_name = Lsp.Base.Message.method_ com in *)
     (* L.trace "process_queue" "exn in method: %s" method_name; *)
     L.trace "print_exn [OCaml]" "%s" (Printexc.to_string exn);
-    L.trace "print_exn [Coq  ]" "%a" Coq.Pp_t.pp_with CErrors.(iprint iexn);
+    L.trace "print_exn [Coq  ]" "%a" Coq.Pp_t.pp pp_msg;
     L.trace "print_bt  [OCaml]" "%s" bt;
     Some (Yield state)