@@ -25,7 +25,7 @@ and [SerAPI 0.7.1][serapi-071], via the SerAPI programs `sercomp`, `sertok`, and
2525The latest release of the corpus, based on MathComp 1.9.0, consists of 449
2626source files from 21 Coq projects --- in total over 297k lines of code (LOC).
2727A [ research paper] [ arxiv-paper ] describes the corpus in more detail
28- and provides additional statistics. The corpus is divided into tiers based
28+ and provides additional statistics. The corpus is divided into three tiers based
2929on how well projects conform to the [ MathComp conventions] [ math-comp-contrib ] .
3030
3131| Project | Revision SHA | No. files | LOC | Tier | License |
@@ -38,6 +38,7 @@ on how well projects conform to the [MathComp conventions][math-comp-contrib].
3838| [ bigenough] [ bigenough ] | 5f79a32 | 1 | 78 | 2 | [ CECILL-B] [ cecill-b ] |
3939| [ elliptic-curves] [ elliptic-curves ] | 631af89 | 18 | 9596 | 2 | [ CECILL-B] [ cecill-b ] |
4040| [ grobner] [ grobner ] | dfa54f9 | 1 | 1330 | 2 | [ CECILL-B] [ cecill-b ] |
41+ | [ infotheo] [ infotheo ] | 6c17242 | 81 | 42295 | 2 | [ GPL-3.0-only] [ gpl3 ] |
4142| [ multinomials] [ multinomials ] | 691d795 | 5 | 7363 | 2 | [ CECILL-B] [ cecill-b ] |
4243| [ real-closed] [ real-closed ] | 495a1fa | 10 | 8925 | 2 | [ CECILL-B] [ cecill-b ] |
4344| [ robot] [ robot ] | b341ad1 | 13 | 11130 | 2 | [ LGPL-3.0-only] [ lgpl3 ] |
@@ -50,7 +51,6 @@ on how well projects conform to the [MathComp conventions][math-comp-contrib].
5051| [ monae] [ monae ] | 9d0e461 | 18 | 6655 | 3 | [ GPL-3.0-only] [ gpl3 ] |
5152| [ reglang] [ reglang ] | da333e0 | 12 | 3033 | 3 | [ CECILL-B] [ cecill-b ] |
5253| [ toychain] [ toychain ] | 97bd697 | 14 | 5275 | 3 | [ BSD-2-Clause] [ bsd2 ] |
53- | [ infotheo] [ infotheo ] | 6c17242 | 81 | 42295 | LO | [ GPL-3.0-only] [ gpl3 ] |
5454
5555The structure of the corpus is as follows:
5656
0 commit comments