Dafny: How to call 'verifcationLogger:csv'?

Question

I'm trying to debug variable verification time in Dafny. I try to run verificationLogger, but get no output.

• I'm on Windows (but would be happy with a Linux solution)

• I set my path to the version of Dafny installed by the VSCode add-in, like so:

  set path=C:\Users\carlk.vscode-insiders\extensions\dafny-lang.ide-vscode-3.1.2\out\resources\4.2.0\github\dafny;%path%

• I run:

  dafny verify --verification-time-limit:15 --cores:6 --boogie -randomSeedIterations:10 --boogie -verificationLogger:csv repro1.dfy

but I see no CSV output.

Answer 1

I discovered that this works to give details of the new style: dafny verify --help

Then I can do:

dafny verify seq_of_sets_example7.dfy --verification-time-limit:45 --cores:20 --log-format text --boogie -randomSeedIterations:10 --boogie -vcsSplitOnEveryAssert | tee TestResults\del3.txt

Someone else might want a different # of cores, a different format (e.g. csv and no "tee"), not to use Split, etc.

(But now that I have *.txt and *.csv and *.trx formats, I don't know what to do with them. I'll start a new question.)

Answer 2

I am not familiar with new style of dafny command line options but this seems to work for me (I am using old style of command line option)

dafny  /compile:0 /verificationLogger:csv repo1.dfy 

I think problem is you are passing verificationLogger after boogie which means it is sent to boogie but verificationLogger is dafny option