Preprocessor uses a _lot_ of memory (and consequently of GC time)

[shym]

To test the performance of gospel pps, I’ve generated .mli files by concatenating copies of test/vocal/Vector.mli in a format:

module Block0 = sig
(* copy of Vector.mli *)
end
module Block1 = sig
...

Results:

• 16 copies (~235KB .mli file):

  allocated_words: 439664837
  real       0m1.798s

  with 439664837 = 27479052 × 16

• 32 copies (~471KB .mli file):

  allocated_words: 1748175205
  real       0m11.291s

  with 1748175205 = 54630475 × 32

• 48 copies (~700KB .mli file):

  allocated_words: 3766420005
  real       0m23.129s

  with 3766420005 = 78467083 × 48

(So note that the allocated_words and time are not linear)

[shym]

353 might be enough to fix this, even though it still loads the whole source into memory. Otherwise we should go into a fully streaming preprocessor.