[isabelle-dev] Testing HOL/Import
makarius at sketis.net
Sun Jul 24 00:29:14 CEST 2011
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.
* 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
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.
More information about the isabelle-dev