| home | project goals | article format | article examples |
Experimentation to date has been with the hol-light theorem prover. The 2Mb file num.art is an article of everything proved in the num.ml input file, and the 32Mb compressed tar file articles.tar.gz contains articles of all the .ml input files distributed with hol-light.
hol-light was naively instrumented to log every function call, whether successful or not, and also to insert every new object into the dictionary (in case it was needed in the future). Thus the article files are far larger than they need to be. There is ongoing work on tool support to eliminate this and other forms of redundancy in article files, but it is encouraging that even without this the sizes are not unmanageable. Here is a list of article sizes, in build order:
Lines Bytes Article
2 21 preamble.art
2 47 basics.art
2 45 nets.art
2 48 preterm.art
2 47 parser.art
2 48 printer.art
2 46 equal.art
31198 155087 bool.art
2 46 drule.art
3581 16958 tactics.art
6695 32958 itab.art
23615 116840 simp.art
942146 5053380 theorems.art
70333 364997 ind-defs.art
358090 1809609 class.art
48559 233449 trivia.art
143651 708440 canon.art
60590 293455 meson.art
651692 3359652 quot.art
2 50 recursion.art
678899 3472186 pair.art
483962 2477009 num.art
4650602 24860400 arith.art
3007805 15715077 wf.art
4717376 26001236 calc_num.art
682347 3524836 normalizer.art
1972070 10377762 ind-types.art
2890987 15344957 list.art
5829516 31346033 realax.art
9021585 49129317 real.art
348760 1763719 calc_rat.art
1769608 9136771 int.art
21833607 119181045 sets.art
------------------------------------
60227292 324475571 Total
The compression ratio for these article files is 90%. During the entire build of hol-light, 1,600,000 new types, terms and theorems were constructed, giving an average of 200 bytes per object, or 20 compressed bytes per object.