With the new optimizations, we extracted about 30K "repairs" to different types of Coq commands including theorems/proofs in less than a day. We still need to filter them based on tags to get an estimate of the number of proof repairs, and spot-checking a random sample would be wise to look for any signs of unexpected or erroneous data.
In the process, we discovered another batch of errors indicating some uncovered edge cases (captured in the attached file). We have not had the chance to go through these yet, but a couple look familiar to the last batch.
repair_mining_errors.xlsx
With the new optimizations, we extracted about 30K "repairs" to different types of Coq commands including theorems/proofs in less than a day. We still need to filter them based on tags to get an estimate of the number of proof repairs, and spot-checking a random sample would be wise to look for any signs of unexpected or erroneous data.
In the process, we discovered another batch of errors indicating some uncovered edge cases (captured in the attached file). We have not had the chance to go through these yet, but a couple look familiar to the last batch. repair_mining_errors.xlsx