[isabelle-dev] Testing HOL/Import
krauss at in.tum.de
Wed Jul 20 11:33:06 CEST 2011
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