Client update to connect to ViperServer's language server #113

WissenIstNacht · 2020-10-12T19:52:42Z

closes #114
closes #115, i.e. same settings are still used and some of them are passed to ViperServer to configure verification. However, some settings values are unused
closes #116, i.e. we decided to simply remove debugging functionality

aterga · 2020-10-22T17:16:34Z

client/.gitignore

+npm-debug.log
+languageServerExample.log
+server/


Please remove the last line (as the server extension is obsolete)

This is not "server" as in the directory that holds the code for the legacy typescript server. That's the folder that held javascript files that bloated this PR.

aterga · 2020-10-22T17:17:57Z

client/src/ExtensionState.ts

@@ -43,7 +45,9 @@ export class State {

    public static unitTest: UnitTestCallback;

-    public static autoVerify: boolean = true;
+    // OG


Unclear comments

aterga · 2020-10-22T17:18:44Z

client/src/ExtensionState.ts

-        if(!this.checkedSettings){
-            Log.error("Error getting timeout, there are no checked Settings available, default to no timeout.");
-            return 0;
+        if (!this.checkedSettings) {


If this is a temporary stub, please add a comment that says so.

aterga · 2020-10-22T17:20:05Z

client/src/extension.ts

@@ -10,12 +10,22 @@
 // The module 'vscode' contains the VS Code extensibility API
 // Import the module and reference it with the alias vscode in your code below

+
+
+//============================================================================//


This very useful comment should be duplicated in README.

aterga · 2020-10-22T17:20:54Z

client/src/extension.ts

-        State.client.onNotification(Commands.Log, (msg: { data: string, logLevel: LogLevel }) => {
-            Log.log((Log.logLevel >= LogLevel.Debug ? "S: " : "") + msg.data, msg.logLevel);
+        State.client.onNotification(Commands.Log, (data, logLevel) => {
+            // OG


What does OG stand for?

aterga · 2020-10-22T17:23:27Z

client/src/extension.ts

@@ -584,8 +591,7 @@ function considerStartingBackend(backendName: string) {
            backend: backendName,
            manuallyTriggered: true,
            forceRestart: false,
-            isViperServerEngine: false //TODO: how to set that correctly
-
+            isViperServerEngine: true


This option is not necessary anymore as the concept of ViperServerEngine is obsolete. If it's easy to carve out the code that mentioned this concept, please do so; otherwise, add an explaination in the comments.

aterga · 2020-10-22T17:25:06Z

client/src/extension.ts

-        State.client.onNotification(Commands.Progress, (msg: { data: Progress, logLevel: LogLevel }) => {
-            Log.progress(msg.data, msg.logLevel);
-        });
-        State.client.onNotification(Commands.ToLogFile, (msg: { data: string, logLevel: LogLevel }) => {


Why are some of the notifications removed?

Because the Command.Error notification is currently not used by the server.

aterga · 2020-10-22T17:26:57Z

client/src/ViperProtocol.ts

@@ -47,6 +52,7 @@ export class Commands {
    static BackendReady = "BackendReady";//BackendReadyParams


What do these comments mean? e.g. //BackendReadyParams

I guess the author wrote them to indicate the type of object the corresponding method takes as input.

aterga · 2020-10-22T17:28:41Z

client/src/Log.ts

@@ -119,7 +119,9 @@ export class Log {
    private static doLog(message: string, logLevel: LogLevel) {
        let timing = this.logTiming ? this.prettyUptime() + ' ' : '';
        message = this.prefix(logLevel) + message;
-        if (!Log.logLevel || Log.logLevel >= logLevel) {
+        // OG


Unclear comment

aterga · 2020-10-22T17:30:23Z

client/src/ExtensionState.ts

        // The server is implemented in node
-        let serverModule = State.context.asAbsolutePath(path.join('server', 'server.js'));
+        // let serverModule = State.context.asAbsolutePath(path.join('server', 'server.js'));


aterga · 2020-10-22T17:30:35Z

client/src/ExtensionState.ts

-            run: { module: serverModule, transport: TransportKind.ipc },
-            debug: { module: serverModule, transport: TransportKind.ipc, options: debugOptions }
-        }
+        // let serverOptions: ServerOptions = {


aterga · 2020-10-22T17:34:23Z

client/src/ExtensionState.ts

-                    resolve();
-                });
+                Log.log("Initiating language server shutdown.", LogLevel.Info);
+                State.client.stop()


Why is it not necessary anymore to shut down the server?

This is implicitly / automatically taken care of by taken care of by the LSP. The call to stop() initiates a "termination handshake" between client and server. The server is shut down during the course of that handshake.

aterga · 2020-10-22T17:35:17Z

client/src/VerificationController.ts

-        let backendName = State.activeBackend;
-        let backendSettings = State.checkedSettings.verificationBackends.find(config => config.name == backendName)
-        return backendSettings.stoppingTimeout;
+        return 10000;


Add a comment that this value should be taken from the settings (I assume).

aterga · 2020-10-22T17:36:43Z

client/src/VerificationController.ts

-                            let diag = new vscode.Diagnostic(range, item.message, item.severity-1);
-                            diagnostics.push( diag );
-                        }) 
+                        let diagnostics: vscode.Diagnostic[] = params.diagnostics;                        


aterga · 2020-10-22T17:38:15Z

client/src/VerificationController.ts

-                        let diagnostics: vscode.Diagnostic[] = [];                        
-                        JSON.parse(params.diagnostics).forEach( item => {
-                            let range = new vscode.Range(item.range.start.line, item.range.start.character, item.range.end.line, item.range.end.character);
-                            let diag = new vscode.Diagnostic(range, item.message, item.severity-1);


I suspect that the yellow squiggly line issue comes from the fact that the severity level is not set properly.
If you want to use only one severity level, at least I would recommend to use the one that corresponds to "red" (i.e. error but not warning).

aterga

Thank you for this PR. I added some comments.

WissenIstNacht · 2020-10-23T09:08:55Z

This PR is part of the ongoing refactoring process to outsource the extension's language server to ViperServer codebase (see the corresponding PR in ViperServer).

So far, Viper IDE extension comprised a client, a server, and a verification engine. With the refactoring of ViperServer, the server and the engine have been merged into a single codebase. I.e., most of the functionality that was previously part of the extension's server has been moved to ViperServer. Accordingly, the server's code has been deleted from this branch.

The extension's client has mostly been unaffected by these changes. Some adaptations have been made to allow the client to directly connect and communicate with ViperServer instead of connecting to the extension's server.

Some of the extension's features have been refactored yet. Refactoring steps that are yet to be done are documented by corresponding issues (#114, #115, #116)

aterga

Thank you for the revision.

Before merging the PR, the issues labeled "PR 113" should be resolved.

Additionally, we should add the compilation and debugging instructions to the README.

…he client, and disallows 'Stable' build versions in pre-releases

… try to get added before the extension has been properly started

… build" This reverts commit e88f008.

This was referenced Oct 22, 2020

Viper IDE refactoring: Version checking / updating #114

Closed

Viper IDE refactoring: Settings #115

Closed

Viper IDE refactoring: Debugger #116

Closed

aterga reviewed Oct 22, 2020

View reviewed changes

aterga requested changes Oct 22, 2020

View reviewed changes

aterga requested changes Oct 25, 2020

View reviewed changes

aterga mentioned this pull request Jan 6, 2021

Port Viper IDE to the LSP frontend of ViperServer viperproject/viperserver#28

Closed

Valentin added 8 commits July 5, 2022 19:01

Connected ViperServer to Viper IDE

4857a78

verification running, diagnostics showing

d3f2d58

main verification cycle error-free

896486a

added cache flushing and proper termination

6e602b0

implemented Carbon/Silicon swap

13f2b6d

Made backend swap work

30b9c38

start ViperServer on cp to LSP frontent

bb5f859

removed files from git, cleaned up code

684ae26

ArquintL added 5 commits September 30, 2022 15:04

removes additional ViperServer logging

f6b440f

extends & fixes linting

7727088

adds test configuration to test against nightly builds

4502e77

fixes tests with multiple setting files

31b94ce

some improvements

d3f80e5

ArquintL approved these changes Sep 30, 2022

View reviewed changes

ArquintL added 17 commits September 30, 2022 19:06

improves Viper-IDE if server could not be started

7551a78

fixes CI for pre-releases, adds mechanism to detect pre-releases to t…

55cb174

…he client, and disallows 'Stable' build versions in pre-releases

since the extension registers handlers early on, we ignore tasks that…

ce0ce3a

… try to get added before the extension has been properly started

another attempt to make unit tests more stable

7ae3023

another attept to make unit tests more stable

7013780

fixes a timeout during a unit test

6b544f6

temporarily disables testing against the nightly ViperServer build

e88f008

increases timeout

092dbb8

improves .gitignore files

50881f9

Reverts "temporarily disables testing against the nightly ViperServer…

915b91f

… build" This reverts commit e88f008.

cleanup

fdb323d

stops CI from testing against a local ViperServer version

03f03a6

fixes flags in CI

7c5c00e

test

8e2ed11

another attempt to fix boolean expressions in CI

a35492e

yet another attempt

bca78bb

disables CI test against local ViperServer version (now for real)

f2cd2f8

ArquintL merged commit 41fae85 into viperproject:master Oct 3, 2022

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Client update to connect to ViperServer's language server #113

Client update to connect to ViperServer's language server #113

WissenIstNacht commented Oct 12, 2020 •

edited by ArquintL

aterga Oct 22, 2020

WissenIstNacht Oct 22, 2020

aterga Oct 22, 2020

aterga Oct 22, 2020

aterga Oct 22, 2020

aterga Oct 22, 2020

WissenIstNacht Oct 23, 2020

aterga Oct 22, 2020

aterga Oct 22, 2020

WissenIstNacht Oct 23, 2020

aterga Oct 22, 2020

WissenIstNacht Oct 23, 2020

aterga Oct 22, 2020

aterga Oct 22, 2020

aterga Oct 22, 2020

aterga Oct 22, 2020

WissenIstNacht Oct 22, 2020

aterga Oct 22, 2020

aterga Oct 22, 2020

aterga Oct 22, 2020

aterga left a comment

WissenIstNacht commented Oct 23, 2020

aterga left a comment •

edited

		@@ -47,6 +52,7 @@ export class Commands {
		static BackendReady = "BackendReady";//BackendReadyParams

Client update to connect to ViperServer's language server #113

Client update to connect to ViperServer's language server #113

Conversation

WissenIstNacht commented Oct 12, 2020 • edited by ArquintL

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

aterga left a comment

Choose a reason for hiding this comment

WissenIstNacht commented Oct 23, 2020

aterga left a comment • edited

Choose a reason for hiding this comment

WissenIstNacht commented Oct 12, 2020 •

edited by ArquintL

aterga left a comment •

edited