termux安装HOL

缘起

HOL早有耳闻，觉得应该很难安装，就一直没有尝试安装，也没有尝试了解。

看到rust微信群里面有人讨论sel4于是就顺手翻了翻代码。

然后就顺手安装了一下其中的依赖软件，还真的安装上了一个polyml。

polyml

于是就尝试用polyml编译HOL，可编译到mlyacc的时候就出错，单独运行mllex会出现段错误，应该是polyml不过关导致的。

mosml

翻翻HOL的INSTALL，发现还能用mosml，于是下载，编译，还真的编译成功了（期间也曾想编译polyml，但是没有成功）。

尝试用mosml编译HOL，结果第一步就出错，出错的原因是不能使用/tmp目录，解决的方法是tmpname变成tempname就行了。

接下来就是漫长的编译过程了，编译了整整一天终于编译完了。

小结

没有想过尝试HOL的另一个原因是：一直想用coq来着。

总结一句话：不能给自己设限。