Remy Willems

Could not reproduce locally by repeatedly running the test

There's a concurrency fix in https://github.com/dafny-lang/dafny/pull/5444 that has a chance of fixing this. Also, that PR improves the logging so the log contains less garbage, which is still present in...

Not fixed: https://github.com/dafny-lang/dafny/actions/runs/9115852973/job/25063146075?pr=5447

Somehow in the final compilation, one of the sources is not considered owned by the project, so its errors are reported as "out of project" diagnostics on the project file....

> I assume this is a temporary breakage, but this means a regression test should probably be added. Definitely. These reports are useful. We'll try to resolve them ASAP.

https://github.com/dafny-lang/dafny/actions/runs/9092347847/job/24988886184?pr=5437

Might be resolved by https://github.com/dafny-lang/dafny/pull/5444

I think the pattern is that statements ending in `}`, such as loops and conditionals, and statements with a `by` clause, do not need an `;` after the `}`. What...

Marking as enhancement not bug, since this is documented behavior.

Moved to `dafny-lang/dafny` since this does not seem IDE related.