[isabelle-dev] Testing HOL/Import

[Lukas Bulwahn]

On 07/20/2011 09:34 PM, Florian Haftmann wrote:
> 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?
>
As we discussed at lunch in Munich, we have an expert on HOL4, Thomas 
Tuerk, who might take that opportunity.

Lukas

> Cheers,
> 	Florian
>
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20110720/4f58b914/attachment-0002.html>