refactor: add line counting command for Verus source files

[Marsman1996]

No description provided.

[Marsman1996]

Since xinyi is busy writing paper, maybe you can try this to see whether count_line works for you.
@hiroki-chen

[rikosellic]

Is this based on the new line-count?

[Marsman1996]

Is this based on the new line-count?

It is based on the new version of line-count (exactly this one)

[rikosellic]

It works, but we may make the interaction nicer. I've run cargo dv verify --count-line, and the terminal output will print every line of the entire project, which is very noisy and flushes the verification result. Can we silence the line-level output and only reserve the file-level table at the end in this case?

If the line-level output is useful in some cases, we may add a cargo dv count function and add an option to decide whether the lines will be printed.

[Marsman1996]

It works, but we may make the interaction nicer. I've run cargo dv verify --count-line, and the terminal output will print every line of the entire project, which is very noisy and flushes the verification result. Can we silence the line-level output and only reserve the file-level table at the end in this case?

If the line-level output is useful in some cases, we may add a cargo dv count function and add an option to decide whether the lines will be printed.

It's because in the original version it adds the --print-all arg, and I keep it.
Just add an option for it will work.

[Marsman1996]

Actually for a large scale project like VOSTD, I do not think this --print-all option useful 🤔

[rikosellic]

Actually for a large scale project like VOSTD, I do not think this --print-all option useful 🤔

Indeed, we can delete this option.

[rikosellic]

Another question: cargo dv verify --targets ostd --count-line -- --verifyonly-module sync::rwlock will also count the whole project. It may be better to remove the count-line option in verify and add a dedicated cargo dv count so that we can handle the module counting properly there.

[Marsman1996]

cargo dv verify --targets ostd --count-line -- --verifyonly-module sync::rwlock will also count the whole project.

This is caused by line_count reads the generated .d dependency file, which includes the file information of the whole crate.

Maybe I shall use the folder scan feature added in the new count line for the folder I guess.

[Marsman1996]

@rikosellic Now it works

[rikosellic]

It works very well! Thanks!

[rikosellic]

Please also sync this in vostd.