/trace output is less helpful than it could be due to buffering

[0xabu]

Just a minor nitpick. When running Dafny with /trace, it produces output such as:

Verifying CheckWellformed$$_.foo ...
  [0.716 s, 2 proof obligations]  verified

Verifying Impl$$_.foo ...
  [187.421 s, 225 proof obligations]  verified

However, the line for "Verifying" only appears in the console window at the same time that the second line with the result information is printed, so you're never sure what Dafny is currently attempting to verify. I assume this could be fixed by adding an fflush()-equivalent between the two print statements.

[parno]

I've been annoyed by that too. However, I think that the trace is coming from Boogie, not Dafny, so you may need to file this on the Boogie repo.

[0xabu]

Done. Feel free to close this, if that's appropriate.

[parno]

Okay, I think it makes sense to close this, given that it needs to be fixed on the Boogie side.

[RustanLeino]

The behavior you're seeing indeed comes from Boogie. It's a feature! Boogie may actually do verifications in different orders or using multiple cores. It then sorts these to come out in the program order.

[cpitclaudel]

Do we really want trace to run things in parallel? Isn't this a profiling tool primarily?