在Vim中使用merlin在ocaml中开发coq插件

Posted

tags:

篇首语:本文由小常识网(cha138.com)小编为大家整理,主要介绍了在Vim中使用merlin在ocaml中开发coq插件相关的知识,希望对你有一定的参考价值。

我安装了带有opam的Coq,并希望制作一个Coq插件。我设法使用coq_makefile编译了一些插件示例,但是如果我可以在vim中使用merlin来获取类型信息并完成Coq库,那就太好了。

是否可以将Coq库添加到ocamlfind?

答案

coq_makefile现在将为您生成一个.merlin。只需输入

make .merlin
另一答案

最后,我回答了自己。仅需使用指令B

将coq的cmi文件的目录放在.merlin文件中。
B path/to/coq/kernel
B path/to/coq/library
...
另一答案

我不知道如何正确使用coq_makefile来执行此操作,@ Nico Lehmann的答案对我不起作用。

我的.merlin文件是:

FLG -rectypes
S /usr/lib/coq/**
B /usr/lib/coq/**

第一行很重要(我不知道这是什么意思)。当然,将/usr/lib/更改为您的Coq所在的路径。您可以通过在命令行中运行coqc -where来找到Coq位置。

以上是关于在Vim中使用merlin在ocaml中开发coq插件的主要内容,如果未能解决你的问题,请参考以下文章

为啥 OCaml 有时需要 eta 扩展?

Coq 中同一个库的不同版本

如何在 Coq 中使用归纳类型处理案例

函数式程序设计入门讲义

如何在 Coq 中使用包含全称量词的假设?

如何在 Coq 中使用 Rmult 在一个术语中重写 Rle?