如何高效地查找 Coq 中标识符的定义位置？

Question

在大多数IDE或文本编辑器中，您可以右键单击术语，然后转到定义该术语的文件。但是CoqIDE似乎没有这个功能，所以我一直在使用coqdoc myfile.v --html，然后转到生成的HTML文档。但是，在该文件中，只有Coq标准库的术语可点击。由ssreflect定义的术语（例如）无法点击。

当在Coq文件中时，是否有一种标准方法可以快速查找某个术语/标识符的定义位置（以及其源代码）？无论是在CoqIDE还是在emacs + ProofGeneral中（我正在使用CoqIDE，但如果emacs / ProofGeneral具有此功能，我会切换过去）。

或者，标准方法是为您使用的每个Coq项目和依赖项生成文档？

- Lance

Answer 1

如果您突出显示一个术语，然后执行“查询” ->“定位”，或者评估 Locate some_identifier. ，您将获得常量的完整名称。如果您知道依赖项安装的位置，则可以查找标识符的位置。

编辑：如果您想要标识符的定义，可以使用 Print 。如果您只想要其类型，则可以使用 About 或 Check （它还接受表达式，而不仅仅是标识符）。

- Jason Gross

---

很接近了，但是Queries -> Locate on finType 给出了这个结果："Notation Ssreflect.fintype.Finite.Exports.finType"（这很有帮助）。但是有没有一种方法可以将我链接到源代码或文档呢？所以它应该链接到http://coqfinitgroup.gforge.inria.fr/doc/fintype.html#Finite.Exports.finType（或类似的东西，可能是ssreflect源代码的本地副本或类似的东西）。 - Lance

在 #coq IRC 中跟进。Jason 说：“目前我不认为有办法做到这一点。源文件甚至没有被安装，尽管我认为他们可能很快会修复这个问题（或在下一个测试版中）。但使用 https://itu.dk/research/tomeso/coqoon/ 可能是可行的，虽然我还没有尝试过。” - Lance

他还提到了他的典型工作流程，这对参考很有帮助：“我使用Locate。如果是我的文件，我会打开相关的源文件。如果是Coq.*，我要么去github.coq/coq/coq，要么去本地的Coq源代码副本。如果是我安装的库，我就去我安装它的目录。但更频繁的情况是，我只是打印标识符，或者使用About或Check，这会给我完整的定义（减去任何文档或格式）。类型签名，有时加上定义，通常就足够了。” - Lance

收到了这个错误 No object of basename cbn...很奇怪吧？请定位cbn。 - Charlie Parker

“Locate” 对 Ltac AST 的组件（对于 Tactic Notations 也是如此）效果不好。如果您想找到 cbn，可以在 Coq 源代码中使用 “git grep”。 - Jason Gross

Answer 2

有一个基于Proof General的工具叫做company-coq，它默认绑定了使用M-.快捷键跳转到定义的功能。

只有在使用Require命令或其变种要求模块的情况下，它才能跳转到光标下的定义（甚至包括标准库）。

- Anton Trunov