最近想尝试Rocq（以前叫Coq），所以安装来试试，国内这方面的东西好像比较少，所以记录一下过程。
下载Rocq
官网的下载链接，因为学院服务器太老了，而且我没有sudo权限，所以我就直接在自己的Windows电脑上装了，所以平台选到Windows，然后我用的是推荐的 Rocq Platform，直接点下面的Download the Rocq Platform binary installer按钮
然后下滑一下在这里找到Windows的安装包，
注意这个是从GitHub下载的，500多M。
安装配置Rocq
下载完之后安装就是一路下一步就行了很简单，只要记得改个路径以及记得路径在哪就行了。然后需要手动设置个环境变量，Windows设置环境变量的过程就不详细说了，把刚刚安装的Rocq的bin目录加入Path变量，比如我的是D:\app\Rocq-Platform~9.0~2025.08\bin。
然后编辑器，我不喜欢那个rocqide，看起来太原始了，而且界面是英文的，所以还是一个vscode走天下。打开vscode在扩展里面安装vsrocq，如果之前环境变量没有正确设置的话，它会提醒你没有安装language server，如果不想设置环境变量需要在插件设置里面手动指定bin\vsrocqtop.exe。到目前为止已经可以用vscode写rocq了，可以新建个test.v来试试。
代码窗口右上角有一些按钮可以点来运行，可以自己试试怎么用，或者也可以右键点击运行到光标处。
右边是显示结果和一些信息，但是目前看来没有lean4的好看，不过毕竟也是刚刚尝试，可能是还没接触到有趣的地方。
一些优化
为了让它看起来更加现代化，并且更加优雅，可以进行一些其他的设置，首先打开vsrocq的插件设置，把补全打开，虽然这个补全也是跟残废一样，只能补全出现过的词，甚至不能补全语言自带的关键字，只能说聊胜于无，起码完整输入过一次Definition之后就只用输入def然后按tab了
另外就是用过lean4之后我对优雅有了更高的要求，比如我不想认为我是在写代码，我想让它的符号看起来更加数学，所以我们可以把vscode的连字符打开，并且选个支持连字符的字体。
在vscode的设置中输入ligatures，然后应该会有这个选项
然后在setting.json中把"editor.fontLigatures": false改成"editor.fontLigatures": true，再设置个支持连字付哈的字体，如"editor.fontFamily": "Fira Code"，最后的效果
如果竖线再连起来就更好了，或者大家可以自己找喜欢的字体。