Support logging verification results in JSON#4951
Conversation
| } | ||
|
|
||
| public IEnumerable<ProofDependency> GetOrderedFullDependencies(IEnumerable<TrackedNodeComponent> components) { | ||
| return components.Select(GetFullIdDependency).OrderBy(dep => (dep.RangeString(), dep.Description)); |
There was a problem hiding this comment.
I find ordering by RangeString to be strange. Why not order on the unprinted object: dep.Range.StartToken or dep.Range ?
Also, Instead of the tuple, you can also use the C# chaining ordering API, OrderBy(dep => dep.Range.StartToken).ThenBy(dep => dep.Description), which I think is a little easier to read.
alex-chew
left a comment
There was a problem hiding this comment.
The changes since Remy's last approval LGTM.
| @@ -0,0 +1,453 @@ | |||
| // RUN: %diff "%s" "%s" | |||
There was a problem hiding this comment.
nit: is there a reason there's so many empty lines at the start of this file?
There was a problem hiding this comment.
It's because those lines used to be comments and the expected messages in some tests have line numbers based on the contents of this file before removing those comments. I should really update the test to remove the blank lines, and re-number the lines in the expected test output, but that'll be a bit time-consuming, so I haven't yet.
Description
Implement support for
dafny verify --log-format jsonto log the information provided in thetextformat logger in JSON format.Fixes #4907
How has this been tested?
logger/JsonLogger.dfyBy submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.