From e399a6530ae3f361c809fad5887096c0b89df476 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 10 May 2024 14:27:20 +0200 Subject: [PATCH] [tmp] Example for Alex's problem. --- test/server/src/LanguageServer.ts | 34 +++++-- test/server/src/simple_client.ts | 154 +++++++++++++++++++++++++----- 2 files changed, 154 insertions(+), 34 deletions(-) diff --git a/test/server/src/LanguageServer.ts b/test/server/src/LanguageServer.ts index d785dbd0..51f58f75 100644 --- a/test/server/src/LanguageServer.ts +++ b/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, + root?: string ): Promise; + exit(): Promise; } 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 = {}, + 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, diff --git a/test/server/src/simple_client.ts b/test/server/src/simple_client.ts index 84ced23c..d4124cd3 100644 --- a/test/server/src/simple_client.ts +++ b/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 = { - 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) + }); });