All this got me to thinking: how did Russel and Whitehead originally compose PM, and how was it typeset? They obviously didn't use TeX. Whatever they did, it must have been a truly staggering amount of work.
For that matter, what is the source material for PM-RW and how is it being processed? Is there a manual translation process from a printed copy of PM, or are they using OCR?