[opentheory-users] article file size

[Joe Hurd]

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