遁入黑暗
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）
学习iris？
我是照着MPI-SWS的semantics course来学的iris 相比iris-lecture-notes和iris-tutorials这个系列 semantics course更注重于logical relations和semantic typing 整本书前半跟iris没有关系 而是某种更有重点的TAPL（TAPL进入了很多iris