[isabelle-dev] Testing HOL/Import

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Wed Jul 20 21:34:54 CEST 2011

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

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




PGP available:

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20110720/0afe49c4/attachment.sig>

More information about the isabelle-dev mailing list