4、Python环境配置：Python3安装、pip包管理器、virtualenv虚拟环境、Jupyter Notebook搭建

说实话，做形式化验证这么多年，我见过太多工程师在环境配置上栽跟头。明明工具链都对了，结果Python版本不对，或者包冲突，一折腾就是半天。今天咱们就把这块彻底捋清楚。

我个人习惯用Python 3.8到3.11之间的版本。为什么？因为形式化验证工具（比如我们后面要用的PySMT、Z3）对太新的Python支持往往滞后。你装个3.12，可能某些库还没适配。

注意：千万别装Python 2.7了！2020年就停止维护了。我去年还碰到一个项目，脚本里混着Python 2和3的语法，排查起来简直噩梦。

Linux（Ubuntu/Debian）下安装：

sudo apt update
sudo apt install python3 python3-dev python3-pip
python3 --version   # 确认版本

Windows下安装：

去官网下载安装包，记得勾选「Add Python to PATH」。嗯，这一步很多人会忘，导致后面命令行找不到python命令。

macOS下安装：

brew install python3
python3 --version

装完之后，我建议你顺手验证一下：

which python3   # 看看路径对不对
python3 -c "import sys; print(sys.version)"

pip就是Python的包管理工具。说白了，你要装什么第三方库，喊它一声就行。

升级pip：

python3 -m pip install --upgrade pip

常用命令：

命令	作用
`pip install <包名>`	安装包
`pip install <包名>==版本号`	安装指定版本
`pip list`	查看已安装的包
`pip freeze > requirements.txt`	导出当前环境依赖
`pip install -r requirements.txt`	批量安装依赖

小技巧：我曾经在项目里用 pip freeze 导出依赖，结果发现同事的环境死活装不上。后来发现是版本号写死了。建议用 pip freeze | grep -v "@" 过滤掉一些奇怪的路径依赖。

你想想看，一个项目用Z3 4.8，另一个项目用Z3 4.12，装在一起肯定打架。virtualenv就是干这个的——给每个项目一个独立的Python环境。

安装virtualenv：

python3 -m pip install virtualenv

创建虚拟环境：

cd my_formal_verification_project
python3 -m virtualenv venv

激活虚拟环境：

激活后，命令行前面会出现 (venv) 字样。这时候你装任何包，都只影响这个环境。

避坑指南：我曾经在虚拟环境里装了一堆包，结果退出后忘了激活，又在全局环境里装了一遍。建议每次打开终端第一件事就是激活虚拟环境，养成肌肉记忆。

退出虚拟环境：

deactivate

做形式化验证时，我特别喜欢用Jupyter Notebook。为什么？因为你可以一段一段地跑代码，随时看中间结果。调试SMT公式的时候，这比写脚本再执行爽多了。

安装Jupyter：

pip install jupyter

启动Notebook：

jupyter notebook

浏览器会自动打开 http://localhost:8888。点右上角的「New」→「Python 3」，就能新建一个Notebook了。

安装内核（可选）：

如果你想让Jupyter识别你的虚拟环境：

pip install ipykernel
python3 -m ipykernel install --user --name=venv --display-name "Python (venv)"

这样在Jupyter里切换内核时，就能选到你的虚拟环境了。

个人经验：我习惯在Notebook里先写一段SMT公式，跑一下看看SAT/UNSAT结果。如果不对，直接改公式再跑，不用重新加载整个脚本。这种交互式调试，效率至少提升30%。

下面这张图，是我自己总结的Python环境配置核心逻辑。你照着这个思路走，基本不会乱。

说白了，这四层是一环扣一环的。先有Python，然后用pip装包，再用virtualenv隔离环境，最后用Jupyter做交互式开发。每一步都踩实了，后面做形式化验证才能顺手。

  总结一下：
  Python版本选3.8~3.11，别追新
pip升级到最新，用 freeze 管理依赖
每个项目建一个虚拟环境，别偷懒
Jupyter Notebook做交互式调试，效率翻倍

好了，环境搭好了，下一节咱们就开始装形式化验证的核心工具链。到时候你会感谢今天把Python环境理清楚的自己。