Would it be possible to include HOL in the gentoo distribution? AFAIK(!) it depends only on mosml (which is already included). Reproducible: Always Steps to Reproduce: 1. 2. 3.
Please note that there is now version 5 of this out. I am attempting to write an ebuild but I am having some problems getting the dependencies working correctly. Additionally I think this should be assigned to maintainer wanted. Once I get the ebuild working, I'll submit it.
Latest release HOL4 (2009)
repository is now on github: https://github.com/HOL-Theorem-Prover/HOL