在Ubuntu 22.04.1 安装acl2(“A Computational Logic for Applicative Common Lisp".)
安装环境如下所示:
Linux ubun 6.8.0-47-generic #47~22.04.1-Ubuntu SMP PREEMPT_DYNAMIC Wed Oct 2 16:16:55 UTC 2 x86_64 x86_64 x86_64 GNU/Linux
ACL2官网:https://www.cs.utexas.edu/~moore/acl2/v8-6/combined-manual/index.html?topic=ACL2____TOP
官方安装网址:https://www.cs.utexas.edu/~moore/acl2/v8-6/HTML/installation/installation.html
ACL2的releases网址:https://github.com/acl2-devel/acl2-devel/releases/
ACL2的安装方式有多种,本文只记录通过编译源码的方式安装。
一、获取ACL2源码
1. 从release网址中下载tar压缩包
tar -xfz acl2-8.6.tar.gz
2. 使用git从github获取源码
git clone https://github.com/acl2/acl2
二、安装lisp
可以从ACL2可支持的lisp中选择一个下载安装https://www.cs.utexas.edu/~moore/acl2/v8-6/HTML/installation/requirements.html
官网支持六种lisp,并且给出了下载链接和安装方法,有的试用版本和需要付费的。这里作者尝试用SBCL、clisp和gcl,只有gcl成功完成了acl2的编译。这里讲一下为什么尝试这三种方式,也讲一下踩过的坑。
一开始使用apt命令下载的sbcl和clisp用来编译acl2,但是会报错,寻找报错原因sbcl是因为版本太低,clisp忘记什么错误了。后面就升级sbcl,作者是下载sbcl的源码编译,但需要lisp编译器,使用apt下载的sbcl编译,但也会报错。在sbcl的官网找了下,看到
在linux的x86架构上本就不支持太高版本的sbcl后,就放弃使用sbcl编译acl2。
在放弃sbcl和clisp后,选择使用gcl,因为其他版本感觉更麻烦些,gcl最好选择acl2光放推荐的版本2_6_13。作者一开始没有切换到这个版本选择的是最新版本,使用gcl编译acl2源码总是会报错,后面将版本降低后就编译成功。
源码编译
1. 进入 acl2-8.6 目录执行make命令,需要指定选择的lisp,这个过程时间可能会长一些。如果报错,错误详细信息可以在make.log文件中查看。
make LISP=<path_to_your_lisp_executable>
安装成功界面如下所示:
在当前目录下就可以看到可执行文件 saved_acl2
2. 安装基础books
在acl2目录下执行命令
make basic
安装完之后就可以使用acl2了
标签:定理,ACL2,编译,acl2,源码,安装,sbcl From: https://www.cnblogs.com/d1s2y3/p/18516542