"Dafny > test"

[MikaelMayer]

I would like to just right-click and run Dafny > test, but this option is not present.
Currently, I select "build with custom arguments" and I replace everything with "test" or "test --no-verify".
it would be good to have the two options.
Test without verification is useful to check up if a property holds before proving it.

[keyboardDrummer]

Related/duplicate: #418

[MikaelMayer]

Indeed that will be good to integrate with VSCode.
For now, tasks assume that there is a build system that does not need input Dafny files. We might have this with project files, right? We need that "dafny test" be a valid command in a repository even without input because tasks are not provided with the input file name.
I think the menu "Dafny > test" is complementary to the tasks approach, adapted to different occasions.

[keyboardDrummer]

Instead of having commands redirect to the Dafny CLI, you could also add a task provider to the Dafny extension, that will generate user level tasks which invoke dafny. User level tasks can be run for any VSCode workspace on the machine.

After the task provider generates them, users can inspect them and will see something like this:

  "tasks": [
    {
      "label": "dafny verify",
      "type": "process",
      "command": "dafny",
      "args": [
        "verify",
        "${input:additionalArguments}",
        "${file}" // This variable is the current file
      ],
      "problemMatcher": []
    }
  ],
  "inputs": [
    {
      "id": "additionalArguments",
      "description": "additional arguments to pass to dafny verify",
      "type": "promptString"
    }
  ]

As you can see, they're easy to read and modify, and users can make variations of them that configure specific Dafny options. You can also attach a problemMatcher, that can let CLI diagnostics be shown in the editors. You can also define a boolean input that lets users decide whether to verify before running or testing.

You can also let the task provider check if there is a dfyconfig.toml in the root of the workspace, and then generate a tasks.json in the .vscode folder in that workspace, with tasks specific to that project file.

You can run defined tasks using a two-step process:

There's also the concept of a build and a test task, to which you can assign hotkeys.

[MikaelMayer]

Ok thanks for the clarification. From the documentation you shared with me, it looks like designing a user-level task generator is a bit more ambitious than what I implemented. It would be certainly be helpful for a class of Dafny users who otherwise just switch to the command line and write their various "make xxx" commands because they usually put everything in a makefile. Being able to get these commands from the dafny project sounds a good idea too.

In my case and with a lot of new Dafny users, they don't necessarily have project files, everything they need at the beginning is a way to run and test their files, using a keyboard shortcut (F5 or SHIFT+F5 as I suggest). It would be a bit overwhelming to have to define them the notion of project file/task/generate task/modify task.

So in short, I like your solution in general, but for what our need is currently, I wouldn't spend time myself implementing it.

[keyboardDrummer]

From the documentation you shared with me, it looks like designing a user-level task generator is a bit more ambitious than what I implemented.

Does it not seem about equivalent in complexity? You define objects like the JSON I quoted, but then in code. You don't have to do anything dynamic or do anything with project files.

It would be a bit overwhelming to have to define them the notion of project file/task/generate task/modify task.

I think there would be an extra step where the user asks VSCode to generate tasks, but after that invoking the tasks is similar to invoking the commands.

I would be careful in adding these commands, if later we might decide to use tasks instead and then want to remove the commands.

[MikaelMayer]

Does it not seem about equivalent in complexity? You define objects like the JSON I quoted, but then in code. You don't have to do anything dynamic or do anything with project files.

For now it looks like it's more obvious to you than to me. What I did was straightforward just to unblock new and existing users discovering the Run function and in need of the test function. I am still not sure about the tasks because I haven't looked deeply at them. I'd be happy to review a proposal about tasks, or even just a comparative workflow.

I would be careful in adding these commands, if later we might decide to use tasks instead and then want to remove the commands.

I think that, for discoverability purposes, I would very likely vote against any removal of commands in general easily accessible from the right-click, unless there is another compelling UI we can start using (e.g. the Run and Debug interface). Again, I have not studied tasks closely so I can't say if they will fit our needs or not, and from what I heard of you, I'm not yet convinced (but happy to change mind with more evidence).

[MikaelMayer]

I should recall about at least one user who would probably like to configure tasks if ever you want to make someone happier.

#383