邪恶rocq iris

遁入黑暗

4月的时候决定一定要学完semantics-course 居然熬到现在真的学完了 这个blog就是来锐评一下这半年学iris/rocq engineering的各种感想。。。。

IDE 地狱

Rocq 在除了coqtail之外的ide里都没有jump-to-def 不过coqdocjs也会给你不错的jump-to-def（我的理解是两者都是基于类似Locate 也就是说他们对 Tactic Notation 都无效） 不过coqdocjs貌似jump to coq standard library的东西更方便点（不过coqtail貌似可以jump to local libraries）

VSCode + Rocq 就更搞笑了 现在有三个现有的插件可以用：

• VSCoq：当前被推荐的版本 需要最新的vscoq-language-server 插件，只能使用于8.18之后的coq版本，需要specify vscoqtop 路径
• VSCoq-Legacy：不需要任何新的插件 貌似是直接parse coqtop的输出（貌似还自带一个coqidetop?） 可以specify project root（所以可以不在project root开editor）
• coq-lsp：需要下载coq-lsp，上面两个都不能jump-to-def但是这个可以！ 证明的部分不会标绿 而且不能stepForward/Backward 而是只读cursor的位置 （这不是lean吗）jump-to-def不能跳Notation
  • 不知道为什么 coq-lsp 不能recognize iris.heap_lang 然后在 semantics-course 里会有一些其他versioning问题。。。 好像被神秘治好了，，，

某种程度上出了jump-to-def我还想要跟opam switch link <switch-name> . 一样能自动识别当前project path的coqc的ide。。。 vscoq/vscoq-legacy每次换project都要改path

学习iris？

我是照着MPI-SWS的semantics course来学的iris [lecture notes] [ws23-24]

相比iris-lecture-notes和iris-tutorials这个系列。semantics course更注重于logical relations和semantic typing 整本书前半跟iris没有关系 而是某种更有重点的TAPL