Hi 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.
Now my question is: What do we actually know when HOL-Generate-HOLLight
completes without error? Should the generated file be compared with the
version in the repository and should the test fail when they are not
identical? Are there other things that should be checked?
Alex
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
