[mizar] Mizar to LaTeX automatic translation

[marco caminati <spam.caminati@gmail.com>]

I tried taking advantage of Grzegorz Bancerek's .miz to .tex renderer:

http://fm.uwb.edu.pl/proof-read/

It would be handy to use it instead of having to manually handcraft
into LaTeX the (many) parts of my Mizar articles I'd like to include
in my thesis.

However, it seems not like a speed-o-matic task, after reading
Bancerek's 2006 paper illustrating his system, and issues 1(1) and
1(4) of Formalized Mathematics.

In fact, my attempts with the above online engine failed miserably,
I'm not reporting the error logs because I think the problem is me :)

My question:

-given my hastiness (at the moment I have little time to dedicate to a
further todo on my list), would you advice me to LaTeX by hand or to
try and exploit this nice engine?

Questions of independent interest:

-is this system conceived for the casual Mizar user or specifically
for the editing needs of "Formalized Mathematics" journal?

-And in the former case, is there a tutorial for hasty dummies?

-Is a local installation of the system available in order to fiddle with it?
I mean, an installation containing the accom, fmparse, newfmrm,
jformat, and the like utilities mentioned in the aforementioned paper.
It would be more instructive than having to resort to online engine, I think.

Best regards,
Marco Caminati.

PS: I couldn't find helpful information online about this. Apologizes
if this has already been discussed.