[isabelle-dev] Testing HOL/Import

[Makarius]

On Wed, 20 Jul 2011, Florian Haftmann wrote:

>> Cezary's major cleanup in 6ca79a354c51, so there is hope for 
>> improvements here.
>
> these are good news, thanks for the excellent work that is going on!

Indeed, 6ca79a354c51 looks like substantial progress in getting rid of 
very odd old code.  After a few more rounds of updating things the 
importer should be able to suck much larger HOL-Light sessions, maybe even 
the full Flyspeck material.


I have not run the regular "generate" process so far (which is hard to 
understand), but made some independent experiments with the proof files. 
Observations:

   * XML.parse vs. YXML.parse:
       . time factor 2..3 (Isabelle/94033767ef9b).
       . space factor 10% for uncompressed or compressed sources

   * Reading all 200000 files from an ext3 file-system is really slow
     (2..3 hours?).  Each file takes about 10..20ms.  There is also a waste
     of disk space since most files are much smaller than the block size.

   * The main proof_kernel.ML seems to assume sequential execution, due to
     strange global references.  There are also several "handle _ => ..."
     which make the meaning of the ML code erratic in the presence
     of environmental effects.

   * Sources are generally unreadable to to very long lines that do not fit
     on normal wide-screen displays with normal fonts.


One could probably speed up the import by a large factor as follows:

   * Exploit the inherent DAG structure of the collection of proofs,
     forking proofs according to static dependencies.  This should give a
     slightly larger speedup than the regular proof parallelization, which
     needs to track explicit proof promises due to unknown dependencies.

   * Direct streaming of source input via "bzip -dc", where each "file" is
     terminated by "\f".  See also File.fold_pages and
     Isabelle_System.bash_output_fifo.  (The latter does not work for
     Cygwin in Isabelle/521de6ab277a, but this can be ignored at the
     moment.)

This requires a slightly different presentation of the proofs, potentially 
with an additional phase after the HOL-Light export.  The result could be 
shipped to users as a compact / fast archive, as sketched above.


 	Makarius