7

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?

Mogsdad
  • 44,709
  • 21
  • 151
  • 275
Lance
  • 75,200
  • 93
  • 289
  • 503

2 Answers2

6

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).

Jason Gross
  • 5,928
  • 1
  • 26
  • 53
  • 1
    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 http://coqfinitgroup.gforge.inria.fr/doc/fintype.html#Finite.Exports.finType (or something along those lines, maybe the local copy of ssreflect source code or similar) – Lance Jul 18 '15 at 18:51
  • 1
    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 https://itu.dk/research/tomeso/coqoon/, though I haven't tried it." – Lance Jul 18 '15 at 19:24
  • 1
    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." – Lance Jul 18 '15 at 19:28
  • got this error `No object of basename cbn`...weird no? `Locate cbn.` – Charlie Parker Mar 04 '22 at 17:39
  • `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. – Jason Gross Mar 05 '22 at 18:31
3

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.

Anton Trunov
  • 15,074
  • 2
  • 23
  • 43