MacBookPro19 Mojave10.14.6安装K framework反复失败问题求助

问题根因 #

K framework的brew安装脚本运行时使用独立的非登录shell环境，不会加载用户目录下shell配置文件（.zshrc/.bash_profile等）中自定义的PATH变量，因此即使当前终端可正常调用z3，安装校验阶段仍然会找不到z3可执行文件。 #

修复步骤 #

方案一：统一使用brew管理z3版本（推荐） #

• 彻底清理手动安装的z3版本：删除~/z3-4.8.7-x64-osx-10.14.6目录，同时删除所有shell配置文件中手动添加的z3相关PATH配置
• 执行以下命令安装brew版z3：
  brew install z3
• 重载shell配置后验证z3路径：
  • zsh用户执行：source ~/.zshrc
  • bash用户执行：source ~/.bash_profile
  • 执行which z3确认返回路径为/usr/local/bin/z3（Intel芯片）或/opt/homebrew/bin/z3（M系列芯片），z3 -version返回正常版本号
• 重新安装kframework：
  PATH="$(brew --prefix)/bin:$PATH" brew install kframework

方案二：手动指定z3路径（仅方案一失效时使用） #

如果必须使用手动下载的z3二进制包，执行安装命令时直接指定z3的绝对路径前缀，替换命令中的用户名后执行即可：
PATH="/Users/你的用户名/z3-4.8.7-x64-osx-10.14.6/bin:$(brew --prefix)/bin:$PATH" brew install kframework #

安装验证 #

安装完成后新开终端，执行kompile --version，返回正常版本信息即为安装成功。

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