The Coq mailing list

[Clément Pit--Claudel <clement.pit AT gmail.com>]

Thanks for that suggestion. 

It's an interesting fallback, but it doesn't have the flexibility that I'm 
looking for; in particular, it doesn't tell you which commands are accessible 
at a given point in a proof, and under which name (depending on what you 
[Require Import], symbols may be available under different names).

Clément.

On 02/19/2015 12:10 PM, Abhishek Anand wrote:
> One way to do auto-completion is to crawl the content of all relevant .glob 
> files when the IDE starts.
> That way, you can also implement "jump to definition".
> In the .glob files, ignore the first 2 lines and then look for lines that 
> start with one of the following:
> rec, proj, def, not ,...
> The last word of these lines are names of the identifier that got defined. 
> One of the words
> in the middle specifies the byte offsets in the corresponding .v file where 
> that identifier was defined.
> 
> For example, consider the following line taken from a .glob file
> 
> def 679:685 <> enqueue
> 
> It says that the identifier enqueue got defined at between the byte offsets 
> 679 and 685.
> 679 is the byte-offset you should jump to if the user wants to see the 
> definition of enqueue.
> 
> 
> Regards,
> -- Abhishek
> http://www.cs.cornell.edu/~aa755/
> 
> On Wed, Feb 18, 2015 at 6:16 PM, Clément Pit--Claudel 
> <clement.pit AT gmail.com
>  
> <mailto:clement.pit AT gmail.com>>
>  wrote:
> 
>     Hi all,
> 
>     Is there a way to list all identifiers known to Coq, without printing 
> their type? Something similar to the output of [SearchPattern _], but with 
> type information stripped out. That is, a way to get
> 
>         Mult.mult_plus_distr_l
>         Mult.mult_succ_l
>         Mult.mult_succ_r
>         Mult.odd_even_lem
>         Mult.mult_acc_aux
> 
>     instead of
> 
>         Mult.mult_plus_distr_l: forall n m p : nat, n * (m + p) = n * m + n 
> * p
>         Mult.mult_succ_l: forall n m : nat, S n * m = n * m + m
>         Mult.mult_succ_r: forall n m : nat, n * S m = n * m + n
>         Mult.odd_even_lem: forall p q : nat, 2 * p + 1 <> 2 * q
>         Mult.mult_acc_aux: forall n m p : nat, m + n * p = Mult.mult_acc m 
> p n
> 
>     I've pushed a basic implementation of such a feature to 
> https://github.com/cpitclaudel/coq/commit/198b9c47dedf4fa3b2a95ab7102b2d2d4ada392f
>  (it adds an option "Search Minimal", which when activated reduces the 
> output of search commands to just names). It would be nice to have that 
> feature in Coq, though! But perhaps I missed an existing option? Another 
> possible direction would be to implement a [Dump Identifiers To File 
> <path>] command, which would write all names to a separate files.
> 
>     A bit of context: such a command would be useful to get better 
> completion support for Coq in Emacs: using the list of all known terms and 
> theorems one could implement a nice autocompletion package. Unfortunately 
> ProofGeneral currently has trouble dealing with the output of 
> [SearchPattern _] when large libraries are loaded (e.g. Reals), because it 
> uses regular expressions to find the next prompt (in my experiments, 
> reading the full list of all defined terms with their types takes about 3s; 
> patching PG to do a plain string search first takes it down to about 1.5s; 
> without the types, it takes 50ms).
> 
>     Thanks!
>     Clément.
> 
>