Extend activation events

[jonaskrask]

Currently extension (and the server) is only launched when the user opens a VDM file. Other activation events could be useful, such as:

• launch debug
• performing actions on non-open workspace folder (e.g. translate to latex)
• combinatorial testing "generate outline" options

[nickbattle]

I think this is quite important. I keep getting caught out by it myself(!), so new users could be very confused. I would say at least it needs to activate on a launch and CT.

[jonaskrask]

Hmm, this is not half as easy as I would have hoped. So I will not be able to have it ready for v1.1.0

[nickbattle]

Drat. OK. But please let's give it priority for the next release.

[nickbattle]

Given how easy it is to fall into this trap, I'll raise a new top level issue with the ECONNREFUSED message that you can get. Though I note that it only gives this error if you have opened another LSP server for a different project in the same workspace. If you just try to launch something without having opened any file at all, it just seems to ignore you and then silently times out.

[FrederikPM]

Looking in to this issue. Are the events mentioned in the issue still the ones we are interested in and/or are there any others? Just to be sure, 'launch debug' is the action of opening a folder without opening an editor and then go to "Run and Debug" and then start a debug session?

[nickbattle]

I think those are the important ones.

Yes, it means trying to launch something from the "Run and Debug" view (just just hitting F5 or CTRL-F5). If you open a file and use the "Launch | Debug" lens, you've already started the server (that created the lenses!).

[FrederikPM]

Okay. I have made a solution for the debug event where the debug adapter is started immediately after receiving the dap port from the server. However, the server does not seem to be ready to start a debug session at this time as it logs errors relating to the ClassMapper conversion stack and then closes the session:

ClassMapper conversion stack...

Converting list ASTModuleList
Converting ASTModule, name=DEFAULT
Converting ASTExplicitOperationDefinition, name=CPU in 'CPU' (console) at line 1:19
Field annotations ASTAnnotationList
Field defs ASTDefinitionList
Field name LexNameToken, name=CPU in 'CPU' (console) at line 1:19
Field type ASTRecordType, name=Plant in 'DEFAULT' (c:\Users\frdrk\Desktop\Repos\vdm-vscode\vdm_test_files\AlarmSL\alarm.vdmsl) at line 3:3
map ASTRecordType{name, fields, composed} to TCRecordType(name, fields, composed);

FAILED: java.lang.IllegalArgumentException: Can not set com.fujitsu.vdmj.tc.types.TCType field com.fujitsu.vdmj.tc.types.TCField.type to com.fujitsu.vdmj.tc.types.TCField

Is this to be expected? For now I have implemented a sleep of ~300ms between receiving the dap port and starting the debug session.

[nickbattle]

You're saying that doesn't happen if there is a 300ms delay?? That's very strange indeed. I suppose it might be a race between different parts, somehow. The mapping process is definitely single threaded. Could you turn on the server diags and get a fine level trace of what's happening?

[FrederikPM]

Yes that's correct. Here's the log file with level 'all': AlarmSL_lang_server.log

[nickbattle]

Hmm... OK, so it does seem to be concurrency interfering with the load/parse process. You'll see a concurrent modification exception and a NPE. The "Checking loaded files (initialized)..." message should also have a "Checked loaded files." complement, but it never gets there because the DAP processing trips it up.

I can try to put some interlocks into the server, but we don't really want to prevent the user from changing the spec while a DAP session is active.

Another way might be to wait for some response from the server before launching, to confirm that the initial parse is completed?

Let me look at it. For now, the delay will work but you're depending on the parse/check taking 300ms. Longer specs take longer!

[FrederikPM]

Hmm I see. At the moment I'm utilising the "onReady" callback from the vs-code client API which seems to fire immediately after the LSP initialization sequence. Ah if the delay is actually waiting on the parse/check then it definitely isn't the solution. I must admit that I'm not much into the DAP protocol and the messaging back and forth between the client and server. But isn't it possible for the server to halt the session 'somewhere' until it is finished with the initial check of the loaded files. Or is that what is done with the interlocks?

[nickbattle]

Yes, that's the idea of an interlock. I've just pushed something that should make the launch wait until the check has finished (up to 5 seconds, which may not be long enough... hmmm...). Anyway, can you give it a try? On the "development" branch of VDMJ.

[nickbattle]

Actually, a fixed pause isn't so bad. It will say "Specification being checked, cannot launch" on stderr if the spec is very large and takes longer than 5s, which just means you have to wait and try again.

It would be better for the user if there was some way for them to know that there was a "parse/checking" pause in progress?

[nickbattle]

If it helps, when the server has completed the initialization phase, it always sends back a dynamic registration for didChangeWatchedFiles. At that point, you can safely launch DAP. But if we could somehow let the user know with a "busy cursor" or something, that might be less confusing?

[FrederikPM]

That works on a number of the test examples. Yes I think it would be better if we could inform the user of the parse/checking being in progress. Okay. I'll look into if it is possible to register for an event, or to do something similar, for a dynamic registration for didChangeWatchedFiles from the server. Then some sort of "busy cursor" could be displayed between the user initiating the debug session (hitting F5 or similar) and the server being ready. Although it would possible only be a small notification in the bottom row of the IDE and/or a information pop-up. Ideally I think the debug panel should be displayed alongside the "busy cursor"..

[FrederikPM]

I have looked into if it is possible to get notified on the client side that the server has made a dynamic registration for didChangeWatchedFiles. However, as far as I can tell it is not. So we would have to come up with an alternative way to let the client know that the server has completed the initialization phase. I'm not sure if this would also be relevant for the "standard" use case where the user opens a VDM file but then quickly goes to the debug view and initiates a debug session, or if the server would have completed the initialization phase by then even on large specs. Do we also need to wait for the server to complete the initialization phase for the other events?

[nickbattle]

Perhaps we could introduce a bespoke notification? We've done this before for PO generation. So we would send something that indicated that the initial parse/check was complete at startup (and not otherwise, I guess?).

If specs get very large, they should still work(!) and so we may be in a situation where this phase can last 10s or more. But yes, it is still relevant for the case where a single file is opened - that causes the whole spec to be checked, and we must wait for that before allowing a debug/execute to begin.

So is there a way to catch a notification?

[FrederikPM]

Yes a notification should be straight forward to use and catch. As I understand it the initial parse/check always happens? So it either succeeds of fails? If so, then we could send a boolean along with the notification to indicate the status. Looking at the LSP specification it seems that there is support for server initiated progress. Alternatively, we could use this to indicate the start and end of the initial parse/check and maybe also a progress if the server is able to calculate it.

[nickbattle]

Interesting idea about server progress, but that's somewhat more difficult at the server end :) I've added a single "slsp/checked" notification that always occurs at the end of a completed parse/check (basically when you start or when you save the spec or do something that causes a build, like creating a new file). It's in the "development" branch. Can you detect that?

09:18:14.299: [FINE][1] <<< LSP { "jsonrpc" : "2.0", "method" : "slsp/checked", "params" : { "successful" : true } }

[FrederikPM]

Yes that works fine. Do you by any chance have a large spec that takes some time to parse/check that I can test it with? Would we also want to indicate that the parse/check is taking place whenever the user initiates a build by saving/adding a file?

[nickbattle]

I don't have a whopper spec to hand, I'm afraid. What I've done in the past is to find a largeish module without imports, and then copy that over and over again with a different "module " header and "end " trailer - that's a simple bash script, or your favourite script language?

The problem with letting the user know is that we don't want to bother them when it's very quick, but it might be helpful when it takes a while. But how do you know ahead of time how long it will take?

One approach might be to "time" the initial initialization check, and then only warn users if it is likely to take a long time on a subsequent save/create/move etc (maybe over 5 seconds, property controlled). Basically, warn them depending on how long it took last time. Might that be possible?

[FrederikPM]

Ah okay. Do you have an example of the syntax for the "module " header and "end " trailer? Hmm. I see. I'm not sure how feasible the indicator is with only the notification from the server, as the extension would then need to hook into all the UI actions that can trigger the parse/check on the server. I think that showing an indicator would be better suited for the server initiated progress if we choose to implement that at some time. That might be something we could do if any users raises a missing indicator as an issue?

[nickbattle]

Perhaps you could look at the examples we distribute with the tool?? Like resources/examples/VDMSL/shmemSL/shmem.vdmsl. So if you copy this and change the first line to module M1 and module M2 etc... while changing the last line to end M1, end M2 etc., that will create one large spec with multiple modules. If you create 20 or so, it should take a few seconds to check. You can do it with a small script?

[FrederikPM]

There's an implementation on the latest Github action for fpm/23 that enables launches the client and server on the activation events mentioned in the issue if you want to give it a go before i merge into development :)

[nickbattle]

Gave that a quick test... seems to work fine :-)