search

dafny-lang / ide-vscode

VSCode IDE Integration for Dafny
https://marketplace.visualstudio.com/items?itemName=dafny-lang.ide-vscode
MIT License
25 stars 20 forks source link

offer "--filter-position" (and perhaps --filter-symbol) via the IDE #484

Open kjx opened 3 months ago

kjx commented 3 months ago

The CLI has --filter-position and perhaps --filter-symbol options to drive verification.

because I have a bad habit of 10,000 line files (or rather projects in just one file - long story) I tend to use that rather than the IDE verification.

it would be nice if I could click on a line and say "verify here" (i.e. --filter-position) or on (or inside) a declaration and verify that declaration (ie.. -filter-symbol)

keyboardDrummer commented 3 months ago

or on (or inside) a declaration and verify that declaration (ie.. -filter-symbol)

Can't you already do that? If you set 'automatic verification' to never:

image

Then you get these clickable icons in the gutter:

image

it would be nice if I could click on a line and say "verify here" (i.e. --filter-position)

For sure. I hope to build that, but I'm currently occupied with more pressing Dafny work

kjx commented 3 months ago

I don't mean to hassle - and I'm fine with working with the IDE on 2/3rds or the screen and the CLI on the other.

I'd like to direct verification to a single line rather than a whole enclosing declaration: it's often quicker for me..

Also, no idea why the language server (does it stay around) is often slower at e.g. verifying a single method than the CLI. Again I know it's bad practice (long story: waiting til I get to a milestone to refactor) to have a 12k line file - but that means e.g. the pre verification etc happens on the whole file each time, and the IDE appears slower to me at than the CLI...

anyway - I do appreciate what you're doing making the IDE better!

keyboardDrummer commented 3 months ago

I'd like to direct verification to a single line rather than a whole enclosing declaration: it's often quicker for me..

Yes, that's what I'd like to build. However, I don't have a timeline for when I'll do that.

Again I know it's bad practice (long story: waiting til I get to a milestone to refactor) to have a 12k line file

It's worse than you'd think. At the moment, parsing and resolution caching in the IDE only work for code that's in an unchanged file. You will see orders of magnitude improved IDE responsiveness if you use small files.