[isabelle-dev] Testing HOL/Import

Alexander Krauss krauss at in.tum.de
Wed Jul 20 11:33:06 CEST 2011

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. 
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?


More information about the isabelle-dev mailing list