[opentheory-users] article file size

[Ramana Kumar]

I'm curious about others' experience with article files.
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.
Of course I was expecting lots of primitive inferences to be required,
but I don't have much better quantitative sense that that.
So does it sound like the right order of magnitude? Or is that
surprisingly small or large?
It seems large to me.
Perhaps once I have a working article file and I run it through the
opentheory tool it might shrink...