Hi, The kananaskis-11 release source tarball (hol-kananaskis-11.tar.gz) [1] downloadable from HOL’s official site [2] has at least one missing file: bin/hol.ML. As a result, even the building process succeeds, HOL cannot startup … I think everyone who is trying to build HOL from the source tarball will meet this issue.
P. S. In Git, the source code under 'kananaskis-11’ tag has no such issues. Regards, Chun [1] https://sourceforge.net/projects/hol/files/hol/kananaskis-11/hol-kananaskis-11.tar.gz/download [2] https://hol-theorem-prover.org/#get
signature.asc
Description: Message signed with OpenPGP using GPGMail
------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
