Intel macOS下TPS定理证明系统安装运行故障求助

一、优先方案：切换到SBCL运行（官方适配性更好） #

TPS对Steel Bank Common Lisp（SBCL）的兼容性优于CLISP，在macOS Intel架构上更稳定，操作步骤：

• 安装SBCL：通过Homebrew执行brew install sbcl
• 进入TPS目录，编辑Makefile，将lisp = lisp替换为lisp = sbcl
• 执行编译命令：make tps（忽略过程中的弃用警告即可）
• 启动TPS：运行sbcl --load tps3.init

二、CLISP环境修复方案（若需保留CLISP） #

如果必须使用CLISP，需手动解决符号冲突并调整内存配置：

1. 编辑TPS目录下的tps3.ini文件，找到(use-package :teacher)这一行
2. 将其替换为以下代码，手动处理GETDATE符号冲突：

(shadowing-import '(teacher:getdate) common-lisp-user)
(use-package :teacher)

3. 重新编译TPS：执行make tps
4. 启动时添加内存限制参数，避免段错误：clisp -M tps3.mem -m 256MB

故障原因说明 #

• 符号冲突：GETDATE符号同时存在于COMMON-LISP-USER包和TPS的TEACHER包中，CLISP无法自动解决包导入时的符号歧义，导致启动中断
• 段错误：CLISP的内存镜像加载逻辑在macOS Intel架构下存在兼容性问题，调整内存参数或换用更适配的SBCL可规避该问题

内容的提问来源于stack exchange，提问作者Lime