[isabelle-dev] Testing HOL/Import

[Florian Haftmann]

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

Cheers,
	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

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