[opentheory-users] article file size

Joe Hurd joe at gilith.com
Fri Sep 16 00:11:07 UTC 2011


Hi Ramana,

> I'm in the process of trying to compile a HOL4 script file of roughly
> 200 lines of ML (~7K) to an OpenTheory article, and though there are
> still some bugs in the translation process, it looks like the file
> will be at least 2.6M.

Article files can be large, and in addition to finding ways to
compress them there's an interesting question about which tactics
result in the most compressible files. For example, I might expect
that rewriting results in smaller articles than exhaustive
enumeration.

> Perhaps once I have a working article file and I run it through the
> opentheory tool it might shrink...

I report on the before and after sizes of your example article in this message:

http://www.gilith.com/opentheory/mailing-list/2011-September/000145.html

Cheers,

Joe



More information about the opentheory-users mailing list