overturetool / vdm-vscode

Visual Studio Code extension for VDM language support
GNU General Public License v3.0
21 stars 6 forks source link

"Add VDM Run Configuration" gives wrong defaultName #214

Open nickbattle opened 12 months ago

nickbattle commented 12 months ago

The "Add VDM Run Configuration" menu option builds a launch entry with an incorrectly set defaultName (and the wrong title, though that is harmless). For example:

    {
        "name": "Launch VDM Debug from f[nat](1,2,3)`DEFAULT",
        "type": "vdm",
        "request": "launch",
        "noDebug": false,
        "defaultName": "f[nat](1,2,3)",
        "command": "print f[nat](1,2,3)"
    }

The "command" is correct, but the defaultName is set to the launch expression and the "name" has the module name and expression the wrong way round. There's a similar problem in VDM++ specs.

leouk commented 12 months ago

Incidentally, the was something my students were experiencing as well: this "name" with the expression was leading to an XDebug print out of the VDM SL file without starting the interpreter.

nickbattle commented 12 months ago

@leouk That's very strange. I just get the following, when trying to run f: set of bool -> nat, passing {true, false}

Module f({true, false}) not loaded
Init terminated.

Session disconnected.