定理证明器HOL的下载和安装

HOL下载安装

直接windows上安装：

1.源码下载：

该命令用于从GitHub获取HOL定理证明器仓库。

2.下载sml-system:

https://polyml.org/download.html

git clone https://github.com/polyml/polyml.git

    cd E://Modelchecking
    cd polyml
    ./configure

报错：

1. 缺少gcc编译器；
2. 缺少make；

原因：

Git-Bash 被归类为一个基于 mingw64 的环境；其默认 shell 设置为 bash；基本上与 Linux 的操作系统架构非常相似；然而它缺乏诸如 gcc 和 make 这样的构建工具套装。

总是报错Path路径下找不到c编译器；

• 确认了环境变量的设置情况；
  • 这样的路径同样是没有空格且非中文的；
  • 按照教程更换了下载的位置也未能如愿。

Windows 10 配置WSL（ubuntu18）

重新阅读HOL官方文档后了解到，在完全的Windows环境下无法直接运行Linux程序，默认情况下也不支持纯Windows操作系统作为运行时环境；因此建议按照以