Support logging verification results in JSON #4951
Conversation
atomb
requested review from
robin-aws and
MikaelMayer
and removed request for
robin-aws
| @@ -83,5 +83,9 @@ public class ProofDependencyManager { | |||
| throw new ArgumentException($"Malformed dependency ID: {component.SolverLabel}"); | |||
| } | |||
| } | |||
|
|
|||
| 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.
| @@ -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.