sel4验证环境搭建疑问：‘link isabelle path to verification directory’是什么意思？

语句含义 #

这句话的核心是给Isabelle的安装路径创建一个指向seL4验证目录的符号链接——本质是让seL4的验证脚本能快速定位到Isabelle工具链，完全不需要把Isabelle的文件实际移动或复制到验证目录里。

seL4的验证流程依赖Isabelle/HOL定理证明器，但验证脚本不会自动遍历系统查找Isabelle的安装位置，所以通过建立软链接，给脚本一个固定的、预期的路径来调用Isabelle的执行文件和库文件。

是否需要将Isabelle下载至验证目录？ #

不需要。你可以把Isabelle安装在系统任意位置（比如/opt/isabelle或者用户主目录下的~/isabelle-2023），之后在seL4的验证目录下执行符号链接命令即可，示例：

ln -s /你的/isabelle实际安装路径 ./isabelle

这里的./isabelle是验证脚本默认会查找的位置，软链接会直接指向你实际安装的Isabelle目录，既节省磁盘空间，后续升级Isabelle也只需要替换实际安装目录，不用改动验证环境的配置。

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