Provide launch and tasks files

[mortenhaahr]

I suggest adding a launch.json and tasks.json to the project that easily allows newcomers to get started with debugging/building the project in VSCode.

[mortenhaahr]

I have created the files myself but I don't have the right to push my patch into a branch.

[nickbattle]

You mean getting started with debugging VDMJ itself using Java for VSCode? That would probably make sense (though I'm still using Eclipse, out of habit). The easiest way to do this is for you to create a pull request on this repo, then I can review and merge it, assuming it looks right. I know that @leouk has managed to work with VDMJ in VSCode, so we should also compare with what he's done.

My first thought is that you would presumably have to do this for all projects within the repository - there are several?

I will try to monitor this issue, but we're still travelling (currently in Bremen) so there will be delays!

[leouk]

Creating the launch is somewhat straightforward. Tasks are more sophisticated. Only needed tasks for ANTLR complications. And create launch as needed.

Nick’s right that they may get stale and hard to maintain, but I get the point they are useful.

Perhaps a “launch” example would suffice?

I know from my students tha the imported examples (say alarm) had fixed launches, and they hadn’t realised: they wanted to ply in the debugger like I was playing. But they were getting “stuck” by some fixed launch behaviour. So it’s not a straightforward choice.

Perhaps the launch examples with tasks etc is the way forward?

L

[mortenhaahr]

I was thinking something like the patch I have submitted.
Simple enough to maintain and gives the user an idea of how to get started.

launch_and_tasks.txt

[mortenhaahr]

And yes I was thinking debugging VDMJ itself.
My motivation was that I wanted to see what was happening "behind the scenes" and found it difficult.
There are probably many use cases I haven't thought of

[leouk]

I use this task to clear the VSCode cache, which is important in some circumstances for ANTLR - Ie for any tool that generates code in the development sources to avoid VSCode getting confused
{
// See https://go.microsoft.com/fwlink/?LinkId=733558
// for the documentation about the tasks.json format
"version": "2.0.0",
"tasks": [
{
"label": "clear-editor-history",
"command": "${command:workbench.action.clearEditorHistory}"
}
]
}

[leouk]

If you look at the launch.json in VDMToolkit
plugins/vdm2isa/.vscode/launch.json

you will see various launch confit for debugging VDMJ itself. This also works for lsp

plugins/vdm2isa-lsp/.vscode/launch.json

In fact, if you look at the .vscode of all plugins you will see slight variations in launch config.

One that I like is the ability to set the starting directory, which allows for test code to have relative paths!

[leouk]

@mortenhaahr don't think I have your email, so will make a comment here (for Nick as well, whom I do have the email!) :-), about the Chess game.

I've ported your PP chess to SL. As you will see, it's pretty much 1-1 (i.e. you didn't need PP at all)? Also, I noticed that your model is very much like a program in VDM (e.g. there are barely any specifications beyond the main game (e.g. I would have expected to see some in the moves of each of the pieces).

That means there might be plenty of "illegal" behaviours possible in your spec, that it so happens you don't take advantage of but others could/would.

The idea of having it as a ADT (abstract data type) works well. Any public type becomes struct export, any public function becomes export. Private functions are not exported; same for operations. Protected? types become non struct exports. Instance variables and invariants become state and invariant, and constructors become state initialisers.

Have. a look in VDM_Toolkit .VDM_Toolkit/experiments/vdm/Chesss

Best,
Leo