coqwc

Friday we needed to measure our Coq development for the PLDI submission. Normally, I just use wc to roughly estimate program size, and

  $ grep ";\|}" FOO | wc

for a more accurate account (of C/Java code FOO). However, in Coq code one is usually interested in knowing both the amount of code you've written AND the size of the proofs about your code. Obviously, wc can't tell the difference, and so I was reduced to hacking out some grep/sed/awk monstrosity that roughly estimates the number of lines in each category.

Then today (too late) I find coqwc which does exactly what I want:

$ coqwc PRTL.v EE.v SideCond_DNM.v 
     spec    proof comments
      279        0       19 PRTL.v
      266      163       84 EE.v
       81       42       18 SideCond_DNM.v
      626      205      121 total