HOL下载安装

直接windows上安装：

1.源码下载：

git clone（使用git工具下载）：
git clone https://github.com/HOL-Theorem-Prover/HOL.git

2.下载sml-system:

https://polyml.org/download.html

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

cd E://Modelchecking
cd polyml
./configure

报错：

缺少gcc编译器；
缺少make；

原因：

git-bash是一个mingw64环境，shell为bash，基本就和linux一样了，但它没有携带gcc和make等程序。

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

重新检查并配置了环境变量；
路径也是无空格非中文路径；
按照网上教程更换下载的gcc文件夹，也没有成功。

Windows 10 配置WSL（ubuntu18）

重新阅读HOL官网文档，得知不支持纯粹的windows环境，需要再装一个WSL环境（i.e. windows subsystems of linux)
查阅Microsoft windows 上WSL的安装教程，安装好Linux环境。

ubuntu 账户：kaixuan
ubuntu 密码：lab

Tips:

WSL下访问windows文件夹，可使用：
cd /mnt
如果要在 Windows 访问 wsl 的文件，则在 wsl 中输入：
explorer.exe .

原因：

启用 WSL 并安装 Linux 分发版时，将安装与 Windows NTFS C： \ 分隔的新文件系统。驱动器。在 Linux 中，不会为驱动器提供字母。为它们提供装入点。文件系统的根目录是根分区或文件夹的装入点（对于 / WSL）。不是下的所有 / 内容都是同一驱动器。例如，在笔记本电脑上，我安装了两个版本的 Ubuntu (20.04 和 18.04) 以及 Debian。如果我打开这些分发，使用命令选择主目录，然后输入命令，Windows 文件资源管理器将打开，并向我显示该分发的 cd ~ explorer.exe . 目录路径。

GIT 可以安装在 WINDOWS 上，也可以安装在 WSL 上。但是两者无法共用。

Linux 发行版	用于访问主文件夹的 Windows 路径
Ubuntu 20.04	\\wsl$\Ubuntu-20.04\home\username
Ubuntu 18.04	\\wsl$\Ubuntu-18.04\home\username
Debian	\\wsl$\Debian\home\username
Windows PowerShell	C:\Users\username

如果正在寻求从 WSL 分发命令行（而不是）访问 Windows 文件目录，则使用访问目录，因为 Linux 分发版将 Windows 文件系统视为已装载的 C:\Users\username /mnt/c/Users/username 驱动器。
[外链图片转存失败,源站可能有防盗链机制,建议将图片保存下来直接上传(img-yYr5g385-1630589144728)(./WSL_Windows.png)]

1. 配置gcc、make:

sudo apt update
sudo apt install build-essential

可使用 gcc -v 和make -v命令显示其版本，检验是否安装成功；

2.安装git：

sudo apt-get install git

3.git clone polyml:

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

4.编译、make与安装

./configure
make
make install

官方文档需要注意的地方：

GIT Source.

The released version has been extensively tested before being released. If you are using Poly/ML for real work this is the version you should use. The development version is kept in a GIT repository at GitHub (https://github.com/polyml). Note that the GIT code may change frequently and things may break. Bug fixes, though, are applied first to this so you may wish to try this if you have problems. To download the GIT version do the following:

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

At this stage you can simply build Poly/ML in the normal way but this may not incorporate all the changes. In particular the compiler is not rebuilt by the normal build process so to do a complete recompile do the following:

./configure
make
make compiler
make install

When updating an existing directory from GIT it may well be worth running make distclean before the update to remove any old files.

The GIT repository contains the main development line but also bug fixes for released versions. These are branches such as fixes-5.8.

安装过程出错记录：

make install 报错提示：

kaixuan@DESKTOP-MHHIDIM:~/polyml$ make install
Making install in libpolyml
make[1]: Entering directory '/home/kaixuan/polyml/libpolyml'
make[2]: Entering directory '/home/kaixuan/polyml/libpolyml'/bin/mkdir -p '/kaixuan/lib'/bin/bash ../libtool   --mode=install /usr/bin/install -c   libpolyml.la '/kaixuan/lib'
libtool: install: /usr/bin/install -c .libs/libpolyml.so.12.0.0 /kaixuan/lib/libpolyml.so.12.0.0
/usr/bin/install: cannot remove '/kaixuan/lib/libpolyml.so.12.0.0': Permission denied
Makefile:616: recipe for target 'install-libLTLIBRARIES' failed
make[2]: *** [install-libLTLIBRARIES] Error 1
make[2]: Leaving directory '/home/kaixuan/polyml/libpolyml'
Makefile:892: recipe for target 'install-am' failed
make[1]: *** [install-am] Error 2
make[1]: Leaving directory '/home/kaixuan/polyml/libpolyml'
Makefile:708: recipe for target 'install-recursive' failed
make: *** [install-recursive] Error 1
kaixuan@DESKTOP-MHHIDIM:~/polyml$ sudo make install
[sudo] password for kaixuan:
Making install in libpolyml
make[1]: Entering directory '/home/kaixuan/polyml/libpolyml'
make[2]: Entering directory '/home/kaixuan/polyml/libpolyml'/bin/mkdir -p '/kaixuan/lib'/bin/bash ../libtool   --mode=install /usr/bin/install -c   libpolyml.la '/kaixuan/lib'
libtool: install: /usr/bin/install -c .libs/libpolyml.so.12.0.0 /kaixuan/lib/libpolyml.so.12.0.0
libtool: install: (cd /kaixuan/lib && { ln -s -f libpolyml.so.12.0.0 libpolyml.so.12 || { rm -f libpolyml.so.12 && ln -s libpolyml.so.12.0.0 libpolyml.so.12; }; })
libtool: install: (cd /kaixuan/lib && { ln -s -f libpolyml.so.12.0.0 libpolyml.so || { rm -f libpolyml.so && ln -s libpolyml.so.12.0.0 libpolyml.so; }; })
libtool: install: /usr/bin/install -c .libs/libpolyml.lai /kaixuan/lib/libpolyml.la
libtool: install: /usr/bin/install -c .libs/libpolyml.a /kaixuan/lib/libpolyml.a
libtool: install: chmod 644 /kaixuan/lib/libpolyml.a
libtool: install: ranlib /kaixuan/lib/libpolyml.a
libtool: finish: PATH="/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin:/snap/bin:/sbin" ldconfig -n /kaixuan/lib
----------------------------------------------------------------------Libraries have been installed in:/kaixuan/libIf you ever happen to want to link against installed libraries
in a given directory, LIBDIR, you must either use libtool, and
specify the full pathname of the library, or use the '-LLIBDIR'
flag during linking and do at least one of the following:- add LIBDIR to the 'LD_LIBRARY_PATH' environment variableduring execution- add LIBDIR to the 'LD_RUN_PATH' environment variableduring linking- use the '-Wl,-rpath -Wl,LIBDIR' linker flag- have your system administrator add LIBDIR to '/etc/ld.so.conf'See any operating system documentation about shared libraries for
more information, such as the ld(1) and ld.so(8) manual pages.-------------------------------------#### 运行poly报错信息：
kaixuan@DESKTOP-MHHIDIM:~/polyml$ poly
poly: error while loading shared libraries: libpolyml.so.12: cannot open shared object file: No such file or directory

解决的灵感来源：

查看两目录下文件

新建用户文件夹下文件：

kaixuan@DESKTOP-MHHIDIM:/usr/local/lib$ ls
libpolymain.a  libpolymain.la  libpolyml.a  libpolyml.la  libpolyml.so  libpolyml.so.12  libpolyml.so.12.0.0  pkgconfig  polyml  python3.6

共享文件夹下：

kaixuan@DESKTOP-MHHIDIM:/kaixuan/lib$ ls
libpolymain.a  libpolymain.la  libpolyml.a  libpolyml.la  libpolyml.so  libpolyml.so.12  libpolyml.so.12.0.0  pkgconfig  polyml

解决：
删除共享文件夹下的编译文件；

小报错的解决：
文件的访问权限不够，需要先给权限再操作；
或者直接使用 sudo ;

报错如下：

kaixuan@DESKTOP-MHHIDIM:~/polyml$ make install
Making install in libpolyml
make[1]: Entering directory '/home/kaixuan/polyml/libpolyml'
make[2]: Entering directory '/home/kaixuan/polyml/libpolyml'/bin/mkdir -p '/kaixuan/lib'/bin/bash ../libtool   --mode=install /usr/bin/install -c   libpolyml.la '/kaixuan/lib'
libtool: install: /usr/bin/install -c .libs/libpolyml.so.12.0.0 /kaixuan/lib/libpolyml.so.12.0.0
/usr/bin/install: cannot remove '/kaixuan/lib/libpolyml.so.12.0.0': Permission denied
Makefile:616: recipe for target 'install-libLTLIBRARIES' failed
make[2]: *** [install-libLTLIBRARIES] Error 1
make[2]: Leaving directory '/home/kaixuan/polyml/libpolyml'
Makefile:892: recipe for target 'install-am' failed
make[1]: *** [install-am] Error 2
make[1]: Leaving directory '/home/kaixuan/polyml/libpolyml'
Makefile:708: recipe for target 'install-recursive' failed
make: *** [install-recursive] Error 1

定理证明器HOL的下载和安装相关推荐

MySQL下载与安装教程以及环境变量配置
MySQL下载 1 搜索mysql 选择mysql downloads 如下 2 点击滑动到底部选择社区版本(免费) 如下 3 选择Community Server 如下 4 选择对应的版本下载我选 ...
java jdk 1.8 安装_下载、安装、配置 java jdk1.8
近期配置react native的开发环境,所以就从配置环境开始.rn的环境配置有那么几项,其中重要的一个就是java jdk(Java Development Kit 的缩写),那么以下就是下载.安 ...
vs安装一直在提取文件_Visual Studio 2019下载及安装教程
宸1分钟前这可是我珍藏多年的资源啊. Visual Studio 2019 Microsoft Visual Studio(简称VS)是美国微软公司的开发工具包系列产品.是目前最流行的Windows ...
python安装包_迈出Python学习第一步：Python开发环境的下载与安装
所谓"磨刀不误砍柴工"."工欲善其事,必先利其器",都在告诉我们一个道理:要做好一个事情,事先做好充分的准备工作是非常重要的.所以在我们正式学习用Python编 ...
oracle怎么下载安装,Oracle数据库的下载和安装方法
一.Oracle数据的下载与安装: 我这里是Oracle Database 11g Release 2版本的. 1.百度云链接: 链接:https://pan.baidu.com/s/1QYvBVS3 ...
我的世界php安装,我的世界Linux搭建网页后台Multicraft下载与安装
小编为大家带来了<我的世界>Linux搭建网页后台Multicraft下载与安装,首先下载Multicraft Linux版,下载好了以后请玩家自己看着下面的教程来安装. 64位:http ...
Editplus下载、安装并最佳配色方案（强烈推荐）
不多说,直接上干货! Editplus下载第一步:进入官网 https://www.editplus.com/ 第二步:下载 https://www.editplus.com/download.ht ...
docker基础文档(链接，下载，安装)
一.docker相关链接 1.docker中国区官网(包含部分中文文档,下载安装包,镜像加速器):https://www.docker-cn.com/ 2.docker官方镜像仓库:https://c ...
下载、安装、配置 java jdk1.8
近期配置react native的开发环境,所以就从配置环境开始.rn的环境配置有那么几项,其中重要的一个就是java jdk(Java Development Kit 的缩写),那么以下就是下载.安 ...
transmission Linux（debian）下的BT下载客户端安装
transmission Linux(debian)下的BT下载客户端安装转载于:https://blog.51cto.com/2042617/1597540

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