[isabelle-dev] Testing HOL/Import

[Alexander Krauss]

Hi all,

with Cezary's guidance, I set up mira configurations for building the 
proofs bundle from the HOL Light repository and for running the 
HOL-Generate-HOLLight with that bundle, cf. 
http://isabelle.in.tum.de/reports/Isabelle/report/ed3813d5499d44f6be414a5f051e85f3 
for the first successful run. I experienced some fairly reproducible 
segmentation faults on some machines, but lxbroy5-9 seem to work. This 
is still prior to Cezary's major cleanup in 6ca79a354c51, so there is 
hope for improvements here.

Now my question is: What do we actually know when HOL-Generate-HOLLight 
completes without error? Should the generated file be compared with the 
version in the repository and should the test fail when they are not 
identical? Are there other things that should be checked?

Alex