[isabelle-dev] Testing HOL/Import
florian.haftmann at informatik.tu-muenchen.de
Wed Jul 20 21:34:54 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.
these are good news, thanks for the excellent work that is going on!
A humble question: is there any chance that also the HOL4 import can be
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 262 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev