[tmp] Example for Alex's problem.

test/server/src/LanguageServer.ts

@@ -10,7 +10,7 @@ import { URI } from "vscode-uri";
 let serverBin = os.platform() === "win32" ? "coq-lsp.exe" : "coq-lsp";
 let projectRoot = path.join(__dirname, "..", "..", "..");
 
-let serverPath = path.join(
+let _serverPath = path.join(
   projectRoot,
   "_build",
   "install",
@@ -19,7 +19,9 @@ let serverPath = path.join(
   serverBin,
 );
 
-let ocamlPath = path.join(projectRoot, "_build", "install", "default", "lib");
+let serverPath = "coq-lsp"
+
+// let ocamlPath = path.join(projectRoot, "_build", "install", "default", "lib");
 
 export function toURI(s: string) {
   return URI.parse(s).toString();
@@ -43,15 +45,17 @@ export function openExample(filename: string) {
 export interface LanguageServer extends rpc.MessageConnection {
   initialize(
     initializeParameters?: Partial<Protocol.InitializeParams>,
+    root?: string
   ): Promise<void>;
+
   exit(): Promise<void>;
 }
 
 export function start(): LanguageServer {
-  let childProcess = cp.spawn(serverPath, [], {
+  let childProcess = cp.spawn(serverPath, ['--int_backend=Mp', '--bt'], {
     env: {
       ...process.env,
-      OCAMLPATH: ocamlPath,
+      // OCAMLPATH: ocamlPath,
     },
   });
   let connection = rpc.createMessageConnection(
@@ -62,15 +66,17 @@ export function start(): LanguageServer {
 
   const initialize = async (
     initializeParameters: Partial<Protocol.InitializeParams> = {},
+    root : string = projectRoot,
   ) => {
     initializeParameters = {
       processId: process.pid,
-      workspaceFolders: [
-        {
-          uri: toURI(projectRoot),
-          name: "coq-lsp",
-        },
-      ],
+      // workspaceFolders: [
+      //   {
+      //     uri: toURI(root),
+      //     name: "coq-lsp",
+      //   },
+      // ],
+      initializationOptions: { eager_diagnostics: false },
       capabilities: {
         textDocument: {
           publishDiagnostics: {
@@ -81,6 +87,14 @@ export function start(): LanguageServer {
       ...initializeParameters,
     };
 
+    const log = (message : string | any, data?: any) => {
+      console.log(`${message} | ${data}`);
+    };
+
+    const tracer : rpc.Tracer = { log };
+
+    connection.trace(rpc.Trace.Verbose, tracer);
+
     await connection.sendRequest(
       Protocol.InitializeRequest.type,
       initializeParameters,

test/server/src/simple_client.ts

@@ -1,42 +1,148 @@
 import * as Protocol from "vscode-languageserver-protocol";
 import * as Types from "vscode-languageserver-types";
-import * as LS from "./LanguageServer"; 
+import * as LS from "./LanguageServer";
+
+function printMessage(params : Protocol.LogMessageParams) {
+  console.log(`${params.type} ${params.message}`);
+}
+
+function printDiags(params : Protocol.PublishDiagnosticsParams) {
+    console.log(`${params.diagnostics.length} diagnostics received`);
+    console.log(params.diagnostics);
+}
 
 async function start() {
   let languageServer = LS.start();
+  languageServer.trace
+  languageServer.onNotification(Protocol.LogMessageNotification.type, printMessage);
+
   let initializeParameters: Partial<Protocol.InitializeParams> = {
-    rootPath: ".",
-    rootUri: ".",
+    rootPath: "/home/egallego/tmp/serapy/CompCert",
+    rootUri: "file:///home/egallego/tmp/serapy/CompCert",
     trace: "verbose",
-    workspaceFolders: null,
+    // workspaceFolders: null,
   };
-  let result = await languageServer.initialize(initializeParameters);
+  let result = await languageServer.initialize(
+    initializeParameters,
+    '/home/egallego/tmp/serapy/CompCert',
+  );
   return languageServer;
 }
 
-async function sendSimpleDoc(languageServer : LS.LanguageServer, text : string) {
-    let textDocument = Types.TextDocumentItem.create(
-        "file.v",
-        "coq",
-        0,
-        text,
-      );
-    await languageServer.sendNotification(
-      Protocol.DidOpenTextDocumentNotification.type,
-        {
-          textDocument,
-        },
-      );
+var version = 0;
+let file = "/home/egallego/tmp/serapy/CompCert/file.v";
+
+async function openDoc(languageServer : LS.LanguageServer, text : string) {
+  let textDocument = Types.TextDocumentItem.create(
+    file,
+    "coq",
+    version,
+    text,
+  );
+
+  await languageServer.sendNotification(
+    Protocol.DidOpenTextDocumentNotification.type,
+    {
+      textDocument,
+    },
+  );
 }
-function printDiags(params : Protocol.PublishDiagnosticsParams) {
-    console.log(`${params.diagnostics.length} diagnostics received`);
-    console.log(params.diagnostics);
+
+async function updateDoc(languageServer : LS.LanguageServer, text : string) {
+  version++;
+
+  let textDocument : Types.VersionedTextDocumentIdentifier = Types.VersionedTextDocumentIdentifier.create(
+    file,
+    version,
+  );
+
+  let contentChanges : Protocol.TextDocumentContentChangeEvent[] = [
+    { text }
+  ]
+
+  console.log("Updating doc");
+
+  await languageServer.sendNotification(
+    Protocol.DidChangeTextDocumentNotification.type,
+    {
+      textDocument,
+      contentChanges,
+    },
+  );
 }
 
+let doc1 = `
+(* From https://github.com/ejgallego/coq-lsp/issues/487 *)
+(* Requires CompCert so that's hard to to test right now *)
+
+Require Import Coqlib.
+Require Import Integers.
+Require Import Values Memory.
+Require Import Cminor CminorSel.
+Require Import SelectOp.
+Section CMCONSTR.
+Variable ge: genv.
+Variable sp: val.
+Variable e: env.
+Variable m: mem.
+
+Definition unary_constructor_sound (cstr: expr -> expr) (sem: val -> val) : Prop
+ := forall le a x,eval_expr ge sp e m le a x ->
+  exists v, eval_expr ge sp e m le (cstr a) v /\\ Val.lessdef (sem x) v.
+
+About unary_constructor_sound.
+
+Lemma eval_mulimm_base: forall n, unary_constructor_sound
+   (mulimm_base n) (fun x => Val.mul x (Vint n)).
+induction n.
+econstructor.
+unfold mulimm_base.
+unfold Int.one_bits.
+unfold map.
+simpl.
+`
+
+let doc2 = `
+(* From https://github.com/ejgallego/coq-lsp/issues/487 *)
+(* Requires CompCert so that's hard to to test right now *)
+
+Require Import Coqlib.
+Require Import Integers.
+Require Import Values Memory.
+Require Import Cminor CminorSel.
+Require Import SelectOp.
+Section CMCONSTR.
+Variable ge: genv.
+Variable sp: val.
+Variable e: env.
+Variable m: mem.
+
+Definition unary_constructor_sound (cstr: expr -> expr) (sem: val -> val) : Prop
+ := forall le a x,eval_expr ge sp e m le a x ->
+  exists v, eval_expr ge sp e m le (cstr a) v /\\ Val.lessdef (sem x) v.
+
+About unary_constructor_sound.
+
+Lemma eval_mulimm_base: forall n, unary_constructor_sound
+   (mulimm_base n) (fun x => Val.mul x (Vint n)).
+induction n.
+econstructor.
+unfold mulimm_base.
+unfold Int.one_bits.
+unfold map.
+
+`
+
 start().then((ls) => {
     console.log("Starting");
     ls.onNotification(Protocol.PublishDiagnosticsNotification.type, printDiags);
-    sendSimpleDoc(ls, "Definition a := 3. Variable (b : nat). Error. ").then(() => {
-        setTimeout(() => { ls.exit(); }, 5000)
-    })
+    openDoc(ls, doc1).then(() => {
+        setTimeout(() => {
+          updateDoc(ls, doc2).then(() => {
+            setTimeout(() => {
+              ls.exit();
+            }, 5000);
+          })
+        }, 5000)
+    });
 });