Using VSCode extension to measure variability (e.g. verificationLogger, randomSeedIterations)

[CarlKCarlK]

I'm seeing a lot of variability in the time of verification (see
https://dafny.org/latest/DafnyRef/DafnyRef#1365-debugging-variable-verification).

What advice to folks have for debugging this within VSCode? Can you run with verificationLogger and randomSeedIterations easily? Can you see resources used?

Thanks,
Carl

[MikaelMayer]

You can right-click on a Dafny file, Build with custom arguments, and replace everything with -compile:0 -randomSeedIterations:5 -verificationLogger:csv
The results will be available in the TestResults folder as explained in the link you provided:

[CarlKCarlK]

Thanks, I ended up getting things working on the command line. Here are my notes on the commands (in a Windows CMD console):

@rem add vscode's Dafny to path
set path=C:\Users\carlk\.vscode-insiders\extensions\dafny-lang.ide-vscode-3.1.2\out\resources\4.2.0\github\dafny;%path%
@rem get help on the verify subcommand
dafny verify --help
@rem run different ways
dafny verify seq_of_sets_example7.dfy --verification-time-limit:10 --cores:20 --log-format csv --boogie -randomSeedIterations:10
@rem dafny verify seq_of_sets_example7.dfy --verification-time-limit:10 --cores:20 --log-format csv --boogie -randomSeedIterations:10 --boogie -vcsSplitOnEveryAssert

Others might want different values for the time limit, cores, # seed iterations, log format, and whether to use Split.

(So, I now have this running, but I don't have a good understanding of which log format to use or how to use the logging results to improve my verification.)

[MikaelMayer]

You should use the dafny-reportgenerator tool. It's a bit heavyweight but can summarize the results nicely.

What it does is that it regroups results for a single method, so you can see how many times they fail and how many time they succeed.
If you have 1 success and 9 failures for a single method, it's that your proofs are brittle. If you have 10 successes and 0 failures, your proofs are currently stable.
If you have 0 success and 10 failures, Dafny can't prove it.