Isabelle上安装c-parser和autocorres

c-parser，autocorres都是在Isabelle上形式验证c代码的工具，它们都是seL4项目的一部分，而这些所有的工具都是主要基于Linux的，所以建议在Linux上安装，以下内容是在WSL上安装的过程。

进行安装前必要的步骤：

• 支持WSL图形化的Windows系统，我个人用的是win10专业版，没有这个就别往下看了，别的系统我都没测试过
• 开启WSL图形化，具体工作可以参考微软官方文档，我的经验是，只要能打开Nautilus就说明WSL GUI是正常的。

安装Isabelle

根据官网要求，下载安装包，解压后，就可以使用Isabelle了。个人使用的是Isabelle2023，建议使用相同的版本。
首先测试一下Isabelle2023能否正常运行，直接在命令行里运行Isabelle2023（应用程序就叫这个名字）

./Isabelle2023/Isabelle2023

如果能够正常显示Isabelle的JEditor，说明安装正确。
确定安装正确后，将Isabelle命令行工具加入环境变量方便使用，命令行工具所在的路径为Isabelle2023/bin/
加入环境变量后可以测试一下，如果能够直接从命令行调用isabelle命令，那么就说明成功了。

安装证明环境

首先从github上clone seL4有关证明的项目到本地

git clone https://github.com/seL4/l4v.git

我们来看一下项目的目录格式，这里只列出我们需要关心的文件夹

l4v-+
    |-isabelle 这是一个软连接，请调整这个软链接使它指向你自己的Isabelle文件夹根目录
    |-tools--+
             |-c-parser
             |-autocorres

里面已经包含了autocorres和c-parser

安装c-parser

安装c-parser之前需要先安装MLton，这个直接参照MLton官网下载链接的安装要求应该就可以。
首先来到c-parser文件夹下面，我们按照文件夹中的INSTALL文件的指令运行如下命令

export L4V_ARCH=X64 #我第一次用ARM似乎也成功了，不知道为啥，明明我电脑是X64的，总之你们多试试
isabelle env make CParser

如果没有产生错误，那么c-parser的安装就完成了

安装autocorres

在l4v文件夹下面运行命令

L4V_ARCH=X64 misc/regression/run_tests.py AutoCorres

如果没有产生问题，那么就安装完成了

运行项目

想要在Isabelle上使用我们刚才安装的两个工具，请按照如下命令运行你的项目

isabelle jedit -d 你的l4v项目根文件夹路径 -l CParser 你要打开的thy文件

可以使用这个thy文件作为例子，测试一下环境是否征程

theory scratch
  imports "CParser.CTranslation" AutoCorres.AutoCorres
begin
install_C_file minmax.c
autocorres minmax.c

context minmax begin
thm min_body_def
thm min'_def
thm max_body_def
lemma min'_is_min: "min' a b = min a b"
  unfolding min_def min'_def
  by (rule refl)
end

end

注意，theory后面的名字应该根据你的文件名修改，使其保持一致。