dafny-lang / dafny-reportgenerator

A tool for analyzing and reporting on Dafny, especially the results of verification
MIT License
3 stars 4 forks source link

Support file pattern argument #4

Closed robin-aws closed 2 years ago

robin-aws commented 2 years ago

The current version relies on pre-processing to collect the set of CSV files and provide them as individual arguments, but this might hit the maximum command length limit if there are a lot of them. I didn't want to take on the work of binding external utilities to search file systems in the initial version, but this could be a scalability issue in the near future. Perhaps dafny-lang/libraries will gain some I/O facilities soon. :)

seebees commented 2 years ago

I would vote that we make a separate library for I/O. But I guess that really depends on how we plan on managing packages...

robin-aws commented 2 years ago

Yup, I'm almost inclined to consider each individual file in dafny-lang/libraries as a separate "library", especially since customizing the verification to provide /noNLarith on a per-file basis is current necessary.

cpitclaudel commented 2 years ago

Could you just concatenate all the CSVs into one file and pass it to the report generator?

robin-aws commented 2 years ago

Could you just concatenate all the CSVs into one file and pass it to the report generator?

Almost, but each CSV file has a header row to label the fields, i.e. TestResult.DisplayName,TestResult.Outcome,....

I ended up keeping things simple by accepting directory paths as well and internally doing a **/TestResults/*.csv globbing search: #5 :)

cpitclaudel commented 2 years ago

I was thinking of something like this: find . -name '*.csv' -exec head -n 1 {} -quit \; ; find . -name *.csv -exec tail -q -n +2 {} +. An equivalent program in C# is good too!

robin-aws commented 2 years ago

Touché. :) But yeah, I'm happier with not depending on any shell functionality for maximum portability of the features this tool is trying to provide!