Merge pull request #523 from ejgallego/workaround_slow_pp_render

[vscode] Limit the number of messages displayed in the goal window

CHANGES.md

@@ -45,6 +45,12 @@
    will set them now (@ejgallego, #517)
  - Preliminary plugin API for completion events (@ejgallego, #518,
    fixes #506)
+ - Limit the number of messages displayed in the goal window to 101,
+   as to workaround slow render of Coq's pretty printing format. This
+   is an issue for example in Search where we can get thousand of
+   results. We also speed up the rendering a bit by not hashing twice,
+   and fix a parameter-passing bug. (@ejgallego, #523, reported by
+   Anton Podkopaev)
 
 # coq-lsp 0.1.6: Peek
 ---------------------

README.md

@@ -301,15 +301,29 @@ See our [list of frequently-asked questions](./etc/FAQ.md).
 
 ## ⁉️ Troubleshooting and Known Problems
 
+### Known problems
+
+- Current rendering code can be slow with complex goals and messages, if that's
+  the case, please open an issue and set the option `Coq LSP > Method to Print
+  Coq Terms` to 0 as a workaround.
+- `coq-lsp` can fail to interrupt Coq in some cases, such as `Qed` or type class
+  search. If that's the case, please open an issue, we have a experimental
+  branch that solves this problem that you can try.
+- Working with multiple files in Coq < 8.17 requires a Coq patch, see below for
+  instructions.
+- If you install `coq-lsp/VSCode` simultaneously with the `VSCoq` Visual Studio
+  Code extension, Visual Studio Code gets confused and neither of them may
+  work. `coq-lsp` will warn about that. You can disable the `VSCoq` extension as
+  a workaround.
+
+### Troubleshooting
+
 - Some problems can be resolved by restarting `coq-lsp`, in Visual Studio Code,
   `Ctrl+Shift+P` will give you access to the `coq-lsp.restart` command.
   You can also start / stop the server from the status bar.
 - In VSCode, the "Output" window will have a "Coq LSP Server Events" channel
   which should contain some important information; the content of this channel
   is controlled by the `Coq LSP > Trace: Server` option.
-- If you install `coq-lsp` simultaneously with VSCoq, VSCode gets confused and
-  neither of them may work. `coq-lsp` will warn about that. If you know how to
-  improve this, don't hesitate to get in touch with us.
 
 ### 📂 Working With Multiple Files
 

editor/code/views/info/Info.tsx

@@ -70,13 +70,17 @@ export function InfoPanel() {
 
   if (!goals) return null;
 
+  // We limit the number of messages as to workaround slow rendering
+  // in pretty print mode, to be fixed.
+  let messages = goals.messages.slice(0, 100);
+
   return (
     <div className="info-panel-container">
       <div className="info-panel">
         <FileInfo textDocument={goals.textDocument} position={goals.position}>
           <Goals goals={goals.goals} />
           <Program program={goals.program} />
-          <Messages messages={goals.messages} />
+          <Messages messages={messages} />
         </FileInfo>
       </div>
       {!goals.error ? null : (

editor/code/views/info/Message.tsx

@@ -1,14 +1,15 @@
-import objectHash from "object-hash";
+// import objectHash from "object-hash";
 import { Message } from "../../lib/types";
 import { PpString } from "../../lib/types";
 import { CoqPp } from "./CoqPp";
 
 export function Message({
+  key,
   message,
 }: {
+  key: React.Key;
   message: PpString | Message<PpString>;
 }) {
-  let key = objectHash(message);
   let text =
     typeof message === "string"
       ? message

editor/code/views/info/Messages.tsx

@@ -1,4 +1,4 @@
-import objectHash from "object-hash";
+// import objectHash from "object-hash";
 import { Message as Msg } from "../../lib/types";
 import { PpString } from "../../lib/types";
 import { Details } from "./Details";
@@ -15,7 +15,8 @@ export function Messages({ messages }: MessagesParams) {
     <Details summary={`Messages (${count})`} open={open}>
       <ul className="messageList">
         {messages.map((value, idx) => {
-          let key = objectHash(value);
+          // let key = objectHash(value);
+          let key = idx;
           return <Message key={key} message={value} />;
         })}
       </ul>