Check proof length as part of CI
Prosa has unfortunately accumulated a significant number of "long" proofs. Originally, we agreed to keep proofs down to 30-50 lines at most (and ideally shorter), as longer proofs tend to hide reusable helper lemmas and/or interesting intermediate steps that should be exposed at the spec level. Unfortunately, this rule was soon forgotten or ignored when inconvenient, since it was not frequently checked or strictly enforced.
To prevent the problem from getting bigger (i.e., to prevent further long proofs from slipping in), this merge request adds a script (scripts/proofloc.py) that automatically flags new proofs that are too long as part of the continuous integration setup. By default, "too long" means 40 lines. Given the current distribution of proof lengths (see below, obtained with scripts/proofloc.py -b 5), this seems like a reasonable cutoff (and it is squarely in the middle of the informal 30-50 LOC range, too). It bears repeating that this is intended as a maximum proof length; shorter proofs are of course always welcome. (It should also be noted that it is of course possible to squeeze any proof onto a single line; the idea here is that all contributors adhere to a reasonable coding style, so such extreme cases shouldn't be a problem in practice.)
To deal with existing long proofs, the script checks a database of "known long proofs" (scripts/known-long-proofs.json) before complaining about a proof exceeding 40 lines. The idea is that, over time, these legacy long proofs will go away as parts of the library are refactored and improved.
Finally, for the rare case where a new proof really needs to span more than 40 lines, it is possible to add manual exceptions to the long-proofs database.
Please holler if you see any problem with this, or if you think the cutoff should be something different from 40 LOC.
| LOC | #Proofs |
|---|---|
| <= 5 | 475 |
| <= 10 | 220 |
| <= 15 | 133 |
| <= 20 | 116 |
| <= 25 | 88 |
| <= 30 | 77 |
| <= 35 | 60 |
| <= 40 | 50 |
| <= 45 | 29 |
| <= 50 | 24 |
| <= 55 | 25 |
| <= 60 | 9 |
| <= 65 | 6 |
| <= 70 | 5 |
| <= 75 | 4 |
| <= 80 | 8 |
| <= 85 | 9 |
| <= 90 | 4 |
| <= 95 | 2 |
| <= 100 | 7 |
| <= 105 | 2 |
| <= 110 | 2 |
| <= 115 | 3 |
| <= 120 | 2 |
| <= 125 | 2 |
| <= 130 | 3 |
| <= 135 | 1 |
| <= 140 | 1 |
| <= 145 | 1 |
| <= 150 | 1 |
| <= 155 | 1 |
| <= 160 | 3 |
| <= 165 | 2 |
| <= 170 | 2 |
| <= 175 | 1 |