Thank you for the bug report! I will upload a corrected tarball shortly.
Michael On 2/5/17, 16:11, "Chun Tian (binghe)" <binghe.l...@gmail.com> wrote: 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 ------------------------------------------------------------------------------ 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