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
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
