Merge branch 'main' into v8.19

.github/workflows/build.yml

@@ -100,6 +100,7 @@ jobs:
 
       - name: Install Coq and SerAPI into OPAM switch
         run: |
+          opam install lwt logs # Also build pet-server
           opam install memprof-limits # We need to do this to avoid coq-lsp rebuilding Coq below due to deptops
           opam install vendor/coq/{coq-core,coq-stdlib,coqide-server,coq}.opam
           opam install vendor/coq-serapi/coq-serapi.opam
@@ -110,6 +111,9 @@ jobs:
       - name: Test `coq-lsp` in installed switch
         run: opam exec -- fcc examples/Demo.v
 
+      - name: Test `pet-server` is built
+        run: opam exec -- which pet-server
+
   client-compile:
     runs-on: ubuntu-latest
     defaults:

CHANGES.md

@@ -1,11 +1,6 @@
-# unreleased
-------------
+# coq-lsp 0.1.9: Hasta el 40 de Mayo...
+---------------------------------------
 
- - Added new heatmap feature allowing timing data to be seen in the
-   editor. Can be enabled with the `Coq LSP: Toggle heatmap`
-   comamnd. Can be configured to show memory usage. Colors and
-   granularity are configurable. (@Alizter and @ejgallego, #686,
-   grants #681).
  - new option `show_loc_info_on_hover` that will display parsing debug
    information on hover; previous flag was fixed in code, which is way
    less flexible. This also fixes the option being on in 0.1.8 by
@@ -70,6 +65,11 @@
    #348)
  - fix Coq performance view display (@ejgallego, #663, regression in
    #513)
+ - Added new heatmap feature allowing timing data to be seen in the
+   editor. Can be enabled with the `Coq LSP: Toggle heatmap`
+   command. Can be configured to show memory usage. Colors and
+   granularity are configurable. (@Alizter and @ejgallego, #686,
+   grants #681).
  - allow more than one input position in `selectionRange` LSP call
    (@ejgallego, #667, fixes #663)
  - new VSCode commands to allow to move one sentence backwards /
@@ -114,40 +114,73 @@
    (@ejgallego, @Alizter, #689, #693)
  - Better types `coq/perfData` call (@ejgallego @Alizter, #689)
  - New server option to enable / disable `coq/perfData` (@ejgallego, #689)
- - New cleint option to enable / disable `coq/perfData` (@ejgallego, #717)
+ - New client option to enable / disable `coq/perfData` (@ejgallego, #717)
  - The `coq-lsp.document` VSCode command will now display the returned
    JSON data in a new editor (@ejgallego, #701)
- - New server option to enable / disable `coq/perfData` (@ejgallego,
-   #689)
  - Update server settings on the fly when tweaking them in VSCode.
    Implement `workspace/didChangeConfiguration` (@ejgallego, #702)
  - [Coq API] Add functions to retrieve list of declarations done in
    .vo files (@ejallego, @eytans, #704)
  - New `petanque` API to interact directly with Coq's proof
-   engine. (@ejgallego, @gbdrt, #703, thanks to Alex Sanchez-Stern)
+   engine. (@ejgallego, @gbdrt, Laetitia Teodorescu #703, thanks to
+   Alex Sanchez-Stern for many insightful feedback and testing)
  - New `petanque` JSON-RPC `pet.exe`, which can be used à la SerAPI
    to perform proof search and more (@ejgallego, @gbdrt, #705)
+ - New `pet-server.exe` TCP server for keep-alive sessions (@gbdrt,
+   #697)
  - Always dispose UI elements. This should improve some strange
    behaviors on extension restart (@ejgallego, #708)
- - Support Coq meta-commands (Reset, Reset Initial, Back) They are
-   actually pretty useful to hint the incremental engine to ignore
-   changes in some part of the document (@ejgallego, #709)
+ - [code] Added new heatmap feature allowing timing data to be seen in
+   the editor. Can be enabled with the `Coq LSP: Toggle heatmap`
+   comamnd. Can be configured to show memory usage. Colors and
+   granularity are configurable. (@Alizter and @ejgallego, #686,
+   grants #681).
+ - [server] Support Coq meta-commands (Reset, Reset Initial, Back)
+   They are actually pretty useful to hint the incremental engine to
+   ignore changes in some part of the document (@ejgallego, #709)
  - JSON-RPC library now supports all kind of incoming messages
    (@ejgallego, #713)
- - New `coq/viewRange` notification, from client to server, than hints
-   the scheduler for the visible area of the document; combined with
-   the new lazy checking mode, this provides checking on scroll, a
-   feature inspired from Isabelle IDE (@ejgallego, #717)
- - Have VSCode wait for full LSP client shutdown on server
+ - [code/server] New `coq/viewRange` notification, from client to
+   server, than hints the scheduler for the visible area of the
+   document; combined with the new lazy checking mode, this provides
+   checking on scroll, a feature inspired from Isabelle IDE
+   (@ejgallego, #717)
+ - [code] Have VSCode wait for full LSP client shutdown on server
    restart. This fixes some bugs on extension restart (finally!)
    (@ejgallego, #719)
- - Center the view if cursor goes out of scope in
+ - [code] Center the view if cursor goes out of scope in
    `sentenceNext/sentencePrevious` (@ejgallego, #718)
  - Switch Flèche range encoding to protocol native, this means UTF-16
-   for now (Léo Stefanesco, @ejgallego, #624, fixes #620, #621)
+   code points for now (Léo Stefanesco, @ejgallego, #624, fixes #620,
+   #621)
  - Give `Goals` panel focus back if it has lost it (in case of
    multiple panels in the second viewColumn of Vscode) whenever
    user navigates proofs (@Alidra @ejgallego, #722, #725)
+ - `fcc`: new option `--diags_level` to control whether Coq's notice
+   and info messages appear as diagnostics
+ - [code] Display the continous/on-request checking mode in the status bar,
+   allow to change it by clicking on it (@ejgallego, #721)
+ - Add an example of multiple workspaces (@ejgallego, @Blaisorblade,
+   #611)
+ - Don't show types of un-expanded goals. We should add an option for
+   this, but we don't have the cycles (@ejgallego, #730, workarounds
+   #525 #652)
+ - Support for `.lv / .v.tex` TeX files with embedded Coq code
+   (@ejgallego, #727)
+ - Don't expand bullet goals at previous levels by default
+   (@ejgallego, @Alizter, #731 cc #525)
+ - [petanque] Return basic goal information after `run_tac`, so we
+   avoid a `goals` round-trip for each tactic (@gbdrt, @ejgallego,
+   #733)
+ - [coq] Add support for reading glob files metadata (@ejgallego,
+   #735)
+ - [petanque] Return extra premise information: file name, position,
+   raw_text, using the above support for reading .glob files
+   (@ejgallego, #735)
+ - [code] Display server status using the `LanguageStatusItem`
+   facility, for now we display version and checking status
+   information (moved from #721), and we also allow to toggle the
+   checking mode from there (@ejgallego, #728)
 
 # coq-lsp 0.1.8.1: Spring fix
 -----------------------------

README.md

@@ -20,6 +20,8 @@ document checking, advanced error recovery, hybrid Coq/markdown document
 support, multiple workspace support, positional goals and information panel,
 performance data, extensible command-line compiler, plugin system, and more.
 
+See the [coq-lsp User Manual](./etc/doc/USER_MANUAL.md) for more information.
+
 `coq-lsp` aims to provide a seamless, modern interactive theorem proving
 experience, as well as to serve as a maintainable platform for research and UI
 integration with other projects.
@@ -37,6 +39,7 @@ and web native usage, providing quite a few extra features from vanilla Coq.
 
 - [🎁 Features](#-features)
   - [⏩ Incremental Compilation and Continuous Document Checking](#-incremental-compilation-and-continuous-document-checking)
+  - [👁 On-demand, Follow The Viewport Document Checking](#-on-demand-follow-the-viewport-document-checking)
   - [🧠 Smart, Cache-Aware Error Recovery](#-smart-cache-aware-error-recovery)
   - [🥅 Whole-Document Goal Display](#-whole-document-goal-display)
   - [🗒️ Markdown Support](#️-markdown-support)
@@ -58,6 +61,7 @@ and web native usage, providing quite a few extra features from vanilla Coq.
   - [✅ Vim](#-vim)
   - [🩱 Neovim](#-neovim)
   - [🐍 Python](#-python)
+- [⇨ `coq-lsp` users and extensions](#-coq-lsp-users-and-extensions)
 - [🗣️ Discussion Channel](#️-discussion-channel)
 - [☎ Weekly Calls](#-weekly-calls)
 - [❓FAQ](#faq)
@@ -87,6 +91,14 @@ restart your proof session where you left it at the last time.
 Incremental support is undergoing refinement, if `coq-lsp` rechecks when it
 should not, please file a bug!
 
+### 👁 On-demand, Follow The Viewport Document Checking
+
+`coq-lsp` does also support on-demand checking. Two modes are available: follow
+the cursor, or follow the viewport; the modes can be toggled using the Language
+Status Item in Code's bottom right corner:
+
+<img alt="On-demand checking" height="572px" src="etc/img/on_demand.gif"/>
+
 ### 🧠 Smart, Cache-Aware Error Recovery
 
 `coq-lsp` won't stop checking on errors, but supports (and encourages) working
@@ -307,6 +319,17 @@ guide](./CONTRIBUTING.md)
 - Interact programmatically with Coq files by using the [Python `coq-lsp` client](https://github.com/sr-lab/coq-lsp-pyclient)
   by Pedro Carrott and Nuno Saavedra.
 
+## ⇨ `coq-lsp` users and extensions
+
+The below projects are using `coq-lsp`, we recommend you try them!
+
+- [CoqPilot uses Large Language Models to generate multiple potential proofs and then uses coq-lsp to typecheck them](https://github.com/JetBrains-Research/coqpilot).
+- [jsCoq: use Coq from your browser](https://github.com/jscoq/jscoq)
+- [Pytanque: a Python library implementing RL Environments](https://github.com/LLM4Coq/pytanque)
+- [ViZX: A Visualizer for the ZX Calculus](https://github.com/inQWIRE/ViZX).
+- [The Waterproof vscode extension helps students learn how to write mathematical proofs](https://github.com/impermeable/waterproof-vscode).
+- [Yade: Support for the YADE diagram editor in VSCode](https://github.com/amblafont/vscode-yade-example).
+
 ## 🗣️ Discussion Channel
 
 `coq-lsp` discussion channel it at [Coq's
@@ -332,7 +355,7 @@ recommend that if you are installing via opam, you use the following branches
 that have some fixes backported:
 
 - For 8.20: No known problems
-- For 8.19: No known problems
+- For 8.19: `opam pin add coq-core https://github.com/ejgallego/coq.git#v8.19+lsp`
 - For 8.18: `opam pin add coq-core https://github.com/ejgallego/coq.git#v8.18+lsp`
 - For 8.17: `opam pin add coq-core https://github.com/ejgallego/coq.git#v8.17+lsp`
 - For 8.16: `opam pin add coq      https://github.com/ejgallego/coq.git#v8.16+lsp`

compiler/args.ml

@@ -14,6 +14,8 @@ type t =
   ; plugins : string list  (** Flèche plugins to load *)
   ; max_errors : int option
         (** Maximum erros before aborting the compilation *)
+  ; coq_diags_level : int
+        (** Whether to include feedback messages in the diagnostics *)
   }
 
 let compute_default_plugins ~no_vo ~plugins =

compiler/compile.ml

@@ -22,7 +22,7 @@ let save_diags_file ~(doc : Fleche.Doc.t) =
   let file = Lang.LUri.File.to_string_file doc.uri in
   let file = Filename.remove_extension file ^ ".diags" in
   let diags = Fleche.Doc.diags doc in
-  Fleche.Compat.format_to_file ~file ~f:Output.pp_diags diags
+  Coq.Compat.format_to_file ~file ~f:Output.pp_diags diags
 
 (** Return: exit status for file:
 
@@ -47,9 +47,7 @@ let compile_file ~cc file : int =
     let workspace = workspace_of_uri ~io ~workspaces ~uri ~default in
     let files = Coq.Files.make () in
     let env = Doc.Env.make ~init:root_state ~workspace ~files in
-    let raw =
-      Fleche.Compat.Ocaml_414.In_channel.(with_open_bin file input_all)
-    in
+    let raw = Coq.Compat.Ocaml_414.In_channel.(with_open_bin file input_all) in
     let () = Theory.create ~io ~token ~env ~uri ~raw ~version:1 in
     match Theory.Check.maybe_check ~io ~token with
     | None -> 102

compiler/driver.ml

@@ -36,12 +36,20 @@ let apply_config ~max_errors =
     max_errors
 
 let go ~int_backend args =
-  let { Args.cmdline; roots; display; debug; files; plugins; max_errors } =
+  let { Args.cmdline
+      ; roots
+      ; display
+      ; debug
+      ; files
+      ; plugins
+      ; max_errors
+      ; coq_diags_level
+      } =
     args
   in
   (* Initialize event callbacks, in testing don't do perfData *)
   let perfData = Option.is_empty fcc_test in
-  let io = Output.init display ~perfData in
+  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

compiler/fcc.ml

@@ -3,7 +3,8 @@ open Cmdliner
 open Fcc_lib
 
 let fcc_main int_backend roots display debug plugins files coqlib coqcorelib
-    ocamlpath rload_path load_path require_libraries no_vo max_errors =
+    ocamlpath rload_path load_path require_libraries no_vo max_errors
+    coq_diags_level =
   let vo_load_path = rload_path @ load_path in
   let ml_include_path = [] in
   let args = [] in
@@ -19,7 +20,16 @@ let fcc_main int_backend roots display debug plugins files coqlib coqcorelib
   in
   let plugins = Args.compute_default_plugins ~no_vo ~plugins in
   let args =
-    Args.{ cmdline; roots; display; files; debug; plugins; max_errors }
+    Args.
+      { cmdline
+      ; roots
+      ; display
+      ; files
+      ; debug
+      ; plugins
+      ; max_errors
+      ; coq_diags_level
+      }
   in
   Driver.go ~int_backend args
 
@@ -91,7 +101,7 @@ let fcc_cmd : int Cmd.t =
     Term.(
       const fcc_main $ int_backend $ roots $ display $ debug $ plugins $ file
       $ coqlib $ coqcorelib $ ocamlpath $ rload_paths $ qload_paths $ ri_from
-      $ no_vo $ max_errors)
+      $ no_vo $ max_errors $ coq_diags_level)
   in
   let exits = Exit_codes.[ fatal; stopped; scheduled; uri_failed ] in
   Cmd.(v (Cmd.info "fcc" ~exits ~version ~doc ~man) fcc_term)

compiler/output.ml

@@ -9,7 +9,6 @@ let pp_diags fmt dl =
 (* We will use this when we set eager diagnotics to true *)
 let diagnostics ~uri:_ ~version:_ _diags = ()
 let fileProgress ~uri:_ ~version:_ _progress = ()
-let perfData ~uri:_ ~version:_ _perf = ()
 
 (* We print trace and messages, and perfData summary *)
 module Fcc_verbose = struct
@@ -24,26 +23,30 @@ module Fcc_verbose = struct
   let perfData ~uri:_ ~version:_ { Fleche.Perf.summary; _ } =
     Format.(eprintf "[perfdata]@\n@[%s@]@\n%!" summary)
 
+  let serverVersion _ = ()
+  let serverStatus _ = ()
+
   let cb =
-    Fleche.Io.CallBack.{ trace; message; diagnostics; fileProgress; perfData }
+    Fleche.Io.CallBack.
+      { trace
+      ; message
+      ; diagnostics
+      ; fileProgress
+      ; perfData
+      ; serverVersion
+      ; serverStatus
+      }
 end
 
 (* We print trace, messages *)
 module Fcc_normal = struct
   let trace _ ?extra:_ _ = ()
-  let message = Fcc_verbose.message
-  let perfData = Fcc_verbose.perfData
-
-  let cb =
-    Fleche.Io.CallBack.{ trace; message; diagnostics; fileProgress; perfData }
+  let cb = { Fcc_verbose.cb with trace }
 end
 
 module Fcc_quiet = struct
-  let trace _ ?extra:_ _ = ()
   let message ~lvl:_ ~message:_ = ()
-
-  let cb =
-    Fleche.Io.CallBack.{ trace; message; diagnostics; fileProgress; perfData }
+  let cb = { Fcc_normal.cb with message }
 end
 
 let set_callbacks (display : Args.Display.t) =
@@ -56,16 +59,18 @@ let set_callbacks (display : Args.Display.t) =
   Fleche.Io.CallBack.set cb;
   cb
 
-let set_config ~perfData =
+let set_config ~perfData ~coq_diags_level =
+  let show_coq_info_messages = coq_diags_level > 1 in
+  let show_notices_as_diagnostics = coq_diags_level > 0 in
   Fleche.Config.(
     v :=
       { !v with
         send_perf_data = perfData
       ; eager_diagnostics = false
-      ; show_coq_info_messages = true
-      ; show_notices_as_diagnostics = true
+      ; show_coq_info_messages
+      ; show_notices_as_diagnostics
       })
 
-let init display ~perfData =
-  set_config ~perfData;
+let init ~display ~coq_diags_level ~perfData =
+  set_config ~perfData ~coq_diags_level;
   set_callbacks display

compiler/output.mli

@@ -1,5 +1,9 @@
 (** Initialize Console Output System *)
-val init : Args.Display.t -> perfData:bool -> Fleche.Io.CallBack.t
+val init :
+     display:Args.Display.t
+  -> coq_diags_level:int
+  -> perfData:bool
+  -> Fleche.Io.CallBack.t
 
 (** Report progress on file compilation *)
 (* val report : unit -> unit *)