Dafny Language Mode question

Dec 12, 2013 at 4:16 PM
Hi,

I like that the Dafny language mode in Visual Studio 2012 provides a 'Dafny' menu option where you can compile, verify, disable auto-verify, etc. It's quite handy :)

However, I was wondering if there will be more menu options and customization within Visual Studio in the near future? For example, it would be nice to access Dafny's command line switches from within Visual Studio or the ability to have multiple Dafny files in one solution (just like in multiple .cs files in one C# solution file). Stuffing multiple classes into one file isn't ideal which is what I find myself doing :(

Thanks,

Matt
Developer
Dec 13, 2013 at 7:56 AM
Hi Matt,

great to hear that you like the VS extension! We're definitely considering to add more features to the menu. Are there any particular options that you would like to have access to?

About support for multiple files: Bryan recently added support for including other Dafny files (see https://dafny.codeplex.com/SourceControl/changeset/c9fe93d11e86). When we discussed adding support for Dafny solutions a while ago we thought that simply being able to include other Dafny files would be sufficient for most use cases and could be supported uniformly for "console users" and "IDE users".

Best regards,

Valentin
Jan 13, 2014 at 6:22 PM
Hi Valentin,

Sorry for the delayed reply.

I'm mainly interested in the support of multiple files. Will this feature be available in the next major release?

The command line argument I use occasionally is '/proverMemoryLimit'. I've experimented with this option for timeout errors, but that's really the only argument I've used in a while. However, some text editors and IDEs have options for the command line arguments by creating a macro. For example, if I wanted to run 'dafny.exe /proverMemoryLimit:1000 -mv:"hello.dfy.model" "hello.dfy"' within an IDE, I could do so by clicking on a custom macro that was created. I think Visual Studio has this for C/C++ projects, but I was curious if this would be available in VS for Dafny.

A 'custom macro' option would be nice, but I am also understand the two separate users scenarios you mentioned. It's just an idea.

Best,

Matt
Developer
Jan 17, 2014 at 8:41 AM
Hi Matt,

thank you for the suggestion. I will check out the "custom macros" you mentioned.

The support for multiple files is included in the latest (1.8) release.

Best regards,

Valentin