How do you look up where identifiers are defined in Coq efficiently?

Question

In most IDEs or text editors, you can right-click a term and it takes you to the file where that term is defined. CoqIDE doesn't seem to have that, so I've been doing coqdoc myfile.v --html, then going to the generated HTML docs. But the only clickable terms in that file are for Coq Standard Library. Terms defined by ssreflect (for example) aren't clickable.

Is there a standard way to be able to quickly lookup where some term/identifier is defined (and the source code for it) when in a Coq file? Either in the CoqIDE or in emacs + ProofGeneral (I'm using CoqIDE, but I'd switch if emacs/ProofGeneral had this ability).

Or is the standard way to generate docs for every Coq project and dependency you use?

Retiary

Answer 1

If you highlight a term, and do Queries -> Locate, or you evaluate Locate some_identifier., you will get the full name of the constant. If you know where the dependencies are installed, this will tell you where to look for the identifier.

Edit: If you want the definition of the identifier, you can Print it. If you just want it's type, you can use About, or Check (which also accepts expressions, and not just identifiers).

Dupuis

That's close, but Queries -> Locate on finType gives this: "Notation Ssreflect.fintype.Finite.Exports.finType" (which is helpful). But is there a way for it to link me to the source code, or the docs somehow? So instead it would go to coqfinitgroup.gforge.inria.fr/doc/… (or something along those lines, maybe the local copy of ssreflect source code or similar) – Retiary

Follow up in #coq IRC. Jason said "No, I don't think there's a way to do that, currently. The source files don't even get installed, though I think they might be fixing that soon (or in the next beta). It might be possible to do with itu.dk/research/tomeso/coqoon, though I haven't tried it." – Retiary

He also said about his typical workflow which was helpful (for reference): "I use Locate. If it's my own file, I open the relevant source file. If it's Coq.*, I either go to github.coq/coq/coq, or to a local copy of the Coq source code. If it's a library I installed, I go to the directory I installed it from. But, more frequently, I just Print the identifier, or use About or Check, instead, which gives me the full definition (less any documentation or formatting). The type signature, plus sometimes the definition, is often enough." – Retiary

got this error No object of basename cbn...weird no? Locate cbn. – Thiosinamine

Locate does not work very well for components of the Ltac AST (nor for Tactic Notations, for that matter). If you want to find cbn, you can use git grep on the Coq sources. – Dupuis

Answer 2

There is a tool working on top of Proof General, called company-coq. It has the jump to definition feature bound to the M-. keyboard shortcut by default.

It can jump to the definition under cursor (even to the standard library) only if the module containing the definition is required with Require command or its variant.

Usia