首页 > 其他分享 >ACL2 定理证明器的安装

ACL2 定理证明器的安装

时间:2024-10-31 10:50:26浏览次数:1  
标签:定理 ACL2 编译 acl2 源码 安装 sbcl

在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

相关文章

  • windows上安装nvm-noinstall.zip
    在windows上安装nvm-noinstall.zip步骤:1、解压nvm-noinstall.zip并创建node_global和node_cache目录2、修改install.cmd3、配置环境变量4、以管理员身份运行install.cmdsettings.txtroot:D:\Develop\nvmpath:D:\Develop\nodejsarch:64proxy:none......
  • docker容器安装nacos详解
    ‌Nacos的核心功能‌Nacos是一个动态服务发现、配置管理和服务管理平台,旨在帮助构建云原生应用。它支持服务注册与发现、配置管理、‌服务健康监测等功能,适用于微服务和云原生架构。Nacos提供了友好的‌Web界面和‌API接口,方便用户进行配置管理、服务注册和发现等操作。1.打......
  • Delphi10.3下SimpleGraph v2.92的安装,使用
     下载 通过百度网盘分享的文件:simple-graph-master.zip链接:https://pan.baidu.com/s/19KHlGaitim21qcgXHl_HgQ提取码:n3zq安装将C:\Users\Administrator\Downloads\simple-graph-master\simple-graph-master\Source加入到第一步:点击“File”-“New”菜单中的“Packag......
  • 计量经济学(十五)的理论基础——时间序列分解定理
    时间序列分析是数据科学中的一个重要分支,旨在探索和理解随着时间变化的数据背后的模式和结构。无论是在金融市场预测、经济政策分析、环境监测还是医学研究中,时间序列数据的广泛应用证明了其在预测未来趋势、制定决策和风险管理方面的重要性。然而,时间序列数据的复杂性和多样性使......
  • ubuntu-安装docker、中间件
    1、基本命令#查看ubuntu版本lsb_release-a#修改密码sudopasswdubuntu#修改远程端口vim/etc/ssh/sshd_configsudoservicesshrestart#基础软件安装sudoaptinstalliputils-ping-ysudoaptinstallnet-tools-ysudoaptinstallvim-ysudoaptinstallufw-y 2、......
  • 《诛仙单机版系列一:六道轮回》安装教程|虚拟机一键端|GM工具包
    今天给大家带来一款单机游戏的架设:诛仙-六道轮回-五职业。游戏版本:v1.2.4只适用于单机娱乐,此教程是本人亲测所写,踩坑无数,如果你是小白跟着教程走也是可以搭建成功。  亲测视频演示https://githubs.xyz/show/289.mp4 游戏安装步骤此游戏架设需要安装虚拟机,没有虚拟机......
  • 【服务器虚拟化详细安装教程(亲测有效)】
    服务器虚拟化是一种技术,它允许在一台物理服务器上创建多个独立的虚拟环境,每个环境都拥有自己的操作系统和应用程序。这项技术通过软件模拟硬件的功能,将单一的物理服务器资源(如CPU、内存、存储和网络带宽)分割成多个虚拟机(VMs),每个虚拟机都可以独立运行不同的操作系统和应用,就......
  • AI Illustrator矢量图形设计软件下载安装
    一、软件简介1.1基本信息AdobeIllustrator,简称AI,是Adobe系统公司推出的一款专业矢量图形设计软件。自1987年首次发布以来,它已成为出版、多媒体和在线图像领域的行业标准之一。AI广泛应用于印刷出版、海报书籍排版、专业插画、多媒体图像处理和互联网页面制作等领域,为设计师......
  • Linux安装Tomcat
    Linux安装Tomcat下载Tomcat打开浏览器,进入Tomcat官网选择要下载的Tomcat版本,下载.tar.gz安装Tomcat将下载的.tar.gz上传至linux服务器,并进行解压tarxzfapache-tomcat-9.0.XX.tar.gz-C/opt/tomcat配置环境变量编辑环境变量文件:vim/etc/profile在文件末尾添加以下......
  • WRF安装和运行教程
    1、WRF安装1.1校验和安装基础包校验指令:whichgfortranwhichcppwhichgcc安装指令:sudoapt-getupdatesudoapt-getinstallgfortrancppgccg++m4cshlibcurl4-openssl-devlibxml2libxml2-devlibhdf5-dev1.2WRF安装的目录结构创建目录mkdirBuild_WRF......